On Decidability of LTL 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 problému ověřování modelu pro LTL a procesové přepisovací systémy
Autoři	BOZZELLI Laura KŘETÍNSKÝ Mojmír ŘEHÁK Vojtěch STREJČEK Jan
Rok publikování	2006
Druh	Článek ve sborníku
Konference	FSTTCS 2006: 26th International Conference on Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
Obor	Informatika
Klíčová slova	infinite-state systems; linear time logic; decidability; model checking
Popis	Je ustanovena hranice rozhodnutelnosti pro problém ověřování modelu pro fragmenty logiky LTL a nekonečně stavové systémy generované tzv. procesovými přepisovacími systémy (eventuelně rozšířenými o tzv.slabou konečně stavovou řídicí jednotku). Zejména je ukázáno, že tento problém je rozhodnutelný na celé zmíněné třídě pro LTL frament s modalitami "strict always" a "strict eventually". Problém je nerozhodnutelný pro třídu PA procesů a fragment s modalitou "until" resp. fragment s modalitami "next" a "infinitely often".
Související projekty:	Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů Techniky automatické verifikace a validace softwarových a hardwarových systémů Institut Teoretické Informatiky Vysoce paralelní a distribuované výpočetní systémy Automatizovaná verifikace softwaru