On Decidability of LTL+Past Model Checking for Process Rewrite Systems

Varování

Publikace nespadá pod Ústav výpočetní techniky, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Název česky	O rozhodnutelnosti ověřování modelu pro logiku LTL+Past a Procesové Přepisovací Systémy
Autoři	KŘETÍNSKÝ Mojmír ŘEHÁK Vojtěch STREJČEK Jan
Rok publikování	2009
Druh	Článek ve sborníku
Konference	Joint Proceedings of the 8th, 9th, and 10th International Workshops on Verification of Infinite-State Systems (INFINITY 2006, 2007, 2008)
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
www	http://dx.doi.org/10.1016/j.entcs.2009.05.033
Obor	Informatika
Klíčová slova	process rewrite systems; LTL; infinite-state; model-checking; decidability
Popis	Je stanovena hranice rozhodnutelnosti ověřování modelu pro logiku LTL+Past a slabě rozšířené Procesové Přepisovací Systémy.
Související projekty:	Techniky automatické verifikace a validace softwarových a hardwarových systémů Institut Teoretické Informatiky Vysoce paralelní a distribuované výpočetní systémy Formální verifikace: algoritmy, vlastnosti modelovacích formalismů a temporálních logik Nové možnosti automatické verifikace síťových protokolů Verifikace a analýza velmi velkých počítačových systémů