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; Ř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
• 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ů