BOZZELLI, Laura, Mojmír KŘETÍNSKÝ, Vojtěch ŘEHÁK a Jan STREJČEK. On Decidability of LTL Model Checking for Process Rewrite Systems. Acta informatica. Berlin: Springer-Verlag, roč. 46, č. 1, s. 1-28. ISSN 0001-5903. 2009.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název 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 BOZZELLI, Laura (380 Itálie), Mojmír KŘETÍNSKÝ (203 Česká republika, garant), Vojtěch ŘEHÁK (203 Česká republika) a Jan STREJČEK (203 Česká republika).
Vydání Acta informatica, Berlin, Springer-Verlag, 2009, 0001-5903.
Další údaje
Originální jazyk angličtina
Typ výsledku Článek v odborném periodiku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Německo
Utajení není předmětem státního či obchodního tajemství
WWW URL
Impakt faktor Impact factor: 0.923
Kód RIV RIV/00216224:14330/09:00029078
Organizační jednotka Fakulta informatiky
UT WoS 000262531800001
Klíčová slova anglicky infinite-state systems; linear time logic; decidability; model checking
Štítky decidability, infinite-state systems, linear time logic, Model checking
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721. Změněno: 22. 5. 2009 16:43.
Anotace
We establish a decidability boundary of the model checking problem for infinite-state systems defined by Process Rewrite Systems (PRS) or weakly extended Process Rewrite Systems (wPRS), and properties described by basic fragments of action-based Linear Temporal Logic (LTL) with both future and past operators. It is known that the problem for general LTL properties is decidable for Petri nets and for pushdown processes, while it is undecidable for PA processes. We show that the problem is decidable for wPRS if we consider properties defined by LTL formulae with only modalities strict eventually, strict always, and their past counterparts. Moreover, we show that the problem remains undecidable for PA processes even with respect to the LTL fragment with the only modality until or the fragment with modalities next and infinitely often.
Anotace česky
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".
Návaznosti
GA201/06/1338, projekt VaVNázev: Automatizovaná verifikace softwaru
Investor: Grantová agentura ČR, Automatizovaná verifikace softwaru
GP201/08/P375, projekt VaVNázev: Formální verifikace: algoritmy, vlastnosti modelovacích formalismů a temporálních logik
Investor: Grantová agentura ČR, Formální verifikace: algoritmy, vlastnosti modelovacích formalismů a temporálních logik
MSM0021622419, záměrNázev: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
1M0545, projekt VaVNázev: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky
VytisknoutZobrazeno: 29. 3. 2024 10:19