{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,13]],"date-time":"2026-03-13T02:42:43Z","timestamp":1773369763326,"version":"3.50.1"},"reference-count":70,"publisher":"Elsevier","isbn-type":[{"value":"9780444516909","type":"print"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1016\/s1570-2464(07)80015-2","type":"book-chapter","created":{"date-parts":[[2007,10,4]],"date-time":"2007-10-04T09:38:50Z","timestamp":1191490730000},"page":"721-756","source":"Crossref","is-referenced-by-count":94,"title":["12 Modal mu-calculi"],"prefix":"10.1016","member":"78","reference":[{"key":"10.1016\/S1570-2464(07)80015-2_bib1","doi-asserted-by":"crossref","DOI":"10.7146\/dpb.v22i445.6762","article-title":"Verification of Temporal Properties of Concurrent Systems","author":"Andersen","year":"1993"},{"issue":"4\/5","key":"10.1016\/S1570-2464(07)80015-2_bib2","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1051\/ita:1999121","article-title":"The\u03bc-calculus alternation hierarchy is strict on binary trees","volume":"33","author":"Arnold","year":"1999","journal-title":"Theoretical Informatics and Applications"},{"key":"10.1016\/S1570-2464(07)80015-2_bib3","first-page":"451","article-title":"Fixed point characterization of Biichi automata on infinite trees","volume":"26","author":"Arnold","year":"1990","journal-title":"J. Inf. Process. Cybern. EIK"},{"key":"10.1016\/S1570-2464(07)80015-2_bib4","series-title":"Studies in Logic","article-title":"Rudiments of \u03bc-Calculus","author":"Arnold","year":"2001"},{"key":"10.1016\/S1570-2464(07)80015-2_bib5","first-page":"304","article-title":"Efficient model checking via the equational mu-calculus","author":"Bhat","year":"1996"},{"key":"10.1016\/S1570-2464(07)80015-2_bib6","series-title":"Verifying Temporal Properties of Systems","author":"Bradfield","year":"1991"},{"issue":"195","key":"10.1016\/S1570-2464(07)80015-2_bib7","first-page":"4","article-title":"The modal mu-calculus alternation hierarchy is strict","author":"Bradfield","year":"1996","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/S1570-2464(07)80015-2_bib8","first-page":"39","article-title":"Simplifying the modal mu-calculus alternation hierarchy","volume":"1373","author":"Bradfield","year":"1998"},{"key":"10.1016\/S1570-2464(07)80015-2_bib9","first-page":"22","article-title":"Alternation on the binary tree","author":"Bradfield","year":"1998"},{"issue":"4\/5","key":"10.1016\/S1570-2464(07)80015-2_bib10","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1051\/ita:1999122","article-title":"Fixpoints in arithmetic, transition systems and trees","volume":"33","author":"Bradfield","year":"1999","journal-title":"Theoretical Informatics and Applications"},{"key":"10.1016\/S1570-2464(07)80015-2_bib11","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/0304-3975(92)90183-G","article-title":"Local model checking for infinite state spaces","volume":"96","author":"Bradfield","year":"1992","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S1570-2464(07)80015-2_bib12","series-title":"Logic, Methodology and Philosophy of Science","first-page":"1","article-title":"On a decision method in restricted second order arithmetic","author":"Biichi","year":"1962"},{"issue":"131","key":"10.1016\/S1570-2464(07)80015-2_bib13","first-page":"52","article-title":"Design and synthesis of synchronization skeletons using branching time temporal logic","author":"Clarke","year":"1981","journal-title":"LNCS"},{"key":"10.1016\/S1570-2464(07)80015-2_bib14","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","article-title":"Automatic verification of finite-state concurrent systems using temporal logic specifications","volume":"8","author":"Clarke","year":"1981","journal-title":"ACM Trans, on Programming Languages and Systems"},{"issue":"1","key":"10.1016\/S1570-2464(07)80015-2_bib15","doi-asserted-by":"crossref","first-page":"310","DOI":"10.2307\/2586539","article-title":"Logical questions concerning the \u03bc-calculus: interpolation, Lyndon and Los-Tarski","volume":"65","author":"d'Agostino","year":"2000","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S1570-2464(07)80015-2_bib16","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/0304-3975(94)90269-0","article-title":"CTL* and ECTL* as fragments of the modal mu-calculus","volume":"126","author":"Dam","year":"1994","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"10.1016\/S1570-2464(07)80015-2_bib17","doi-asserted-by":"crossref","DOI":"10.1145\/976706.976710","article-title":"Inflationary fixed points in modal logics","volume":"5","author":"Dawar","year":"2004","journal-title":"ACM Trans, on Computational Logic"},{"key":"10.1016\/S1570-2464(07)80015-2_bib18","series-title":"Finite Model Theory","author":"Ebbinghaus","year":"1999"},{"key":"10.1016\/S1570-2464(07)80015-2_bib19","article-title":"Temporal and modal logic","volume":"Volume B.","author":"Emerson","year":"1990"},{"key":"10.1016\/S1570-2464(07)80015-2_bib20","first-page":"169","article-title":"Characterizing correctness properties of parallel programs using fixpoints","volume":"85","author":"Emerson","year":"1980","journal-title":"Procs ICALP '80 LNCS"},{"key":"10.1016\/S1570-2464(07)80015-2_bib21","series-title":"Proc. 29th IEEE FOCS","first-page":"328","article-title":"The complexity of tree automata and logics of programs","author":"Emerson","year":"1988"},{"key":"10.1016\/S1570-2464(07)80015-2_bib22","series-title":"Proc. 32nd IEEE FOCS","first-page":"368","article-title":"Tree automata, mu-calculus and determinacy","author":"Emerson","year":"1991"},{"key":"10.1016\/S1570-2464(07)80015-2_bib23","series-title":"Proc. 1st IEEE LICS","first-page":"267","article-title":"Efficient model checking in fragments of the propositional mu-calculus","author":"Emerson","year":"1986"},{"key":"10.1016\/S1570-2464(07)80015-2_bib24","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","article-title":"Propositional dynamic logic of regular programs","volume":"18","author":"Fischer","year":"1979","journal-title":"J. Computer and System Science"},{"key":"10.1016\/S1570-2464(07)80015-2_bib25","series-title":"Mathematical Aspects of Computer Science","first-page":"19","article-title":"Assigning meanings to programs","author":"Floyd","year":"1967"},{"key":"10.1016\/S1570-2464(07)80015-2_bib26","doi-asserted-by":"crossref","first-page":"1719","DOI":"10.2307\/2586808","article-title":"On the restraining power of guards","volume":"64","author":"Gr\u00e4del","year":"1999","journal-title":"J. Symbol. Logic"},{"key":"10.1016\/S1570-2464(07)80015-2_bib27","series-title":"Automata, Logics, and Infinite Games, LNCS","first-page":"2500","year":"2002"},{"key":"10.1016\/S1570-2464(07)80015-2_bib28","article-title":"Guarded fixed point logic","volume":"45","author":"Gr\u00e4del","year":"1999","journal-title":"Proc. 14th LICS"},{"key":"10.1016\/S1570-2464(07)80015-2_bib29","first-page":"60","article-title":"Trees, automata and games","author":"Gurevich","year":"1982","journal-title":"Procs 14th ACM STOC"},{"key":"10.1016\/S1570-2464(07)80015-2_bib30","first-page":"295","article-title":"On observing nondeterminism and concurrency","volume":"85","author":"Hennessy","year":"1980","journal-title":"Procs ICALP '80 LNCS"},{"issue":"969","key":"10.1016\/S1570-2464(07)80015-2_bib31","first-page":"552","article-title":"Automata for the \u03bc-calculus and related results","author":"Janin","year":"1995","journal-title":"Proc. MFCS '95 LNCS"},{"key":"10.1016\/S1570-2464(07)80015-2_bib32","first-page":"263","article-title":"On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic","volume":"1119","author":"Janin","year":"1996","journal-title":"Proc. CONCUR '96 LNCS"},{"key":"10.1016\/S1570-2464(07)80015-2_bib33","article-title":"Using Automata to Characterise Fixpoint Temporal Logics","author":"Kaivola","year":"1997"},{"key":"10.1016\/S1570-2464(07)80015-2_bib34","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","article-title":"Results on the propositional mu-calculus","volume":"27","author":"Kozen","year":"1983","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S1570-2464(07)80015-2_bib35","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/BF00370554","article-title":"A finite model theorem for the propositional \u03bc-calculus","volume":"47","author":"Kozen","year":"1988","journal-title":"Studia Logica"},{"key":"10.1016\/S1570-2464(07)80015-2_bib36","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/0304-3975(81)90019-0","article-title":"An elementary proof of the completeness of PDL","volume":"14","author":"Kozen","year":"1981","journal-title":"Theoret. Comput. Sci."},{"issue":"164","key":"10.1016\/S1570-2464(07)80015-2_bib37","first-page":"313","article-title":"A decision procedure for the propositional \u03bc-calculus","author":"Kozen","year":"1984","journal-title":"LNCS"},{"issue":"1\u20133","key":"10.1016\/S1570-2464(07)80015-2_bib38","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/j.apal.2004.02.001","article-title":"Expressive equivalence of least and inflationary fixed-point logic","volume":"130","author":"Kreutzer","year":"2004","journal-title":"Annals of Pure and Applied Logic"},{"issue":"2","key":"10.1016\/S1570-2464(07)80015-2_bib39","doi-asserted-by":"crossref","first-page":"312","DOI":"10.1145\/333979.333987","article-title":"An automata-theoretic approach to branching-time model checking","volume":"42","author":"Kupferman","year":"2000","journal-title":"J. ACM"},{"issue":"2556","key":"10.1016\/S1570-2464(07)80015-2_bib40","first-page":"241","article-title":"Deciding the first level of the \u03bc-calculus alternation hierarchy","author":"K\u00fcsters","year":"2002","journal-title":"Proc. FSTTCS 2002"},{"key":"10.1016\/S1570-2464(07)80015-2_bib41","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1109\/TSE.1977.229904","article-title":"Proving the correctness of multiprocess programs","volume":"2","author":"Lamport","year":"1977","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/S1570-2464(07)80015-2_bib42","first-page":"87","article-title":"A hierarchy theorem for the mu-calculus","volume":"1099","author":"Lenzi","year":"1996"},{"key":"10.1016\/S1570-2464(07)80015-2_bib43","first-page":"5","article-title":"Fully local and efficient evaluation of alternating fixed points","volume":"1384","author":"Liu","year":"1998"},{"key":"10.1016\/S1570-2464(07)80015-2_bib44","article-title":"Modal logic and the two-variable fragment","volume":"247","author":"Lutz","year":"2001","journal-title":"Proc. CSL'01 (LNCS 2142)"},{"key":"10.1016\/S1570-2464(07)80015-2_bib45","article-title":"Verification of Modal Properties Using Boolean Equation Systems","author":"Mader","year":"1997"},{"issue":"6","key":"10.1016\/S1570-2464(07)80015-2_bib46","first-page":"109","article-title":"Absence of interpolation and of Beth's property in temporal logics with 'the next' operation","volume":"32","author":"Maksimova","year":"1991","journal-title":"Siberian Mathematical Journal"},{"key":"10.1016\/S1570-2464(07)80015-2_bib47","first-page":"201","article-title":"Formalization of properties of recursively defined functions","author":"Manna","year":"1969","journal-title":"Proc. ACM STOC"},{"key":"10.1016\/S1570-2464(07)80015-2_bib48","first-page":"141","article-title":"How to cook a temporal proof system for your pet language","author":"Manna","year":"1983","journal-title":"Proc. 10th ACM POPL"},{"key":"10.1016\/S1570-2464(07)80015-2_bib49","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","volume":"92","author":"Milner","year":"1980","journal-title":"A Calculus of Communicating Systems. LNCS"},{"key":"10.1016\/S1570-2464(07)80015-2_bib50","series-title":"Communication and Concurrency","author":"Milner","year":"1989"},{"key":"10.1016\/S1570-2464(07)80015-2_bib51","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1007\/3-540-16066-3_15","article-title":"Regular expressions for infinite trees and a standard form of automata","volume":"208","author":"Mostowski","year":"1984","journal-title":"Computa- tion Theory"},{"key":"10.1016\/S1570-2464(07)80015-2_bib52","first-page":"464","article-title":"On fixed point clones","volume":"226","author":"Niwinski","year":"1986"},{"key":"10.1016\/S1570-2464(07)80015-2_bib53","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1016\/S0304-3975(98)00314-4","article-title":"Bisimulation-invariant Ptime and higher-dimensional mu-calculus","volume":"224","author":"Otto","year":"1999","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S1570-2464(07)80015-2_bib54","first-page":"531","article-title":"Eliminating recursion in the mu-calculus","volume":"1563","author":"Otto","year":"1999"},{"key":"10.1016\/S1570-2464(07)80015-2_bib55","first-page":"59","article-title":"Fixpoint induction and proofs of program properties","volume":"5","author":"D","year":"1969"},{"key":"10.1016\/S1570-2464(07)80015-2_bib56","first-page":"109","article-title":"Semantical considerations of Floyd-Hoare logic","author":"Pratt","year":"1976","journal-title":"Proc. 16th IEEE FOCS"},{"key":"10.1016\/S1570-2464(07)80015-2_bib57","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0022-0000(80)90061-6","article-title":"A near-optimal method for reasoning about action","volume":"20","author":"Pratt","year":"1980","journal-title":"Journal of Comput. and System Sciences"},{"key":"10.1016\/S1570-2464(07)80015-2_bib58","first-page":"421","article-title":"A decidable mu-calculus","author":"Pratt","year":"1982"},{"key":"10.1016\/S1570-2464(07)80015-2_bib59","first-page":"1","article-title":"Decidability of second-order theories and automata on infinite trees","volume":"141","author":"Rabin","year":"1969","journal-title":"Transactions of American Mathematical Society"},{"key":"10.1016\/S1570-2464(07)80015-2_bib60","first-page":"1","article-title":"Local model checking games","volume":"962","author":"Stirling","year":"1995","journal-title":"Proc. Concur '95 LNCS"},{"key":"10.1016\/S1570-2464(07)80015-2_bib61","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1007\/3-540-52148-8_14","article-title":"CCS, liveness, and local model checking in the linear time mu-calculus","volume":"407","author":"Stirling","year":"1990","journal-title":"Proc. First International Workshop on Automatic Verification Methods for Finite State Systems, LNCS"},{"key":"10.1016\/S1570-2464(07)80015-2_bib62","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1016\/0304-3975(90)90110-4","article-title":"Local model checking in the modal mu-calculus","volume":"89","author":"Stirling","year":"1991","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/S1570-2464(07)80015-2_bib63","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1016\/0890-5401(89)90031-X","article-title":"An automata theoretic decision procedure for the propositional mu-calculus","volume":"81","author":"Streett","year":"1989","journal-title":"Information and Computation"},{"key":"10.1016\/S1570-2464(07)80015-2_bib64","first-page":"375","article-title":"Propositional dynamic logic of looping and converse","author":"Streett","year":"1981","journal-title":"Proc. 13th ACM STOC"},{"key":"10.1016\/S1570-2464(07)80015-2_bib65","first-page":"389","article-title":"Languages, Automata, and Logic","volume":"Vol. III","author":"Thomas","year":"1998"},{"key":"10.1016\/S1570-2464(07)80015-2_bib66","first-page":"250","article-title":"A temporal fixpoint calculus","author":"Vardi","year":"1988"},{"key":"10.1016\/S1570-2464(07)80015-2_bib67","series-title":"Descriptive Complexity and Finite Models","article-title":"Why is modal logic so robustly decidable?","author":"Vardi","year":"1997"},{"key":"10.1016\/S1570-2464(07)80015-2_bib68","first-page":"628","article-title":"Reasoning about the past with two-way automata","volume":"1443","author":"Vardi","year":"1998"},{"key":"10.1016\/S1570-2464(07)80015-2_bib69","doi-asserted-by":"crossref","first-page":"501","DOI":"10.1007\/3-540-12896-4_383","article-title":"Yet another process logic","volume":"164","author":"Vardi","year":"1983","journal-title":"Logics of Programs LNCS"},{"key":"10.1016\/S1570-2464(07)80015-2_bib70","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1006\/inco.1999.2836","article-title":"Completeness of Kozen's axiomatisation of the propositional \u03bc-calculus","volume":"157","author":"Walukiewicz","year":"2000","journal-title":"Information and Computation"}],"container-title":["Studies in Logic and Practical Reasoning","Handbook of Modal Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1570246407800152?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1570246407800152?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T23:18:01Z","timestamp":1761607081000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1570246407800152"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9780444516909"],"references-count":70,"URL":"https:\/\/doi.org\/10.1016\/s1570-2464(07)80015-2","relation":{},"ISSN":["1570-2464"],"issn-type":[{"value":"1570-2464","type":"print"}],"subject":[],"published":{"date-parts":[[2007]]}}}