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

KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK and 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). 2009th ed. Amsterdam, The Netherlands: Elsevier Science Publishers, 2009, p. 105-117. ISSN 1571-0661.

Basic information

• Original name: On Decidability of LTL+Past Model Checking for Process Rewrite Systems
• Name in Czech: O rozhodnutelnosti ověřování modelu pro logiku LTL+Past a Procesové Přepisovací Systémy
• Authors: KŘETÍNSKÝ, Mojmír (203 Czech Republic), Vojtěch ŘEHÁK (203 Czech Republic) and Jan STREJČEK (203 Czech Republic, guarantor).
• Edition: 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), p. 105-117, 13 pp. 2009.
• Publisher: Elsevier Science Publishers

Other information

• Original language: English
• Type of outcome: Proceedings paper
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: Portugal
• Confidentiality degree: is not subject to a state or trade secret
• WWW: URL
• RIV identification code: RIV/00216224:14330/09:00028439
• Organization unit: Faculty of Informatics
• ISSN: 1571-0661
• Keywords in English: process rewrite systems; LTL; infinite-state; model-checking; decidability
• Tags: decidability, infinite-state, LTL, Model-Checking, process rewrite systems
• Tags: International impact, Reviewed

Abstract

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

Abstract (in Czech)

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

Links

• GA201/09/1389, research and development project: Name: Verifikace a analýza velmi velkých počítačových systémů

Investor: Czech Science Foundation, Verification and Analysis of Large-Scale Computer Systems

• GP201/08/P375, research and development project: Name: Formální verifikace: algoritmy, vlastnosti modelovacích formalismů a temporálních logik

Investor: Czech Science Foundation, Formal verification: algorithms, properties of modelling formalisms amd temporal logics

• GP201/08/P459, research and development project: Name: Nové možnosti automatické verifikace síťových protokolů

Investor: Czech Science Foundation, New possibilities in automatic verification of network protocols

• MSM0021622419, plan (intention): Name: Vysoce paralelní a distribuované výpočetní systémy

Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems

• 1ET408050503, research and development project: Name: Techniky automatické verifikace a validace softwarových a hardwarových systémů

Investor: Academy of Sciences of the Czech Republic, Techniques for automatic verification and validation of software nad hardware systems

• 1M0545, research and development project: Name: Institut Teoretické Informatiky

Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science