zbMATH — the first resource for mathematics

Results on the propositional \(\mu\)-calculus. (English) Zbl 0553.03007
In this paper we define and study a propositional \(\mu\)-calculus \(L\mu\), which consists essentially of propositional modal logic with a least fixpoint operator. \(L\mu\) is syntactically simpler yet strictly more expressive than Propositional Dynamic Logic (PDL). For a restricted version we give an exponential-time decision procedure, small model property, and complete deductive system, thereby subsuming the corresponding results for PDL.

03B45 Modal logic (including the logic of norms)
68Q65 Abstract data types; algebraic specification
Full Text: DOI
[1] De Bakker, J.W., Mathematical theory of program correctness, (1980), Prentice-Hall Englewood Cliffs, NJ
[2] De Bakker, J.W.; De Roever, W., A calculus for recursive program schemes, (), 167-196 · Zbl 0238.68006
[3] Chandra, A.; Kozen, D.; Stockmeyer, L., Alternation, J. assoc. comput. Mach., 28, 1, 114-133, (1981) · Zbl 0473.68043
[4] Emerson, E.A.; Clarke, E.M., Characterizing correctness properties of parallel programs using fixpoints, (), 169-181 · Zbl 0456.68016
[5] Emerson, E.A.; Clarke, E.M., Design and synthesis of synchronization skeletons using branching-time temporal logic, (), 52-71
[6] Fischer, M.; Ladner, R., Propositional dynamic logic of regular programs, J. comput. system sci., 18, 2, 194-211, (1979) · Zbl 0408.03014
[7] Hitchcock, P.; Park, D.M.R., Induction rules and termination proofs, (), 225-251
[8] Halpern, J.; Reif, J., The propositional dynamic logic of deterministic, well-structured programs (extended abstract), Proc. 22nd IEEE symp. on foundations of computer science, 322-334, (1981)
[9] Kozen, D., A representation theorem for models of ∗-free PDL, (), 352-362
[10] Kozen, D., On the duality of dynamic algebras and Kripke models, (), 1-11
[11] Kozen, D., On induction vs. ∗-continuity, (), 167-176
[12] D. Kozen, On the expressiveness of μ, Unpublished manuscript.
[13] D. Kozen, Small models for the propositional μ-calculus, Unpublished manuscript.
[14] Kozen, D., Results on the propositional μ-calculus, Proc. 9th internat. colloq. on automata, languages, and programming, 348-359, (1982)
[15] Kozen, D.; Parikh, R., An elementary proof of the completeness of PDL, Theoret. comput. sci., 14, 113-118, (1981) · Zbl 0451.03006
[16] Kozen, D.; Parikh, R., A decision procedure for the propositional μ-calculus, () · Zbl 0564.03012
[17] Park, D.M.R, Fixpoint induction and proof of program semantics, (), 59-78 · Zbl 0219.68007
[18] Pratt, V.R., A near optimal method for reasoning about action, J. comput. systems sci., 20, 231-254, (1980) · Zbl 0424.03010
[19] Pratt, V.R., A decidable μ-calculus, Proc. 22nd IEEE symp. on foundations of computer science, 421-427, (1981), (Preliminary Rept.)
[20] De Roever, W.P., Recursive program schemes: semantics and proof theory, () · Zbl 0344.68001
[21] Streett, R., Propositional dynamic logic of looping and converse, Proc. 13th ACM symp. on theory of computing, 375-383, (1981)
[22] Scott, D.; De Bakker, J.W., A theory of programs, (1969), IBM Vienna, Unpublished manuscript
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.