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. In FSTTCS 2006: 26th International Conference on Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings. Berlin: Springer-Verlag, 2006, s. 248-259. ISBN 978-3-540-49994-7.

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í

Berlin, FSTTCS 2006: 26th International Conference on Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings, od s. 248-259, 12 s. 2006

Nakladatel

Springer-Verlag

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Indie

Utajení

není předmětem státního či obchodního tajemství

Kód RIV

RIV/00216224:14330/06:00015417

Organizační jednotka

Fakulta informatiky

ISBN

978-3-540-49994-7

UT WoS

000244553400024

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), possibly extended with a weak finite-state control unit, and properties described by basic fragments of action-based Linear Temporal Logic (LTL). 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. As our main result, we show that the problem is decidable for wPRS if we consider properties defined by formulae with only modalities "strict eventually" and "strict always". 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 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".

---

Návaznosti

GA201/06/1338, projekt VaV	Název: Automatizovaná verifikace softwaru Investor: Grantová agentura ČR, Automatizovaná verifikace softwaru
GD102/05/H050, projekt VaV	Název: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů Investor: Grantová agentura ČR, Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
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
1ET408050503, projekt VaV	Název: Techniky automatické verifikace a validace softwarových a hardwarových systémů Investor: Akademie věd ČR, Techniky automatické verifikace a validace softwarových a hardwarových systémů
1M0545, projekt VaV	Název: Institut Teoretické Informatiky Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky