Reachability of Hennessy-Milner Properties for Weakly Extended PRS

1. Ben-Ari, M., Pnueli, A., Manna, Z.: The temporal logic of branching time. Acta Informatica 20(3), 207–226 (1983)

   Article  MATH  MathSciNet  Google Scholar 

2. Burkart, O., Caucal, D., Moller, F., Steffen, B.: Verification on infinite structures. In: Handbook of Process Algebra, pp. 545–623. Elsevier, Amsterdam (2001)

   Chapter  Google Scholar 

3. 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)

   Google Scholar 

4. 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)

   Google Scholar 

5. Caucal, D.: On the regular structure of prefix rewriting. Theor. Comput. Sci. 106, 61–86 (1992)

   Article  MathSciNet  Google Scholar 

6. 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)

   Google Scholar 

7. 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)

   Chapter  Google Scholar 

8. Esparza, J.: Decidability of model checking for infinite-state concurrent systems. Acta Informatica 34(2), 85–107 (1997)

   Article  MathSciNet  Google Scholar 

9. 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)

   Chapter  Google Scholar 

10. Hirshfeld, Y., Moller, F.: Pushdown automata, multiset automata, and petri nets. Theor. Comput. Sci. 256(1-2), 3–21 (2001)

    Article  MATH  MathSciNet  Google Scholar 

11. Jančar, P.: Undecidability of bisimilarity for Petri nets and some related problems. Theor. Comput. Sci. 148(2), 281–301 (1995)

    Article  MATH  Google Scholar 

12. 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)

    Google Scholar 

13. Jančar, P., Kučera, A., Mayr, R.: Deciding bisimulation-like equivalences with finite-state processes. Theor. Comput. Sci. 258, 409–433 (2001)

    Article  MATH  Google Scholar 

14. 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)

    Google Scholar 

15. 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)

    Chapter  Google Scholar 

16. 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)

    Chapter  Google Scholar 

17. 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)

    Google Scholar 

18. 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)

    Chapter  Google Scholar 

19. Mayr, R.: Decidability and Complexity of Model Checking Problems for Infinite-State Systems. Ph.D thesis, Technische UniversitätMünchen (1998)

    Google Scholar 

20. Mayr, R.: Process rewrite systems. Information and Computation 156(1), 264–286 (2000)

    Article  MATH  MathSciNet  Google Scholar 

21. Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)

    MATH  Google Scholar 

22. Moller, F.: Infinite results. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 195–216. Springer, Heidelberg (1996)

    Google Scholar 

23. Mayr, R., Rusinowitch, M.: Reachability is decidable for ground AC rewrite systems. In: Proceedings of INFINITY 1998 workshop (1998)

    Google Scholar 

24. Muller, D., Schupp, P.: The theory of ends, pushdown automata, and second-order logic. Theor. Comput. Sci. 37, 51–75 (1985)

    Article  MATH  MathSciNet  Google Scholar 

25. 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)

    Article  MATH  MathSciNet  Google Scholar 

26. Srba, J.: Roadmap of infinite results. EATCS Bulletin (78), 163–175 (2002), http://www.brics.dk/~srba/roadmap/

Download references