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, roč. 207, č. 6, s. 671-680. ISSN 0890-5401. 2009.
Další formáty:   BibTeX LaTeX RIS
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
Originální 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í
WWW 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
Změnil Změnil: prof. RNDr. Mojmír Křetínský, CSc., učo 631. Změněno: 7. 5. 2009 10:19.
Anotace
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.
Anotace č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 VaVNá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 VaVNá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 VaVNá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ěrNá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 VaVNá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 VaVNázev: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky
VytisknoutZobrazeno: 28. 3. 2024 18:53