On Decidability of LTL Model Checking for Process Rewrite Systems

Logo poskytovatele
Logo poskytovatele

Varování

Publikace nespadá pod Fakultu sportovních studií, 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:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.

Další info