LTL Hierarchies and Model Checking

Varování

Publikace nespadá pod Pedagogickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Autoři	PELÁNEK Radek
Rok publikování	2003
Druh	Článek ve sborníku
Konference	Proceedings of the Eight ESSLLI Student Session
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
Obor	Informatika
Klíčová slova	LTL; model checking
Popis	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.
Související projekty:	Automatizovaná verifikace paralelních a distribuovaných systémů Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů