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, 2009, vol. 207, No 6, p. 671-680. ISSN 0890-5401.

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

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

References:

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

In the original language

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.

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