LTL Hierarchies and Model Checking

PELÁNEK, Radek. LTL Hierarchies and Model Checking. In Proceedings of the Eight ESSLLI Student Session. Wien: TU Wien, 2003, s. 245-254, 9 s.

Základní údaje

Originální název

LTL Hierarchies and Model Checking

Autoři

PELÁNEK, Radek (203 Česká republika, garant)

Vydání

Wien, Proceedings of the Eight ESSLLI Student Session, od s. 245-254, 9 s. 2003

Nakladatel

TU Wien

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Rakousko

Utajení

není předmětem státního či obchodního tajemství

Kód RIV

RIV/00216224:14330/03:00008596

Organizační jednotka

Fakulta informatiky

Klíčová slova anglicky

LTL; model checking

Štítky

LTL, Model checking

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

We propose a new hierarchy of LTL formulas based on alternations of Until and Release operators and show that it is more relevant to model checking then previously studied hierarchies. Moreover, we study practically used formulas and conclude that in most cases it is possible to use specialized algorithms which are more efficient then general algorithm for LTL model checking.

---

Návaznosti

GA201/03/0509, projekt VaV	Název: Automatizovaná verifikace paralelních a distribuovaných systémů Investor: Grantová agentura ČR, Automatizovaná verifikace paralelních a distribuovaných systémů
MSM 143300001, záměr	Název: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů