Reachability of Hennessy - Milner properties for weakly extended PRS

Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
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.