The propositional mu-calculus is elementary

• deBakker, J., and deRoever, W. P. (1973), A Calculus for Recursive Program Schemes, in "First International Colloquium on Automata, Languages, and Programming", 167–196.

  Google Scholar 

• deRoever, W. P. (1974), "Recursive Program Schemes: Semantics and Proof Theory", Ph. D. thesis, Free University, Amsterdam.

  Google Scholar 

• Emerson, E. A., and Clarke, E. C. (1980), Characterizing Correctness Properties of Parallel Programs Using Fixpoints, in "Seventh International Colloquium on Automata, Languages, and Programming", 169–181.

  Google Scholar 

• Fischer, M. J., and Ladner, R. E. (1979), Propositional Dynamic Logic of Regular Programs, Journal of Computer System Science 18, 194–211.

  Google Scholar 

• Hitchcock, P., and Park, D. M. R. (1973), Induction Rules and Termination Proofs, in "First International Colloquium on Automata, Languages, and Programming", 225–251.

  Google Scholar 

• Hossley, R., and Rackoff, C. W. (1972), The Emptiness Problem for Automata on Infinite Trees, in "Thirteenth IEEE Symposium on Switching and Automata Theory", 121–124.

  Google Scholar 

• Kfoury, A. J., and Park, D. M. R. (1975), On Termination of Program Schemes, Information and Control 29, 243–251.

  Google Scholar 

• Kozen, D. (1982), Results on the Propositional Mu-Calculus, in "Ninth International Colloquium on Automata, Languages, and Programming", 348–359.

  Google Scholar 

• Kozen, D., and Parikh, R. J. (1983), A Decision Procedure for the Propositional Mu-Calculus, to appear in "Second Workshop on Logics of Programs".

  Google Scholar 

• Meyer, A. R. (1974), Weak Monadic Second Order Theory of Successor is not Elementary Recursive, Boston Logic Colloquium, Springer-Verlag Lecture Notes in Mathematics 453.

  Google Scholar 

• Parikh, R. J. (1979), A Decidability Result for a Second Order Process Logic, in "Nineteenth IEEE Symposium on the Foundations of Computing", 177–183.

  Google Scholar 

• Parikh, R. J. (1983a), Cake Cutting, Dynamic Logic, Games, and Fairness, to appear in "Second Workshop on Logics of Programs".

  Google Scholar 

• Parikh, R. J. (1983b), Propositional Game Logic, to appear in "Twenty-third IEEE Symposium on the Foundations of Computer Science".

  Google Scholar 

• Park, D. M. R. (1970), Fixpoint Induction and Proof of Program Semantics, Machine Intelligence 5, Edinburgh University Press.

  Google Scholar 

• Park, D. M. R. (1976), Finiteness is Mu-Ineffable, Theoretical Computer Science 3, 173–181.

  Google Scholar 

• Pratt, V. R. (1982), A Decidable Mu-Calculus: Preliminary Report, in "Twenty-second IEEE Symposium on the Foundations of Computer Science", 421–427.

  Google Scholar 

• Rabin, M. O. (1969), Decidability of Second Order Theories and Automata on Infinite Trees", Transactions of the American Mathematical Society 141, 1–35.

  Google Scholar 

• Streett, R. S. (1981), "Propositional Dynamic Logic of Looping and Converse", MIT LCS Technical Report TR-263.

  Google Scholar 

• Streett, R. S. (1982), Propositional Dynamic Logic of Looping and Converse is Elementarily Decidable, Information and Control 54, 121–141.

  Google Scholar 

• Vardi, M., and Wolper, P. (1984), Automata Theoretic Techniques for Modal Logics of Programs, to appear in "Sixteenth ACM Symposium on the Theory of Computing".

  Google Scholar 

Download references