On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic

1. R. Alur, D. Peled, and W. Penczek. Model-checking of causality properties. In LICS '95, pages 90–100, 1995.

   Google Scholar 

2. A. Amir. Separation in nonlinear time models. Information and Computation, 66:177–203, 1985.

   Google Scholar 

3. A. Arnold. Finite Transition Systems. Masson, Prentice-Hall, 1994.

   Google Scholar 

4. B. Banieqbal and H. Barringer. Temporal logic with fixed points. volume 398 of LNCS, pages 62–74. Springer-Verlag, 1989.

   Google Scholar 

5. J. Benthem. Languages in Action: Categories, Lambdas and Dynamic Logic, volume 130 of Studies in Logic. North-Holland, 1991.

   Google Scholar 

6. J. Benthem and J. Bergstra. Logic of transition systems. Report P9308, Programming Research Group, University of Amsterdam, 1993.

   Google Scholar 

7. A. Bouajjani, R. Echahed, and P. Habermehl. On verification problem of nonregular properties of nonregular processes. In LICS '95, pages 123–133, 1995.

   Google Scholar 

8. I. Castellani. Bisimulations and abstraction homomorphisms. Journal of Computer and System Sciences, 34:210–235, 1987.

   Google Scholar 

9. M. Dam. CTL^* and ECTL^* as a fragments of the modal Μ-calculus. In CAAP'92, volume 581 of LNCS, pages 145–165, 1992.

   Google Scholar 

10. E. A. Emerson. Temporal and modal logic. In J. Leeuven, editor, Handbook of Theoretical Computer Science Vol.B, pages 995–1072. Elsevier, 1990.

    Google Scholar 

11. E. A. Emerson and C. Jutla. Tree automata, mu-calculus and determinacy. In Proc. FOCS 91, 1991.

    Google Scholar 

12. J. Esparza and A. Kiehn. On the model checking problem for branching time logics and basic parallel processes. In CAV '95, volume 939 of LNCS, pages 353–366, 1995.

    Google Scholar 

13. A. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. On the temporal analysis of fairness. In 7th Ann. ACM Symp. on Principles of Programming Languages, pages 163–173, 1980.

    Google Scholar 

14. D. Gabbay. Expressive functional completeness in tense logic. In Aspects of Philosophical Logic, pages 91–117. Reidel, 1981.

    Google Scholar 

15. H. Gaifman. On local and non-local properties. In Herbrand Symposium, Logic Colloquium'81, pages 105–135. North-Holland, 1982.

    Google Scholar 

16. T. Hafer and W. Thomas. Computation tree logic CTL^* and path quantifiers in the monadic theory of the binary tree. In 14th Internat. Coll. on Automata, Languages and Programming, volume 267 of LNCS, pages 269–279, 1987.

    Google Scholar 

17. D. Harel and D. Raz. Deciding properties of nonregular programs. SIAM J. Comput, 22:857–874, 1993.

    Google Scholar 

18. D. Janin. Propriérés logiques du non-déterminisme et Μ-calcul modal. PhD thesis, LaBRI — Université de Bordeaux I, 1995. Available from http://www.labri.u-bordeaux.fr/∼janin.

    Google Scholar 

19. D. Janin and I. Walukiewicz. Automata for the Μ-calculus and related results. In MFCS '95, volume 969 of LNCS, pages 552–562, 1995.

    Google Scholar 

20. H. Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, University of California, 1968.

    Google Scholar 

21. D. Kozen. Results on the prepositional mu-calculus. Theoretical Computer Science, 27:333–354, 1983.

    Google Scholar 

22. R. Milner. Communication and Concurrency. Prentice-Hall, Englewood Clifs, 1989.

    Google Scholar 

23. D. Muller and P. Schupp. Alternating automata on infinite trees. Theoretical Computer Science, 54:267–276, 1987.

    Google Scholar 

24. D. Niwiński. Fixed points vs. infinite generation. In LICS '88, pages 402–409, 1988.

    Google Scholar 

25. G. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Aarhus University, 1981.

    Google Scholar 

26. A. Pnueli. The temporal logic of programs. In 18th Symposium on Foundations of Computer Science, pages 46–57, 1977.

    Google Scholar 

27. M. Rabin. Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc., 141:1–35, 1969.

    Google Scholar 

28. C. S. Stirling. Modal and temporal logics. In S.Abramsky, D.Gabbay, and T.Maibaum, editors, Handbook of Logic in Comuter Science, pages 477–563. Oxford University Press, 1991.

    Google Scholar 

29. P. Thiagarajan. A trace based extension of linear time temporal logic. In LICS, pages 438–447, 1994.

    Google Scholar 

30. R. van Glabbeek. The linear time — branching time spectrum. In CONCUR'90, volume 458 of LNCS, pages 278–297, 1990.

    Google Scholar 

31. I. Walukiewicz. Monadic second order logic on tree-like structures. In STACS '96, volume 1046 of LNCS, pages 401–414, 1996.

    Google Scholar 

32. G. Winskel and M. Nielsen. Handbook of Logic in Computer Science, volume 4, Chapter Models for Concurrency, pages 1–148. Clarendon Press-Oxford, 1995.

    Google Scholar 

Download references