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í	2009
Druh	Článek v odborném periodiku
Časopis / Zdroj	Acta informatica
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
www	http://springerlink.com/content/4610330747913678/?p=9daadd38980f4b8695a892fd058e8e5e&pi=0
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 s budoucími i minulostními operátory a nekonečně stavové systémy generované tzv. procesovými přepisovacími systémy (PRS) nebo slabě rozšířenými procesovými přepisovacími systémy (wPRS). Je známo, že tento problém je pro obecnou LTL rozhodnutelný pro Petriho sítě a zásobníkové procesy, ale nerozhodnutelný pro PA procesy. Ukážeme, že tento problém je rozhodnutelný pro třídu wPRS pokud uvažujeme LTL frament s modalitami "strict always", "strict eventually" a jejich minulostními verzemi. Dále ukážeme, že 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:	Institut Teoretické Informatiky Vysoce paralelní a distribuované výpočetní systémy Automatizovaná verifikace softwaru Formální verifikace: algoritmy, vlastnosti modelovacích formalismů a temporálních logik