{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T13:03:18Z","timestamp":1770296598947,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642314230","type":"print"},{"value":"9783642314247","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31424-7_7","type":"book-chapter","created":{"date-parts":[[2012,6,21]],"date-time":"2012-06-21T14:26:49Z","timestamp":1340288809000},"page":"7-22","source":"Crossref","is-referenced-by-count":37,"title":["Deterministic Automata for the (F,G)-Fragment of LTL"],"prefix":"10.1007","author":[{"given":"Jan","family":"K\u0159et\u00ednsk\u00fd","sequence":"first","affiliation":[]},{"given":"Javier","family":"Esparza","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"7_CR1","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":"7_CR2","unstructured":"Baier, C., Katoen, J.-P.: Principles of model checking. MIT Press (2008)"},{"key":"7_CR3","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.\u00a02102, pp. 53\u201365. Springer, Heidelberg (2001), Tool accessible at http:\/\/www.lsv.ens-cachan.fr\/"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: FMCAD, pp. 117\u2013124. IEEE Computer Society (2006)","DOI":"10.1109\/FMCAD.2006.22"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-73368-3_29","volume-title":"Computer Aided Verification","author":"B. Jobstmann","year":"2007","unstructured":"Jobstmann, B., Galler, S., Weiglhofer, M., Bloem, R.: Anzu: A Tool for Property Synthesis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 258\u2013262. Springer, Heidelberg (2007)"},{"issue":"2","key":"7_CR6","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1016\/j.tcs.2006.07.022","volume":"363","author":"J. Klein","year":"2006","unstructured":"Klein, J., Baier, C.: Experiments with deterministic omega-automata for formulas of linear temporal logic. Theor. Comput. Sci.\u00a0363(2), 182\u2013195 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-540-76336-9_7","volume-title":"Implementation and Application of Automata","author":"J. Klein","year":"2007","unstructured":"Klein, J., Baier, C.: On-the-Fly Stuttering in the Construction of Deterministic \u03c9-Automata. In: Holub, J., \u017dd\u2019\u00e1rek, J. (eds.) CIAA 2007. LNCS, vol.\u00a04783, pp. 51\u201361. Springer, Heidelberg (2007)"},{"key":"7_CR8","unstructured":"Klein, J.: ltl2dstar - LTL to deterministic Streett and Rabin automata, http:\/\/www.ltl2dstar.de\/"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M. Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of Probabilistic Real-Time Systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/11817963_6","volume-title":"Computer Aided Verification","author":"O. Kupferman","year":"2006","unstructured":"Kupferman, O., Piterman, N., Vardi, M.Y.: Safraless Compositional Synthesis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 31\u201344. Springer, Heidelberg (2006)"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-642-20674-0_6","volume-title":"Model Checking and Artificial Intelligence","author":"O. Kupferman","year":"2011","unstructured":"Kupferman, O., Rosenberg, A.: The Blow-Up in Translating LTL to Deterministic Automata. In: van der Meyden, R., Smaus, J.-G. (eds.) MoChArt 2010. LNCS, vol.\u00a06572, pp. 85\u201394. Springer, Heidelberg (2011)"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-642-27660-6_8","volume-title":"SOFSEM 2012: Theory and Practice of Computer Science","author":"O. Kupferman","year":"2012","unstructured":"Kupferman, O.: Recent Challenges and Ideas in Temporal Synthesis. In: Bielikov\u00e1, M., Friedrich, G., Gottlob, G., Katzenbeisser, S., Tur\u00e1n, G. (eds.) SOFSEM 2012. LNCS, vol.\u00a07147, pp. 88\u201398. Springer, Heidelberg (2012)"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: FOCS, pp. 531\u2013542. IEEE Computer Society (2005)","DOI":"10.1109\/SFCS.2005.66"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-540-78163-9_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Morgenstern","year":"2008","unstructured":"Morgenstern, A., Schneider, K.: From LTL to Symbolically Represented Deterministic Automata. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol.\u00a04905, pp. 279\u2013293. Springer, Heidelberg (2008)"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-540-73370-6_17","volume-title":"Model Checking Software","author":"R. Pel\u00e1nek","year":"2007","unstructured":"Pel\u00e1nek, R.: BEEM: Benchmarks for Explicit Model Checkers. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 263\u2013267. Springer, Heidelberg (2007)"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Piterman, N.: From nondeterministic Buchi and Streett automata to deterministic parity automata. In: LICS, pp. 255\u2013264. IEEE Computer Society (2006)","DOI":"10.2168\/LMCS-3(3:5)2007"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11609773_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"N. Piterman","year":"2005","unstructured":"Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of Reactive(1) Designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 364\u2013380. Springer, Heidelberg (2005)"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/3-540-50403-6_28","volume-title":"Concurrency 88","author":"A. Pnueli","year":"1988","unstructured":"Pnueli, A., Rosner, R.: A Framework for the Synthesis of Reactive Modules. In: Vogt, F.H. (ed.) CONCURRENCY 1988. LNCS, vol.\u00a0335, pp. 4\u201317. Springer, Heidelberg (1988)"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Safra, S.: On the complexity of \u03c9-automata. In: FOCS, pp. 319\u2013327. IEEE Computer Society (1988)","DOI":"10.1109\/SFCS.1988.21948"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/10722167_21","volume-title":"Computer Aided Verification","author":"F. Somenzi","year":"2000","unstructured":"Somenzi, F., Bloem, R.: Efficient B\u00fcchi Automata from LTL Formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 248\u2013263. Springer, Heidelberg (2000)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31424-7_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,2]],"date-time":"2025-04-02T09:30:33Z","timestamp":1743586233000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31424-7_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642314230","9783642314247"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31424-7_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}