Publication details

Reachability of Hennessy - Milner properties for weakly extended PRS

Investor logo
Authors

KŘETÍNSKÝ Mojmír ŘEHÁK Vojtěch STREJČEK Jan

Year of publication 2005
Type Article in Proceedings
Conference FSTTCS 2005: 25th International Conference on Foundations of Software Technology and Theoretical Computer Science, 25th International Conference
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords process rewrite systems; state extension; infinite-state; (un)decidability; HM logic; reachability
Description 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:

You are running an old browser version. We recommend updating your browser to its latest version.

More info