Reachability of Hennessy - Milner properties for weakly extended PRS

Logo poskytovatele

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
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

Citace
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:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.