{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,20]],"date-time":"2025-11-20T06:36:02Z","timestamp":1763620562592,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030148119"},{"type":"electronic","value":"9783030148126"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-14812-6_43","type":"book-chapter","created":{"date-parts":[[2019,4,9]],"date-time":"2019-04-09T23:44:24Z","timestamp":1554853464000},"page":"684-705","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["First-Order vs. Second-Order Encodings for $$\\textsc {ltl}_f$$-to-Automata Translation"],"prefix":"10.1007","author":[{"given":"Shufang","family":"Zhu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Geguang","family":"Pu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,3,6]]},"reference":[{"key":"43_CR1","doi-asserted-by":"crossref","unstructured":"Bloem, R., Galler, S.J., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Interactive pesentation: automatic hardware synthesis from specifications: a case study. In: DATE, pp. 1188\u20131193 (2007)","DOI":"10.1109\/DATE.2007.364456"},{"key":"43_CR2","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":"43_CR3","doi-asserted-by":"publisher","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."},{"issue":"2","key":"43_CR4","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J Burch","year":"1992","unstructured":"Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, L.: Symbolic model checking: $$10^{20}$$ states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"issue":"1","key":"43_CR5","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1145\/322234.322243","volume":"28","author":"A Chandra","year":"1981","unstructured":"Chandra, A., Kozen, D., Stockmeyer, L.: Alternation. J. ACM 28(1), 114\u2013133 (1981)","journal-title":"J. ACM"},{"key":"43_CR6","unstructured":"De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: IJCAI, pp. 854\u2013860 (2013)"},{"key":"43_CR7","doi-asserted-by":"crossref","unstructured":"De Giacomo, G., De Masellis, R., Montali, M.: Reasoning on LTL on finite traces: insensitivity to infiniteness. In: AAAI, pp. 1027\u20131033 (2014)","DOI":"10.1609\/aaai.v28i1.8872"},{"key":"43_CR8","unstructured":"De Giacomo, G., Vardi, M.Y.: Synthesis for LTL and LDL on finite traces. In: IJCAI, pp. 1558\u20131564 (2015)"},{"key":"43_CR9","unstructured":"De Giacomo, G., Vardi, M.Y.: LTL$$_f$$ and LDL$$_f$$ synthesis under partial observability. In: IJCAI, pp. 1044\u20131050 (2016)"},{"key":"43_CR10","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1016\/j.is.2015.06.009","volume":"56","author":"C Di Ciccio","year":"2016","unstructured":"Di Ciccio, C., Maggi, F.M., Mendling, J.: Efficient discovery of target-branched declare constraints. Inf. Syst. 56, 258\u2013283 (2016)","journal-title":"Inf. Syst."},{"issue":"4","key":"43_CR11","doi-asserted-by":"publisher","first-page":"24:1","DOI":"10.1145\/2629447","volume":"5","author":"CD Ciccio","year":"2015","unstructured":"Ciccio, C.D., Mecella, M.: On the discovery of declarative control flows for artful processes. ACM Trans. Manag. Inf. Syst. 5(4), 24:1\u201324:37 (2015)","journal-title":"ACM Trans. Manag. Inf. Syst."},{"key":"43_CR12","doi-asserted-by":"crossref","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0 \u2013 a framework for LTL and $$\\omega $$-automata manipulation. In: ATVA, pp. 122\u2013129 (2016)","DOI":"10.1007\/978-3-319-46520-3_8"},{"key":"43_CR13","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., et al.: 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":"6","key":"43_CR14","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1109\/TC.1978.1675141","volume":"27","author":"SB Akers Jr","year":"1978","unstructured":"Akers Jr., S.B.: Binary decision diagrams. IEEE Trans. Comput. 27(6), 509\u2013516 (1978)","journal-title":"IEEE Trans. Comput."},{"key":"43_CR15","unstructured":"Kamp, J.: Tense logic and the theory of order. Ph.D. thesis, UCLA (1968)"},{"key":"43_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/3-540-44674-5_15","volume-title":"Implementation and Application of Automata","author":"N Klarlund","year":"2001","unstructured":"Klarlund, N., M\u00f8ller, A., Schwartzbach, M.I.: MONA implementation secrets. In: Yu, S., P\u0103un, A. (eds.) CIAA 2000. LNCS, vol. 2088, pp. 182\u2013194. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44674-5_15"},{"key":"43_CR17","unstructured":"Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: FOCS, pp. 531\u2013540 (2005)"},{"issue":"3","key":"43_CR18","doi-asserted-by":"publisher","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 Syst. Des. 19(3), 291\u2013314 (2001)","journal-title":"Formal Methods Syst. Des."},{"key":"43_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/3-540-15648-8_16","volume-title":"Logics of Programs","author":"O Lichtenstein","year":"1985","unstructured":"Lichtenstein, O., Pnueli, A., Zuck, L.: The glory of the past. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol. 193, pp. 196\u2013218. Springer, Heidelberg (1985). https:\/\/doi.org\/10.1007\/3-540-15648-8_16"},{"key":"43_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/3-540-61648-9_56","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"M Biehl","year":"1996","unstructured":"Biehl, M., Klarlund, N., Rauhe, T.: Mona: decidable arithmetic in practice. In: Jonsson, B., Parrow, J. (eds.) FTRTFT 1996. LNCS, vol. 1135, pp. 459\u2013462. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61648-9_56"},{"key":"43_CR21","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/3-540-45620-1_2","volume-title":"Automated Deduction\u2014CADE-18","author":"G Pan","year":"2002","unstructured":"Pan, G., Sattler, U., Vardi, M.Y.: BDD-based decision procedures for $$\\cal{K}$$. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 16\u201330. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45620-1_2"},{"key":"43_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-3-540-45085-6_7","volume-title":"Automated Deduction \u2013 CADE-19","author":"G Pan","year":"2003","unstructured":"Pan, G., Vardi, M.Y.: Optimizing a BDD-based modal solver. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 75\u201389. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45085-6_7"},{"key":"43_CR23","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":"43_CR24","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":"43_CR25","unstructured":"Prescher, J., Di Ciccio, C., Mendling, J.: From declarative processes to imperative models. In: SIMPDA 2014, pp. 162\u2013173 (2014)"},{"key":"43_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-540-73370-6_11","volume-title":"Model Checking Software","author":"KY Rozier","year":"2007","unstructured":"Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 149\u2013167. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73370-6_11"},{"key":"43_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/978-3-642-21437-0_31","volume-title":"FM 2011: Formal Methods","author":"KY Rozier","year":"2011","unstructured":"Rozier, K.Y., Vardi, M.Y.: A multi-encoding approach for LTL symbolic satisfiability checking. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 417\u2013431. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_31"},{"key":"43_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-39611-3_23","volume-title":"Hardware and Software: Verification and Testing","author":"KY Rozier","year":"2013","unstructured":"Rozier, K.Y., Vardi, M.Y.: Deterministic compilation of temporal safety properties in explicit state model checking. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 243\u2013259. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39611-3_23"},{"issue":"3","key":"43_CR29","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/s10703-011-0139-8","volume":"41","author":"D Tabakov","year":"2012","unstructured":"Tabakov, D., Rozier, K.Y., Vardi, M.Y.: Optimized temporal monitors for SystemC. Formal Methods Syst. Des. 41(3), 236\u2013268 (2012)","journal-title":"Formal Methods Syst. Des."},{"key":"43_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-319-70389-3_10","volume-title":"Hardware and Software: Verification and Testing","author":"S Zhu","year":"2017","unstructured":"Zhu, S., Tabajara, L.M., Li, J., Pu, G., Vardi, M.Y.: A symbolic approach to safety ltl synthesis. Hardware and Software: Verification and Testing. LNCS, vol. 10629, pp. 147\u2013162. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-70389-3_10"},{"key":"43_CR31","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"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Models of Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-14812-6_43","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,7]],"date-time":"2024-03-07T15:11:58Z","timestamp":1709824318000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-14812-6_43"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030148119","9783030148126"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-14812-6_43","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"6 March 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TAMC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Theory and Applications of Models of Computation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Kitakyushu","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 April 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tamc2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}