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. s. 105-117. ISSN 1571-0661. 2009.
Další formáty:   BibTeX LaTeX RIS
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
Originální 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í
WWW URL
Kód RIV RIV/00216224:14330/09:00028439
Organizační jednotka Fakulta informatiky
ISSN 1571-0661
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
Změnil Změnil: doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721. Změněno: 23. 6. 2009 16:57.
Anotace
The Decidability Borderline for Model Checking of LTL+Past and Weakly--Extended Process Rewrite Systems is determined.
Anotace č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 VaVNá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 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
GP201/08/P459, projekt VaVNá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ě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
1ET408050503, projekt VaVNá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 VaVNázev: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky
VytisknoutZobrazeno: 28. 3. 2024 18:20