On Decidability of LTL+Past Model Checking for Process Rewrite Systems

KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a Jan STREJČEK. On Decidability of LTL+Past Model Checking for Process Rewrite Systems. In Joint Proceedings of the 8th, 9th, and 10th International Workshops on Verification of Infinite-State Systems (INFINITY 2006, 2007, 2008). 2009. vyd. Amsterdam, The Netherlands: Elsevier Science Publishers, 2009, s. 105-117. ISSN 1571-0661.

Základní údaje

Originální název

On Decidability of LTL+Past Model Checking for Process Rewrite Systems

Název česky

O rozhodnutelnosti ověřování modelu pro logiku LTL+Past a Procesové Přepisovací Systémy

Autoři

KŘETÍNSKÝ, Mojmír (203 Česká republika), Vojtěch ŘEHÁK (203 Česká republika) a Jan STREJČEK (203 Česká republika, garant)

Vydání

2009. vyd. Amsterdam, The Netherlands, Joint Proceedings of the 8th, 9th, and 10th International Workshops on Verification of Infinite-State Systems (INFINITY 2006, 2007, 2008), od s. 105-117, 13 s. 2009

Nakladatel

Elsevier Science Publishers

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Portugalsko

Utajení

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

Odkazy

URL

Kód RIV

RIV/00216224:14330/09:00028439

Organizační jednotka

Fakulta informatiky

ISSN

Klíčová slova anglicky

process rewrite systems; LTL; infinite-state; model-checking; decidability

Štítky

decidability, infinite-state, LTL, Model-Checking, process rewrite systems

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

The Decidability Borderline for Model Checking of LTL+Past and Weakly--Extended Process Rewrite Systems is determined.

Česky

Je stanovena hranice rozhodnutelnosti ověřování modelu pro logiku LTL+Past a slabě rozšířené Procesové Přepisovací Systémy.

---

Návaznosti

GA201/09/1389, projekt VaV	Název: Verifikace a analýza velmi velkých počítačových systémů Investor: Grantová agentura ČR, Verifikace a analýza velmi velkých počítačových systémů
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
GP201/08/P459, projekt VaV	Název: Nové možnosti automatické verifikace síťových protokolů Investor: Grantová agentura ČR, Nové možnosti automatické verifikace síťových protokolů
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