Reachability of Hennessy - Milner properties for weakly extended PRS

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