Informace o publikaci
On Decidability of LTL Model Checking for Process Rewrite Systems
| Název česky | O rozhodnutelnosti problému ověřování modelu pro LTL a procesové přepisovací systémy |
|---|---|
| Autoři | |
| 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 | |
| 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: |