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. |
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 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 |
VytisknoutZobrazeno: 28. 9. 2024 04:10