{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:17:01Z","timestamp":1775873821143,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540311393","type":"print"},{"value":"9783540316220","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11609773_24","type":"book-chapter","created":{"date-parts":[[2005,12,12]],"date-time":"2005-12-12T07:28:57Z","timestamp":1134372537000},"page":"364-380","source":"Crossref","is-referenced-by-count":231,"title":["Synthesis of Reactive(1) Designs"],"prefix":"10.1007","author":[{"given":"Nir","family":"Piterman","sequence":"first","affiliation":[]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[]},{"given":"Yaniv","family":"Sa\u2019ar","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/3-540-46002-0_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Armoni","year":"2002","unstructured":"Armoni, R., Fix, L., Flaisher, A., Gerth, R., Ginsburg, B., Kanza, T., Landver, A., Mador-Haim, S., Singerman, E., Tiemeyer, A., Vardi, M., Zbar, Y.: The ForSpec temporal logic: A new temporal property-specification language. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, p. 296. Springer, Heidelberg (2002)"},{"key":"24_CR2","first-page":"469","volume-title":"IFAC Symposium on System Structure and Control","author":"E. Asarin","year":"1998","unstructured":"Asarin, E., Maler, O., Pnueli, A., Sifakis, J.: Controller synthesis for timed automata. In: IFAC Symposium on System Structure and Control, pp. 469\u2013474. Elsevier, Amsterdam (1998)"},{"key":"24_CR3","unstructured":"Inc. Accellera\u00a0Organization. Formal semantics of Accellera(c) property specification language. Appendix B of (January 2004), \n                  \n                    http:\/\/www.eda.org\/vfv\/docs\/PSL-v1.1.pdf"},{"issue":"1","key":"24_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/963927.963928","volume":"5","author":"R. Alur","year":"2004","unstructured":"Alur, R., La Torre, S.: Deterministic generators and games for LTL fragments. ACM Trans. Comput. Log.\u00a05(1), 1\u201325 (2004)","journal-title":"ACM Trans. Comput. Log."},{"key":"24_CR5","doi-asserted-by":"publisher","first-page":"295","DOI":"10.2307\/1994916","volume":"138","author":"J.R. B\u00fcchi","year":"1969","unstructured":"B\u00fcchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Trans. Amer. Math. Soc.\u00a0138, 295\u2013311 (1969)","journal-title":"Trans. Amer. Math. Soc."},{"issue":"12","key":"24_CR6","doi-asserted-by":"publisher","first-page":"1035","DOI":"10.1109\/TC.1986.1676711","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers\u00a0C-35(12), 1035\u20131044 (1986)","journal-title":"IEEE Transactions on Computers"},{"key":"24_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"24_CR8","unstructured":"Church, A.: Logic, arithmetic and automata. In: Proc. 1962 Int. Congr. Math., pp. 23\u201325 (1962)"},{"key":"24_CR9","unstructured":"Emerson, E.A., Lei, C.L.: Efficient model-checking in fragments of the propositional modal \u03bc-calculus. In: Proc. First IEEE Symp. Logic in Comp. Sci., pp. 267\u2013278 (1986)"},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"Emerson, E.A.: Model checking and the \u03bc-calculus. In: Immerman, N., Kolaitis, P.G. (eds.) Descriptive Complexity and Finite Models, pp. 185\u2013214. AMS (1997)","DOI":"10.1090\/dimacs\/031\/06"},{"key":"24_CR11","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional \u03bc-calculus. Theoretical Computer Science\u00a027, 333\u2013354 (1983)","journal-title":"Theoretical Computer Science"},{"key":"24_CR12","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1006\/inco.2000.3000","volume":"163","author":"Y. Kesten","year":"2000","unstructured":"Kesten, Y., Pnueli, A.: Verification by augmented finitary abstraction. Inf. and Comp.\u00a0163, 203\u2013243 (2000)","journal-title":"Inf. and Comp."},{"issue":"1","key":"24_CR13","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1016\/j.ic.2005.01.006","volume":"200","author":"Y. Kesten","year":"2005","unstructured":"Kesten, Y., Piterman, N., Pnueli, A.: Bridging the gap between fair simulation and trace inclusion. Inf. and Comp.\u00a0200(1), 36\u201361 (2005)","journal-title":"Inf. and Comp."},{"key":"24_CR14","unstructured":"Lichtenstein, O.: Decidability, Completeness, and Extensions of Linear Time Temporal Logic. PhD thesis, Weizmann Institute of Science (1991)"},{"key":"24_CR15","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/357233.357237","volume":"6","author":"Z. Manna","year":"1984","unstructured":"Manna, Z., Wolper, P.: Synthesis of communicating processes from temporal logic specifications. ACM Trans. Prog. Lang. Sys.\u00a06, 68\u201393 (1984)","journal-title":"ACM Trans. Prog. Lang. Sys."},{"key":"24_CR16","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. 16th ACM Symp. Princ. of Prog. Lang., pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"24_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1007\/BFb0035790","volume-title":"Automata, Languages and Programming","author":"A. Pnueli","year":"1989","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol.\u00a0372, pp. 652\u2013671. Springer, Heidelberg (1989)"},{"key":"24_CR18","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: Proc. 31st IEEE Symp. Found. of Comp. Sci., pp. 746\u2013757 (1990)","DOI":"10.1109\/FSCS.1990.89597"},{"key":"24_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/3-540-61474-5_68","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"1996","unstructured":"Pnueli, A., Shahar, E.: A platform for combining deductive with algorithmic verification. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 184\u2013195. Springer, Heidelberg (1996)"},{"key":"24_CR20","doi-asserted-by":"crossref","unstructured":"Rabin, M.O.: Automata on Infinite Objects and Churc\u2019s Problem. Regional Conference Series in Mathematics, vol.\u00a013. Amer. Math. Soc. (1972)","DOI":"10.1090\/cbms\/013"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11609773_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:07:03Z","timestamp":1619507223000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11609773_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540311393","9783540316220"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/11609773_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}