{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T06:29:29Z","timestamp":1762324169533},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319703886"},{"type":"electronic","value":"9783319703893"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-70389-3_10","type":"book-chapter","created":{"date-parts":[[2017,11,11]],"date-time":"2017-11-11T14:42:30Z","timestamp":1510411350000},"page":"147-162","source":"Crossref","is-referenced-by-count":25,"title":["A Symbolic Approach to Safety ltl Synthesis"],"prefix":"10.1007","author":[{"given":"Shufang","family":"Zhu","sequence":"first","affiliation":[]},{"given":"Lucas M.","family":"Tabajara","sequence":"additional","affiliation":[]},{"given":"Jianwen","family":"Li","sequence":"additional","affiliation":[]},{"given":"Geguang","family":"Pu","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,11,12]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Henzinger, T.A., Kupferman, O.: Concurrent reachability games. In: FOCS, pp. 564\u2013575 (1998)","DOI":"10.1109\/SFCS.1998.743507"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-54013-4_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Bloem","year":"2014","unstructured":"Bloem, R., K\u00f6nighofer, R., Seidl, M.: SAT-Based synthesis methods for safety specs. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 1\u201320. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54013-4_1"},{"issue":"3","key":"10_CR3","doi-asserted-by":"crossref","first-page":"911","DOI":"10.1016\/j.jcss.2011.08.007","volume":"78","author":"R Bloem","year":"2012","unstructured":"Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of Reactive(1) designs. J. Comput. Syst. Sci. 78(3), 911\u2013938 (2012)","journal-title":"J. Comput. Syst. Sci."},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1007\/978-3-642-31424-7_45","volume-title":"Computer Aided Verification","author":"A Bohy","year":"2012","unstructured":"Bohy, A., Bruy\u00e8re, V., Filiot, E., Jin, N., Raskin, J.-F.: Acacia+, a Tool for LTL synthesis. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 652\u2013657. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_45"},{"issue":"3","key":"10_CR5","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"RE Bryant","year":"1992","unstructured":"Bryant, R.E.: Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams. ACM Comput. Surv. 24(3), 293\u2013318 (1992)","journal-title":"ACM Comput. Surv."},{"key":"10_CR6","unstructured":"B\u00fcchi, J.R.: Weak Second-Order Arithmetic and Finite Automata. Z.Math. Logik Grundl. Math. 6, 66\u201392 (1960)"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Calude, C.S., Jain, S., Khoussainov, B., Li, W., Stephan, F.: Deciding parity games in Quasipolynomial time. In: STOC, pp. 252\u2013263 (2017)","DOI":"10.1145\/3055399.3055409"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-319-41528-4_6","volume-title":"Computer Aided Verification","author":"C-H Cheng","year":"2016","unstructured":"Cheng, C.-H., Hamza, Y., Ruess, H.: Structural synthesis for GXW specifications. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 95\u2013117. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_6"},{"key":"10_CR9","unstructured":"De Giacomo, G., Vardi, M.Y.: Synthesis for LTL and LDL on Finite Traces. In: IJCAI, pp. 1558\u20131564 (2015)"},{"issue":"5","key":"10_CR10","doi-asserted-by":"crossref","first-page":"406","DOI":"10.1016\/S0022-0000(70)80041-1","volume":"4","author":"J Doner","year":"1970","unstructured":"Doner, J.: Tree Acceptors and Some of Their Applications. J. Comput. Syst. Sci. 4(5), 406\u2013451 (1970)","journal-title":"J. Comput. Syst. Sci."},{"issue":"3","key":"10_CR11","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","volume":"1","author":"WF Dowling","year":"1984","unstructured":"Dowling, W.F., Gallier, J.H.: Linear-Time Algorithms for Testing the Satisfiability of Propositional Horn Formulae. J. Log. Program. 1(3), 267\u2013284 (1984)","journal-title":"J. Log. Program."},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-319-46520-3_8","volume-title":"Automated Technology for Verification and Analysis","author":"A Duret-Lutz","year":"2016","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, \u00c9., Xu, L.: Spot 2.0 \u2014 A framework for LTL and $$\\omega $$ -automata manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 122\u2013129. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_8"},{"key":"10_CR13","unstructured":"E\u00e9n, N., Mishchenko, A., Amla, N.: A Single-Instance Incremental SAT Formulation of Proof- and Counterexample-Based Abstraction (2010)"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/978-3-642-14295-6_33","volume-title":"Computer Aided Verification","author":"R Ehlers","year":"2010","unstructured":"Ehlers, R.: Symbolic bounded synthesis. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 365\u2013379. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_33"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Fogarty, S., Kupferman, O., Vardi, M.Y., Wilke, T.: Profile Trees for B\u00fcchi Word Automata, with Application to Determinization. In: GandALF, pp. 107\u2013121 (2013)","DOI":"10.4204\/EPTCS.119.11"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/978-3-319-41540-6_22","volume-title":"Computer Aided Verification","author":"D Fried","year":"2016","unstructured":"Fried, D., Tabajara, L.M., Vardi, M.Y.: BDD-Based boolean functional synthesis. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016, Part II. LNCS, vol. 9780, pp. 402\u2013421. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_22"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53\u201365. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_6"},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/3-540-60630-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"JG Henriksen","year":"1995","unstructured":"Henriksen, J.G., Jensen, J., J\u00f8rgensen, M., Klarlund, N., Paige, R., Rauhe, T., Sandholm, A.: Mona: monadic second-order logic in practice. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 89\u2013110. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60630-0_5"},{"issue":"3","key":"10_CR19","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Model Checking of Safety Properties. Formal Methods in System Design 19(3), 291\u2013314 (2001)","journal-title":"Formal Methods in System Design"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Safraless Decision Procedures. In: FOCS, pp. 531\u2013542 (2005)","DOI":"10.1109\/SFCS.2005.66"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Lamport, L.: What good is temporal logic? In: IFIP Congress, pp. 657\u2013668 (1983)","DOI":"10.1145\/2402.322398"},{"issue":"8","key":"10_CR22","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1145\/1536616.1536637","volume":"52","author":"S Malik","year":"2009","unstructured":"Malik, S., Zhang, L.: Boolean Satisfiability from Theoretical Hardness to Practical Success. Commun. ACM 52(8), 76\u201382 (2009)","journal-title":"Commun. ACM"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The Temporal Logic of Programs. In: FOCS, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the Synthesis of a Reactive Module. In: POPL, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"10_CR25","doi-asserted-by":"crossref","unstructured":"Safra, S.: On the Complexity of omega-Automata. In: FOCS, pp. 319\u2013327 (1988)","DOI":"10.1109\/SFCS.1988.21948"},{"issue":"5","key":"10_CR26","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1007\/BF01211865","volume":"6","author":"AP Sistla","year":"1994","unstructured":"Sistla, A.P.: Safety, Liveness and Fairness in Temporal Logic. Formal Asp. Comput. 6(5), 495\u2013512 (1994)","journal-title":"Formal Asp. Comput."},{"key":"10_CR27","doi-asserted-by":"crossref","unstructured":"Sohail, S., Somenzi, F.: Safety First: A Two-Stage Algorithm for LTL Games. In: FMCAD, pp. 77\u201384 (2009)","DOI":"10.1109\/FMCAD.2009.5351138"},{"key":"10_CR28","unstructured":"Somenzi, F.: CUDD: CU Decision Diagram Package 3.0.0. Universiy of Colorado at Boulder (2016)"},{"key":"10_CR29","doi-asserted-by":"crossref","unstructured":"Zhu, S., Tabajara, L.M., Li, J., Pu, G., Vardi, M.Y.: Symbolic LTL $$_f$$ Synthesis. In: IJCAI, pp. 1362\u20131369 (2017)","DOI":"10.24963\/ijcai.2017\/189"},{"issue":"3","key":"10_CR30","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/362566.362568","volume":"14","author":"ZM Zohar","year":"1971","unstructured":"Zohar, Z.M., Waldinger, R.: Toward Automatic Program Synthesis. Commun. ACM 14(3), 151\u2013165 (1971)","journal-title":"Commun. ACM"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-70389-3_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,21]],"date-time":"2020-10-21T17:45:26Z","timestamp":1603302326000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-70389-3_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319703886","9783319703893"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-70389-3_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}