An automata theoretic decision procedure for the propositional mu- calculus. (English) Zbl 0671.03023

A decision procedure of elementary complexity is presented for the propositional mu-calculus. This calculus was introduced by D. Kozen as a powerful generalization of propositional dynamic logic, in which, in particular, Streett’s infinite repeating construction \(\Delta\) \(a\) can be expressed. The proof is based on using tree automata and strengthens a result by D. Kozen and R. Parikh on (non-elementary) decidability of the mu-calculus obtained by reduction to the monadic second order theory of many successors.
Reviewer: M.K.Valiev


03B70 Logic in computer science
68N01 General topics in the theory of software
03B25 Decidability of theories and sets of sentences
68Q65 Abstract data types; algebraic specification
03D05 Automata and formal grammars in connection with logical questions
Full Text: DOI


[1] de Bakker, J.; de Roever, W. P., A calculus for recursive program schemes, (First International Colloquium on Automata, Languages, and Programming, (1973)), 167-196 · Zbl 0262.68004
[2] de Roever, W. P., Recursive program schemes: semantics and proof theory, (Ph.D. thesis, (1974), Free University Amsterdam) · Zbl 0302.68019
[3] Emerson, E. A.; Clarke, E. M., Characterizing correctness properties of parallel programs using fixpoints, (Seventh International Colloquium on Automata, Languages and Programming, (1980)), 169-181 · Zbl 0456.68016
[4] Fischer, M. J.; Ladner, R. E., Propositional dynamic logic of regular programs, J. Comput. System Sci., 18, 194-211, (1979) · Zbl 0408.03014
[5] Harel, D., First-order dynamic logic, (Lecture Notes in Computer Science, Vol. 68, (1979), Springer-Verlag) · Zbl 0403.03024
[6] Hitchcock, P.; Park, D. M.R., Induction rules and termination proofs, (First International Colloquium on Automata, Languages, and Programming, (1973)), 225-251
[7] Hossley, R.; Rackoff, C. W., The emptiness problem for automata on infinite trees, (Thirteenth IEEE Symposium on Switching and Automata Theory, (1972)), 121-124
[8] Kfoury, A. J.; Park, D. M.R., On termination of program schemes, Inform. and Control, 29, 243-251, (1975) · Zbl 0329.68015
[9] Kozen, D., Results on the propositional mu-calculus, (Ninth International Colloquium on Automata, Languages, and Programming, (1982)), 348-359
[10] Kozen, D.; Parikh, R. J., A decision procedure for the propositional mu-calculus, (Second Workshop on Logics of Programs, (1983))
[11] Kripke, S. A., Semantical considerations on model logics, Acta Philos. Fennica., (1963) · Zbl 0131.00602
[12] McNaughton, R., Testing and generating infinite sequences by a finite automaton, Inform. and Control, 9, 521-530, (1966) · Zbl 0212.33902
[13] Meyer, A. R., Weak monadic second order theory of successor is not elementary recursive, (“Boston Logic Colloquium,” Lecture Notes in Mathematics, Vol. 453, (1974), Springer-Verlag New York/Berlin)
[14] Parikh, R. J., A decidability result for a second order process logic, (Nineteenth IEEE Symposium on the Foundations of Computer Science, (1979)), 177-183
[15] Parikh, R. J., Cake cutting, dynamic logic, games, and fairness, (Second Workshop on Logics of Programs, (1983))
[16] Parikh, R. J., Propositional game logic, (Twenty-third IEEE Symposium on the Foundations of Computer Science, (1983))
[17] Park, D. M.R., Fixpoint induction and proof of program semantics, (Machine Intelligence, Vol. 5, (1970), Edinburgh Univ. Press Edinburgh)
[18] Park, D. M.R., Finiteness is mu-ineffable, Theoret. Comput. Sci., 3, 173-181, (1976) · Zbl 0353.02027
[19] Pratt, V. R., Semantical considerations on floyd-Hoare logic, (Seventeenth IEEE Symposium on Foundations of Computer Science, (1976)), 109-121
[20] Pratt, V. R., A decidable mu-calculus: preliminary report, (Twenty-second IEEE Symposium on the Foundations of Computer Science, (1982)), 421-427
[21] Rabin, M. O., Decidability of second order theories and automata on infinite trees, Trans. Amer. Math. Soc., 141, 1-35, (1969) · Zbl 0221.02031
[22] Streett, R. S., (Propositional Dynamic Logic of Looping and Converse, (1981), MIT LCS), Technical Report TR-263
[23] Streett, R. S., Propositional dynamic logic of looping and converse is elementarily decidable, Inform. and Control, 54, 121-141, (1982) · Zbl 0515.68062
[24] Streett, R. S.; Emerson, E. A., The propositional mu-calculus is elementary, (Eleventh International Colloquium on Automato, Languages, and Programming, Lecture Notes in Computer Science, Vol. 172, (1984), Springer-Verlag New York/Berlin), 465-472 · Zbl 0556.68005
[25] Vardi, M. (1984), private communication.
[26] Vardi, M.; Wolper, P., Automata theoretic techniques for modal logics of programs, (Sixteenth ACM Symposium on the Theory of Computing, (1984))
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.