Reachability is decidable for weakly extended process rewrite systems

KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK and Jan STREJČEK. Reachability is decidable for weakly extended process rewrite systems. Information and Computation. Elsevier, vol. 207, No 6, p. 671-680. ISSN 0890-5401. 2009.

Basic information

• Original name: Reachability is decidable for weakly extended process rewrite systems
• Name in Czech: Dosažitelnost je rozhodnutelná pro slabě rozšířené 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: Information and Computation, Elsevier, 2009, 0890-5401.

Other information

• Original language: English
• Type of outcome: Article in a journal
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: Germany
• Confidentiality degree: is not subject to a state or trade secret
• WWW: URL
• Impact factor: Impact factor: 1.225
• RIV identification code: RIV/00216224:14330/09:00028490
• Organization unit: Faculty of Informatics
• UT WoS: 000267337100001
• Keywords in English: process rewrite systems; state extension; infinite-state; (un)decidability; reachability
• Tags: (un)decidability, infinite-state, process rewrite systems, reachability, state extension
• Tags: International impact, Reviewed

Abstract

Process Rewrite Systems (PRS) are widely accepted as a formalism for the description of infinite-state systems. It is known that the reachability problem for PRS is decidable. The problem becomes undecidable when PRS are extended with a~finite-state control unit. In this paper we show that the problem remains decidable when PRS are extended with a weak (i.e. acyclic except for self-loops) finite-state control unit. We also present some applications of this decidability result.

Abstract (in Czech)

Procesové přepisovací systémy (PRS) jsou akceptovaným formalismem pro popis nekonečně-stavových systémů. Je známo, že problém dosažitelnosti je pro PRS rozhodnutelný. Tento problém se stává nerozhodnutelným, pokud PRS rozšíříme o konečně-stavovou řídící jednotku. V článku dokážeme, že problém zůstává rozhodnutelný, když PRS rozšíříme pouze o slabou (acyklickou) konečně-stavovou řídící jednotku. Také představíme některé aplikace tohoto výsledku.

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