Reachability of Hennessy - Milner properties for weakly extended PRS

• Název česky: Dosažitelnost Hennessy-Milner vlastností pro slabě rozšířené PRS
• Autoři: KŘETÍNSKÝ Mojmír; ŘEHÁK Vojtěch; STREJČEK Jan
• Rok publikování: 2005
• Druh: Článek ve sborníku
• Konference: FSTTCS 2005: 25th International Conference on Foundations of Software Technology and Theoretical Computer Science, 25th International Conference
• Fakulta / Pracoviště MU: Fakulta informatiky
• Obor: Informatika
• Klíčová slova: process rewrite systems; state extension; infinite-state; (un)decidability; HM logic; reachability
• Popis: Zabýváme se problémem, zda-li daný slabě rozšířený procesový přepisovací systém (wPRS) obsahuje dosažitelný stav splňující danou formuli Hennessy-Milner logiky. Ukážeme, že tento problém je rozhodnutelný. Jako důsledek dostáváme rozhodnutelnost silné bisimulace mezi wPRS a konečně stavovými systémy. Rozhodnutelnost tohoto problému pro podtřídy wPRS nazývané PAN a PRS byla otevřenou otázkou (viz [Srb02]). Taktéž zesílíme některé výsledky o nerozhodnutelnosti.

Související projekty

• Verifikace nekonečně stavových systémů
• Techniky automatické verifikace a validace softwarových a hardwarových systémů
• Institut Teoretické Informatiky
• Vysoce paralelní a distribuované výpočetní systémy