Reachability is decidable for weakly extended process rewrite systems

Varování

Publikace nespadá pod Ústav výpočetní techniky, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Název česky	Dosažitelnost je rozhodnutelná pro slabě rozšířené procesové přepisovací systémy
Autoři	KŘETÍNSKÝ Mojmír ŘEHÁK Vojtěch STREJČEK Jan
Rok publikování	2009
Druh	Článek v odborném periodiku
Časopis / Zdroj	Information and Computation
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
www	http://dx.doi.org/10.1016/j.ic.2009.01.003
Obor	Informatika
Klíčová slova	process rewrite systems; state extension; infinite-state; (un)decidability; reachability
Popis	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.
Související projekty:	Techniky automatické verifikace a validace softwarových a hardwarových systémů Institut Teoretické Informatiky Vysoce paralelní a distribuované výpočetní systémy Formální verifikace: algoritmy, vlastnosti modelovacích formalismů a temporálních logik Nové možnosti automatické verifikace síťových protokolů Verifikace a analýza velmi velkých počítačových systémů