{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T07:26:43Z","timestamp":1750318003805},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540679011"},{"type":"electronic","value":"9783540446125"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44612-5_45","type":"book-chapter","created":{"date-parts":[[2007,5,5]],"date-time":"2007-05-05T09:28:20Z","timestamp":1178357300000},"page":"497-507","source":"Crossref","is-referenced-by-count":23,"title":["\u03bc-Calculus Synthesis"],"prefix":"10.1007","author":[{"given":"Oma","family":"Kupferman","sequence":"first","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,6,1]]},"reference":[{"key":"45_CR1","series-title":"Lect Notes Comput Sci","volume-title":"Proc. TACAS","author":"G. Bhat","year":"1996","unstructured":"G. Bhat and R. Cleaveland. Efficient local model-checking for fragments of the modal \u03bc-calculus. In Proc. TACAS, LNCS 1055, 1996."},{"issue":"2","key":"45_CR2","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. Information & Computation, 98(2): 142\u2013170, 1992.","journal-title":"Information & Computation"},{"key":"45_CR3","unstructured":"M. Daniele, P. Traverso, and M.Y. Vardi. Strong cyclic planning revisited. In Proc 5th European Conference on Planning, pp. 34\u201346, 1999."},{"key":"45_CR4","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and E.M. Clarke. Characterizing correctness properties of parallel programs using fixpoints. In Proc. 7th ICALP, pp. 169\u2013181, 1980.","DOI":"10.1007\/3-540-10003-2_69"},{"key":"45_CR5","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E.A. Emerson","year":"1982","unstructured":"E.A. Emerson and E.M. Clarke. Using branching time logic to synthesize synchronization skeletons. Science of Computer Programming, 2:241\u2013266, 1982.","journal-title":"Science of Computer Programming"},{"issue":"1","key":"45_CR6","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"E.A. Emerson and J.Y. 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":"45_CR7","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and C. Jutla. Tree automata, Mu-calculus and determinacy. In Proc. 32nd FOCS, pp. 368\u2013377, 1991.","DOI":"10.1109\/SFCS.1991.185392"},{"key":"45_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1007\/3-540-56922-7_32","volume-title":"Proc. 5th CAV","author":"E.A. Emerson","year":"1993","unstructured":"E.A. Emerson, C. Jutla, and A.P. Sistla. On model-checking for fragments of \u03bc-calculus. In Proc. 5th CAV, LNCS 697, pp. 385\u2013396, 1993."},{"key":"45_CR9","doi-asserted-by":"crossref","unstructured":"E.A. Emerson. Temporal and modal logic. Handbook of Theoretical Computer Science, pp. 997\u20131072, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"45_CR10","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M.J. Fischer","year":"1979","unstructured":"M.J. Fischer and R.E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and Systems Sciences, 18:194\u2013211, 1979.","journal-title":"Journal of Computer and Systems Sciences"},{"key":"45_CR11","doi-asserted-by":"crossref","unstructured":"E. Graedel and I. Walukiewicz. Guarded fixed point logic. In Proc. 14th LICS, 1999.","DOI":"10.1109\/LICS.1999.782585"},{"key":"45_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"552","DOI":"10.1007\/3-540-60246-1_160","volume-title":"Proc. 20th MFCS","author":"D. Janin","year":"1995","unstructured":"D. Janin and I. Walukiewicz. Automata for the modal \u03bc-calculus and related results. In Proc. 20th MFCS, LNCS, pp. 552\u2013562, 1995."},{"key":"45_CR13","doi-asserted-by":"crossref","unstructured":"R. Kumar and V.K. Garg. Modeling and control of logical discrete event systems.Kluwer Academic Publishers, 1995.","DOI":"10.1007\/978-1-4615-2217-1"},{"key":"45_CR14","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 prepositional\u03bc-calculus. Theoretical Computer Science, 27:333\u2013354, 1983.","journal-title":"Theoretical Computer Science"},{"key":"45_CR15","unstructured":"R. Kumar and M.A. Shayman. Supervisory control of nondeterministic systems under partial observation and decentralization. SIAM J. of Control and Optimization, 1995."},{"key":"45_CR16","unstructured":"O. Kupferman and M.Y. Vardi. Synthesis with incomplete informatio. In Proc. 2nd ICTL, pp. 91\u2013106, July 1997."},{"key":"45_CR17","doi-asserted-by":"crossref","unstructured":"O. Kupferman, M.Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. Journal of the ACM, 47(2), March 2000.","DOI":"10.1145\/333979.333987"},{"key":"45_CR18","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/0304-3975(94)00214-4","volume":"141","author":"D.E. Muller","year":"1995","unstructured":"D.E. Muller and P.E. Schupp. Simulating alternating tree automata by nondeterministic automata: New results and new proofs of theorems of Rabin, McNaughton and Safra. Theoretical Computer Science, 141:69\u2013107, 1995.","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"45_CR19","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1145\/357084.357090","volume":"2","author":"Z. Manna","year":"1980","unstructured":"Z. Manna and R. Waldinger. A deductive approach to program synthesis. ACM TOPLAS, 2(1):90\u2013121, 1980.","journal-title":"ACM TOPLAS"},{"key":"45_CR20","doi-asserted-by":"crossref","unstructured":"A. Pnueli and R. Rosner On the synthesis of a reactive module. In 16th POPL, 1989.","DOI":"10.1145\/75277.75293"},{"key":"45_CR21","doi-asserted-by":"crossref","unstructured":"M.O. Rabin. Weakly definable relations and special automata. In Proc. Symp. Math. Logic and Foundations of Set Theory, pp. 1\u201323. North Holland, 1970.","DOI":"10.1016\/S0049-237X(08)71929-3"},{"key":"45_CR22","series-title":"PhD thesis","volume-title":"Modular Synthesis of Reactive Systems","author":"R. Rosner","year":"1992","unstructured":"R. Rosner. Modular Synthesis of Reactive Systems. PhD thesis, Weizmann Institute of Science, Rehovot, Israel, 1992."},{"key":"45_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/3-540-60045-0_56","volume-title":"Proc. 7th CAV","author":"M.Y. Vardi","year":"1995","unstructured":"M.Y. Vardi. An automata-theoretic approach to fair realizability and synthesis. In Proc. 7th CAV, LNCS939, pp. 267\u2013292, 1995."},{"key":"45_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"628","DOI":"10.1007\/BFb0055090","volume-title":"Proc. 25th ICALP","author":"M.Y. Vardi","year":"1998","unstructured":"M.Y. Vardi. Reasoning about the past with two-way automata. In Proc. 25th ICALP, LNCS 1443, pp. 628\u2013641, 1998."},{"key":"45_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/3-540-46691-6_9","volume-title":"Proc. 19th TST & TCS","author":"T. Wilke","year":"1999","unstructured":"T. Wilke. CTL+ is exponentially more succinct than CTL. In Proc. 19th TST & TCS, LNCS 1738, pp. 110\u2013121, 1999."}],"container-title":["Lecture Notes in Computer Science","Mathematical Foundations of Computer Science 2000"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44612-5_45","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,27]],"date-time":"2019-04-27T14:41:39Z","timestamp":1556376099000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44612-5_45"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540679011","9783540446125"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-44612-5_45","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}