On Decidability of LTL Model Checking for Process Rewrite Systems

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, 2009, roč. 46, č. 1, s. 1-28. ISSN 0001-5903.

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

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í

Odkazy

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

---

Anotace

V originále

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.

Č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 VaV	Název: Automatizovaná verifikace softwaru Investor: Grantová agentura ČR, Automatizovaná verifikace softwaru
GP201/08/P375, projekt VaV	Ná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ěr	Ná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 VaV	Název: Institut Teoretické Informatiky Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky