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

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Portugal

Confidentiality degree

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

References:

URL

RIV identification code

RIV/00216224:14330/09:00028439

Organization unit

Faculty of Informatics

ISSN

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

V originále

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

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