Reachability of Hennessy - Milner properties for weakly extended PRS
KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK and 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, p. 213-224. ISBN 3-540-30495-9. |
Other formats:
BibTeX
LaTeX
RIS
|
Basic information | |
---|---|
Original name | Reachability of Hennessy - Milner properties for weakly extended PRS |
Name in Czech | Dosažitelnost Hennessy-Milner vlastností pro slabě rozšířené PRS |
Authors | KŘETÍNSKÝ, Mojmír (203 Czech Republic, guarantor), Vojtěch ŘEHÁK (203 Czech Republic) and Jan STREJČEK (203 Czech Republic). |
Edition | Berlin, Heidelberg, FSTTCS 2005: 25th International Conference on Foundations of Software Technology and Theoretical Computer Science, 25th International Conference, p. 213-224, 12 pp. 2005. |
Publisher | Springer-Verlag |
Other information | |
---|---|
Original language | English |
Type of outcome | Proceedings paper |
Field of Study | 10201 Computer sciences, information science, bioinformatics |
Country of publisher | Germany |
Confidentiality degree | is not subject to a state or trade secret |
RIV identification code | RIV/00216224:14330/05:00012582 |
Organization unit | Faculty of Informatics |
ISBN | 3-540-30495-9 |
UT WoS | 000234885800017 |
Keywords in English | process rewrite systems; state extension; infinite-state; (un)decidability; HM logic; reachability |
Tags | (un)decidability, HM logic, infinite-state, process rewrite systems, reachability, state extension |
Tags | International impact, Reviewed |
Changed by | Changed by: prof. RNDr. Mojmír Křetínský, CSc., učo 631. Changed: 8/4/2010 21:40. |
Abstract |
---|
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. |
Abstract (in Czech) |
---|
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. |
Links | |
---|---|
GA201/03/1161, research and development project | Name: Verifikace nekonečně stavových systémů |
Investor: Czech Science Foundation, Verification of infinite-state systems | |
MSM0021622419, plan (intention) | Name: Vysoce paralelní a distribuované výpočetní systémy |
Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems | |
1ET408050503, research and development project | Name: Techniky automatické verifikace a validace softwarových a hardwarových systémů |
Investor: Academy of Sciences of the Czech Republic, Techniques for automatic verification and validation of software nad hardware systems | |
1M0545, research and development project | Name: Institut Teoretické Informatiky |
Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science |
PrintDisplayed: 18/9/2024 22:24