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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ben-Ari, M., Pnueli, A., Manna, Z.: The temporal logic of branching time. Acta Informatica 20(3), 207–226 (1983)
Burkart, O., Caucal, D., Moller, F., Steffen, B.: Verification on infinite structures. In: Handbook of Process Algebra, pp. 545–623. Elsevier, Amsterdam (2001)
Burkart, O., Caucal, D., Steffen, B.: Bisimulation collapse and the process taxonomy. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 247–262. Springer, Heidelberg (1996)
Bouajjani, A., Echahed, R., Habermehl, P.: On the verification problem of nonregular properties for nonregular processes. In: Proc. of LICS 1995, IEEE, Los Alamitos (1995)
Caucal, D.: On the regular structure of prefix rewriting. Theor. Comput. Sci. 106, 61–86 (1992)
Esparza, J., Kiehn, A.: On the model checking problem for branching time logics and basic parallel processes. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 353–366. Springer, Heidelberg (1995)
Esparza, J.: On the decidability of model checking for several mu-calculi and petri nets. In: Tison, S. (ed.) CAAP 1994. LNCS, vol. 787, pp. 115–129. Springer, Heidelberg (1994)
Esparza, J.: Decidability of model checking for infinite-state concurrent systems. Acta Informatica 34(2), 85–107 (1997)
Esparza, J.: Grammars as processes. In: Brauer, W., Ehrig, H., Karhumäki, J., Salomaa, A. (eds.) Formal and Natural Computing. LNCS, vol. 2300, p. 277. Springer, Heidelberg (2002)
Hirshfeld, Y., Moller, F.: Pushdown automata, multiset automata, and petri nets. Theor. Comput. Sci. 256(1-2), 3–21 (2001)
Jančar, P.: Undecidability of bisimilarity for Petri nets and some related problems. Theor. Comput. Sci. 148(2), 281–301 (1995)
Jančar, P.: Strong bisimilarity on basic parallel processes is PSPACE complete. In: Proc. of 18th IEEE Symposium on Logic in Computer Science (LICS 2003), pp. 218–227. IEEE Computer Society Press, Los Alamitos (2003)
Jančar, P., Kučera, A., Mayr, R.: Deciding bisimulation-like equivalences with finite-state processes. Theor. Comput. Sci. 258, 409–433 (2001)
Jancar, P., Moller, F.: Checking regular properties of petri nets. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 348–362. Springer, Heidelberg (1995)
Kučera, A., Jančar, P.: Equivalence-checking with infinite-state systems: Techniques and results. In: Grosky, W.I., Plášil, F. (eds.) SOFSEM 2002. LNCS, vol. 2540, pp. 41–73. Springer, Heidelberg (2002)
Křetínský, M., Řehák, V., Strejček, J.: Extended process rewrite systems: Expressiveness and reachability. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 355–370. Springer, Heidelberg (2004)
Křetínský, M., Řehák, V., Strejček, J.: On extensions of process rewrite systems: Rewrite systems with weak finite-state unit. In: Proceedings of INFINITY 2003. ENTCS, vol. 98, pp. 75–88. Elsevier, Amsterdam (2004)
Kučera, A., Schnoebelen, P.: A general approach to comparing infinite state systems with their finite-state specifications. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 371–386. Springer, Heidelberg (2004)
Mayr, R.: Decidability and Complexity of Model Checking Problems for Infinite-State Systems. Ph.D thesis, Technische UniversitätMünchen (1998)
Mayr, R.: Process rewrite systems. Information and Computation 156(1), 264–286 (2000)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Moller, F.: Infinite results. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 195–216. Springer, Heidelberg (1996)
Mayr, R., Rusinowitch, M.: Reachability is decidable for ground AC rewrite systems. In: Proceedings of INFINITY 1998 workshop (1998)
Muller, D., Schupp, P.: The theory of ends, pushdown automata, and second-order logic. Theor. Comput. Sci. 37, 51–75 (1985)
Muller, D., Saoudi, A., Schupp, P.: Alternating automata, the weak monadic theory of trees and its complexity. Theor. Comput. Sci. 97(1– 2), 233–244 (1992)
Srba, J.: Roadmap of infinite results. EATCS Bulletin (78), 163–175 (2002), http://www.brics.dk/~srba/roadmap/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Křetínský, M., Řehák, V., Strejček, J. (2005). Reachability of Hennessy-Milner Properties for Weakly Extended PRS. In: Sarukkai, S., Sen, S. (eds) FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2005. Lecture Notes in Computer Science, vol 3821. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11590156_17
Download citation
DOI: https://doi.org/10.1007/11590156_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-30495-1
Online ISBN: 978-3-540-32419-5
eBook Packages: Computer ScienceComputer Science (R0)