Reachability is decidable for weakly extended process rewrite systems

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

Základní údaje

Originální název

Reachability is decidable for weakly extended process rewrite systems

Název česky

Dosažitelnost je rozhodnutelná pro slabě rozšířené 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í

Information and Computation, Elsevier, 2009, 0890-5401

---

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

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

Odkazy

URL

Impakt faktor

Impact factor: 1.225

Kód RIV

RIV/00216224:14330/09:00028490

Organizační jednotka

Fakulta informatiky

UT WoS

000267337100001

Klíčová slova anglicky

process rewrite systems; state extension; infinite-state; (un)decidability; reachability

Štítky

(un)decidability, infinite-state, process rewrite systems, reachability, state extension

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

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.

Česky

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.

---

Návaznosti

GA201/09/1389, projekt VaV	Ná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 VaV	Ná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 VaV	Ná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ěr	Ná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 VaV	Ná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 VaV	Název: Institut Teoretické Informatiky Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky