{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:40:41Z","timestamp":1725550841684},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540008989"},{"type":"electronic","value":"9783540365778"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36577-x_5","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T17:12:04Z","timestamp":1269882724000},"page":"49-64","source":"Crossref","is-referenced-by-count":2,"title":["On the Universal and Existential Fragments of the \u03bc-Calculus"],"prefix":"10.1007","author":[{"given":"Thomas A.","family":"Henzinger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Orna","family":"Kupferman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"key":"5_CR1","series-title":"Lect Notes Comput Sci","first-page":"62","volume-title":"Temporal Logic in Specification","author":"B. Banieqbal","year":"1987","unstructured":"B. Banieqbal and H. Barringer. Temporal logic with fixed points. Temporal Logic in Specification, LNCS 398, pages 62\u201374. Springer-Verlag, 1987."},{"issue":"2","key":"5_CR2","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J. Burch","year":"1992","unstructured":"J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142\u2013170, June 1992.","journal-title":"Information and Computation"},{"key":"5_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logic of Programs","author":"E. Clarke","year":"1981","unstructured":"E. Clarke and E. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logic of Programs, LNCS 131, pages 52\u201371. Springer-Verlag, 1981."},{"issue":"2","key":"5_CR4","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. Clarke","year":"1986","unstructured":"E. Clarke, E. Emerson, and A. Sistla. Automatic verification of finite-state concurrent systems using temporal-logic specifications. ACM Trans. on Programming Languages and Systems, 8(2):244\u2013263, 1986.","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"5_CR5","unstructured":"E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999."},{"key":"5_CR6","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/BF01383878","volume":"2","author":"R. Cleaveland","year":"1993","unstructured":"R. Cleaveland and B. Steffen. A linear-time model-checking algorithm for the alternation-free modal \u03bc-calculus. Formal Methods in System Design, 2:121\u2013147, 1993.","journal-title":"Formal Methods in System Design"},{"key":"5_CR7","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/0304-3975(94)90269-0","volume":"126","author":"M. Dam","year":"1994","unstructured":"M. Dam. CTL. and ECTL. as fragments of the modal \u03bc-calculus. Theoretical Computer Science, 126:77\u201396, 1994.","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"5_CR8","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E. Emerson","year":"1986","unstructured":"E. Emerson and J. Halpern. Sometimes and not never revisited: On branching versus linear time. Journal of the ACM, 33(1):151\u2013178, 1986.","journal-title":"Journal of the ACM"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"E. Emerson and C. Jutla. The complexity of tree automata and logics of programs. In Proc. Foundations of Computer Science, pages 328\u2013337. IEEE Press, 1988.","DOI":"10.1109\/SFCS.1988.21949"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"E. Emerson and C. Jutla. Tree automata, \u03bc-calculus and determinacy. In Proc. Foundations of Computer Science, pages 368\u2013377. IEEE Press, 1991.","DOI":"10.1109\/SFCS.1991.185392"},{"key":"5_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1007\/3-540-56922-7_32","volume-title":"Computer Aided Verification","author":"E. Emerson","year":"1993","unstructured":"E. Emerson, C. Jutla, and A. Sistla. On model-checking for fragments of \u03bc-calculus. In Computer Aided Verification, LNCS 697, pages 385\u2013396. Springer-Verlag, 1993."},{"key":"5_CR12","unstructured":"E. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional \u03bc-calculus. In Proc. Logic in Computer Science, pages 267\u2013278. 1986."},{"key":"5_CR13","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M. Fischer","year":"1979","unstructured":"M. Fischer and R. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 18:194\u2013211, 1979.","journal-title":"Journal of Computer and System Sciences"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"R. Greenlaw, H. Hoover, and W. Ruzzo. Limits of Parallel Computation. Oxford University Press, 1995.","DOI":"10.1093\/oso\/9780195085914.001.0001"},{"issue":"3","key":"5_CR15","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"O. Grumberg and D.E. Long. Model checking and modular verification. ACM Trans. on Programming Languages and Systems, 16(3):843\u2013871, 1994.","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"5_CR16","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M. Hennessy","year":"1985","unstructured":"M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32:137\u2013161, 1985.","journal-title":"Journal of the ACM"},{"issue":"3","key":"5_CR17","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1016\/0022-0000(81)90039-8","volume":"22","author":"N. Immerman","year":"1981","unstructured":"N. Immerman. Number of quantifiers is better than number of tape cells. Journal of Computer and System Sciences, 22(3):384\u2013406, 1981.","journal-title":"Journal of Computer and System Sciences"},{"key":"5_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/3-540-61604-7_60","volume-title":"Concurrency Theory","author":"D. Janin","year":"1996","unstructured":"D. Janin and I. Walukiewicz. On the expressive completeness of the propositional \u03bc-calculus with respect to the monadic second-order logic. In Concurrency Theory, LNCS 1119, pages 263\u2013277. Springer-Verlag, 1996."},{"issue":"3","key":"5_CR19","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/S0020-0190(98)00150-1","volume":"68","author":"M. Jurdzinski","year":"1998","unstructured":"M. Jurdzinski. Deciding the winner in parity games is in UP \u2229 co-UP. Information Processing Letters, 68(3):119\u2013124, 1998.","journal-title":"Information Processing Letters"},{"key":"5_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"290","DOI":"10.1007\/3-540-46541-3_24","volume-title":"Theoretical Aspects of Computer Science","author":"M. Jurdzinski","year":"2000","unstructured":"M. Jurdzinski. Small progress measures for solving parity games. In Theoretical Aspects of Computer Science, LNCS 1770, pages 290\u2013301. Springer-Verlag, 2000."},{"key":"5_CR21","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"D. Kozen. Results on the propositional \u03bc-calculus. Theoretical Computer Science, 27:333\u2013354, 1983.","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"5_CR22","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/BF00370554","volume":"47","author":"D. Kozen","year":"1988","unstructured":"D. Kozen. A finite model theorem for the propositional \u03bc-calculus. Studia Logica, 47(3):333\u2013354, 1988.","journal-title":"Studia Logica"},{"key":"5_CR23","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1145\/345099.345104","volume":"22","author":"O. Kupferman","year":"2000","unstructured":"O. Kupferman and M. Vardi. An automata-theoretic approach to modular model checking. ACM Trans. on Programming Languages and Systems, 22:87\u2013128, 2000.","journal-title":"ACM Trans. on Programming Languages and Systems"},{"issue":"2","key":"5_CR24","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O. Kupferman","year":"2000","unstructured":"O. Kupferman, M. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. Journal of the ACM, 47(2):312\u2013360, 2000.","journal-title":"Journal of the ACM"},{"key":"5_CR25","unstructured":"R. Kurshan. FormalCheck User\u2019s Manual. Cadence Design Inc., 1998."},{"key":"5_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1007\/3-540-58179-0_66","volume-title":"Computer Aided Verification","author":"D. Long","year":"1994","unstructured":"D. Long, A. Brown, E. Clarke, S. Jha, and W. Marrero. An improved algorithm for the evaluation of fixpoint expressions. In Computer Aided Verification, LNCS 818, pages 338\u2013350. Springer-Verlag, 1994."},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"K. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"5_CR28","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/978-3-642-82453-1_5","volume":"F-13","author":"A. Pnueli","year":"1985","unstructured":"A. Pnueli. In transition from global to modular temporal reasoning about programs. In Logics and Models of Concurrent Systems, volume F-13 of NATO Advanced Summer Institutes, pages 123\u2013144. Springer-Verlag, 1985.","journal-title":"Logics and Models of Concurrent Systems"},{"key":"5_CR29","doi-asserted-by":"crossref","unstructured":"A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proc. Principles of Programming Languages, pages 179\u2013190. ACM Press, 1989.","DOI":"10.1145\/75277.75293"},{"key":"5_CR30","first-page":"81","volume":"77","author":"P. Ramadge","year":"1989","unstructured":"P. Ramadge and W. Wonham. The control of discrete-event systems. IEEE Trans. on Control Theory, 77:81\u201398, 1989.","journal-title":"IEEE Trans. on Control Theory"},{"issue":"6","key":"5_CR31","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1016\/0020-0190(96)00130-5","volume":"59","author":"H. Seidl","year":"1996","unstructured":"H. Seidl. Fast and simple nested fixpoints. Information Processing Letters, 59(6):303\u2013308, 1996.","journal-title":"Information Processing Letters"},{"key":"5_CR32","doi-asserted-by":"crossref","unstructured":"M. Vardi. A temporal fixpoint calculus. In Proc. Principles of Programming Languages, pages 250\u2013259. ACM Press, 1988.","DOI":"10.1145\/73560.73582"},{"key":"5_CR33","doi-asserted-by":"crossref","unstructured":"M. Vardi and L. Stockmeyer. Improved upper and lower bounds for modal logics of programs. In Proc. Theory of Computing, pages 240\u2013251. ACM Press, 1985.","DOI":"10.1145\/22145.22173"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36577-X_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,25]],"date-time":"2021-10-25T04:08:32Z","timestamp":1635134912000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36577-X_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008989","9783540365778"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/3-540-36577-x_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}