Reachability of Hennessy - Milner properties for weakly extended PRS

KŘETÍNSKÝ, Mojmír; Vojtěch ŘEHÁK a Jan STREJČEK. Reachability of Hennessy - Milner properties for weakly extended PRS. In FSTTCS 2005: 25th International Conference on Foundations of Software Technology and Theoretical Computer Science, 25th International Conference. Berlin, Heidelberg: Springer-Verlag, 2005, s. 213-224. ISBN 3-540-30495-9.

Základní údaje

Originální název

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; Vojtěch ŘEHÁK a Jan STREJČEK

Vydání

Berlin, Heidelberg, FSTTCS 2005: 25th International Conference on Foundations of Software Technology and Theoretical Computer Science, 25th International Conference, od s. 213-224, 12 s. 2005

Nakladatel

Springer-Verlag

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/05:00012582

Organizační jednotka

Fakulta informatiky

ISBN

3-540-30495-9

UT WoS

000234885800017

Klíčová slova anglicky

process rewrite systems; state extension; infinite-state; (un)decidability; HM logic; reachability

Štítky

(un)decidability, HM logic, infinite-state, process rewrite systems, reachability, state extension

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

We examine the problem whether a given weakly extended process rewrite system (wPRS) contains a reachable state satisfying a given formula of Hennessy-Milner logic. We show that this problem is decidable. As a corollary we observe that the problem of strong bisimilarity between wPRS and finite-state systems is decidable. Decidability of the same problem for wPRS subclasses, namely PAN and PRS, has been formulated as an open question, see e.g. [Srb02]. We also strengthen some related undecidability results on some PRS subclasses.

Česky

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.

---

Návaznosti

GA201/03/1161, projekt VaV	Název: Verifikace nekonečně stavových systémů Investor: Grantová agentura ČR, Verifikace nekonečně stavových systémů
MSM0021622419, záměr	Název: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
1ET408050503, projekt VaV	Název: Techniky automatické verifikace a validace softwarových a hardwarových systémů Investor: Akademie věd ČR, Techniky automatické verifikace a validace softwarových a hardwarových systémů
1M0545, projekt VaV	Název: Institut Teoretické Informatiky Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky