On Decidability of LTL Model Checking for Weakly Extended 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 Weakly Extended Process Rewrite Systems. Brno: FI MU. FIMU-RS-2006-05. 2006.

Základní údaje

• Originální název: On Decidability of LTL Model Checking for Weakly Extended Process Rewrite Systems
• Název česky: O rozhodnutelnosti problému ověřování modelu pro LTL a slabě royšířené 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í: Brno, FIMU-RS-2006-05, 2006.
• Nakladatel: FI MU

Další údaje

• Originální jazyk: angličtina
• Typ výsledku: Audiovizuální tvorba
• Obor: 10201 Computer sciences, information science, bioinformatics
• Stát vydavatele: Česká republika
• Utajení: není předmětem státního či obchodního tajemství
• WWW: URL
• Kód RIV: RIV/00216224:14330/06:00015439
• Organizační jednotka: Fakulta informatiky
• 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

Anotace

We establish a decidability boundary of the model checking problem for infinite-state systems defined by \emph{Process Rewrite Systems} (PRS) or \emph{weakly extended Process Rewrite Systems} (wPRS), % possibly extended with a weak finite-state control unit, and properties described by basic fragments of action-based \emph{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 \emph{strict eventually} and \emph{strict always}. Moreover, we show that the problem remains undecidable for PA processes even with respect to the LTL fragment with the only modality \emph{until} or the fragment with modalities \emph{next} and \emph{infinitely often}.

Anotace č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