Publication details
Reachability of Hennessy 
- Milner properties for weakly extended PRS
| Basic information | |
|---|---|
| Original title: | Reachability of Hennessy - Milner properties for weakly extended PRS |
| Authors: | Mojmír Křetínský, Vojtěch Řehák, Jan Strejček |
| Further information | |
|---|---|
| Citation: | KŘETÍNSKÝ, Mojmír - ŘEHÁK, Vojtěch - STREJČEK, Jan. 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. ISBN 3-540-30495-9, pp. 213-224. 2005, Hyderabad, India. |
| Original language: | English |
| Field: | Informatika |
| Type: | Article in Proceedings |
| Keywords: | process rewrite systems; state extension; infinite-state; (un)decidability; HM logic; reachability |
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.
Related projects:
- Verification of infinite-state systems
- Techniques for automatic verification and validation of software nad hardware systems
- Institute for Theoretical Computer Science
- Highly Parallel and Distributed Computing Systems
