Informační systém Masarykovy univerzity 

Reachability is decidable for weakly extended process rewrite systems

česky | in English

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 Informatika
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, Standardní projekty
GP201/08/P375, projekt VaVNázev: Formální verifikace: algoritmy, vlastnosti modelovacích formalismů a temporálních logik
Investor: Grantová agentura ČR, Postdoktorské projekty
GP201/08/P459, projekt VaVNázev: Nové možnosti automatické verifikace síťových protokolů
Investor: Grantová agentura ČR, Postdoktorské projekty
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, Výzkumné záměry
1ET408050503, projekt VaVNázev: Techniky automatické verifikace a validace softwarových a hardwarových systémů
Investor: Akademie věd ČR, Informační společnost (Národní program výzkumu)
1M0545, projekt VaVNázev: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumná centra (Národní program výzkumu)
VytisknoutZobrazeno: 21. 10. 2017 21:14

Relevantní odkazy 


Nahoru | Aktuální datum a čas: 21. 10. 2017 21:14, 42. (sudý) týden

Kontakty: istech(zavináč/atsign)fi(tečka/dot)muni(tečka/dot)cz, studijní odd., správci práv, is-technici, e-technici, IT podpora | Použití cookies | Více o Informačním systému