{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:03:07Z","timestamp":1776304987581,"version":"3.50.1"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2011,12,21]],"date-time":"2011-12-21T00:00:00Z","timestamp":1324425600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2012,4]]},"DOI":"10.1007\/s10703-011-0137-x","type":"journal-article","created":{"date-parts":[[2011,12,20]],"date-time":"2011-12-20T20:45:18Z","timestamp":1324413918000},"page":"232-262","source":"Crossref","is-referenced-by-count":27,"title":["Symbolic bounded synthesis"],"prefix":"10.1007","volume":"40","author":[{"given":"R\u00fcdiger","family":"Ehlers","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,12,21]]},"reference":[{"issue":"2","key":"137_CR1","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1007\/s10009-004-0179-0","volume":"7","author":"R Alur","year":"2005","unstructured":"Alur R, Madhusudan P, Nam W (2005) Symbolic computational techniques for solving games. Int J Softw Tools Technol Transf 7(2):118\u2013128","journal-title":"Int J Softw Tools Technol Transf"},{"issue":"1","key":"137_CR2","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(94)90266-6","volume":"126","author":"HR Andersen","year":"1994","unstructured":"Andersen HR (1994) Model checking and Boolean graphs. Theor Comput Sci 126(1):3\u201330","journal-title":"Theor Comput Sci"},{"issue":"4","key":"137_CR3","doi-asserted-by":"crossref","first-page":"727","DOI":"10.1142\/S0129054107004942","volume":"18","author":"R Bloem","year":"2007","unstructured":"Bloem R, Cimatti A, Pill I, Roveri M (2007) Symbolic implementation of alternating automata. Int J Found Comput Sci 18(4):727\u2013743","journal-title":"Int J Found Comput Sci"},{"issue":"4","key":"137_CR4","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.entcs.2007.09.004","volume":"190","author":"R Bloem","year":"2007","unstructured":"Bloem R, Galler S, Jobstmann B, Piterman N, Pnueli A, Weiglhofer M (2007) Specify, compile, run: hardware from PSL. Electron Notes Theor Comput Sci 190(4):3\u201316","journal-title":"Electron Notes Theor Comput Sci"},{"key":"137_CR5","first-page":"1188","volume-title":"DATE","author":"R Bloem","year":"2007","unstructured":"Bloem R, Galler SJ, Jobstmann B, Piterman N, Pnueli A, Weiglhofer M (2007) Interactive presentation: automatic hardware synthesis from specifications: a case study. In: Lauwereins R, Madsen J (eds) DATE. ACM Press, New York, pp\u00a01188\u20131193"},{"key":"137_CR6","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"410","DOI":"10.1007\/978-3-642-14295-6_36","volume-title":"Computer aided verification","author":"R Bloem","year":"2010","unstructured":"Bloem R, Chatterjee K, Greimel K, Henzinger TA, Jobstmann B (2010) Robustness in the presence of liveness. In: Touili T, Cook B, Jackson P (eds) Computer aided verification. Lecture notes in computer science, vol\u00a06174. Springer, Berlin, pp\u00a0410\u2013424"},{"key":"137_CR7","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/3-540-63166-6_19","volume-title":"Computer aided verification","author":"M Bozga","year":"1997","unstructured":"Bozga M, Maler O, Pnueli A, Yovine S (1997) Some progress in the symbolic verification of timed automata. In: Grumberg O (ed) Computer aided verification. Lecture notes in computer science, vol\u00a01254. Springer, Berlin, pp\u00a0179\u2013190"},{"issue":"8","key":"137_CR8","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant RE (1986) Graph-based algorithms for Boolean function manipulation. IEEE Trans Comput 35(8):677\u2013691","journal-title":"IEEE Trans Comput"},{"issue":"2","key":"137_CR9","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ (1992) Symbolic model checking: 1020 states and beyond. Inf Comput 98(2):142\u2013170","journal-title":"Inf Comput"},{"key":"137_CR10","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer aided verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti A, Clarke EM, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A (2002) NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma E, Larsen KG (eds) Computer aided verification. Lecture notes in computer science, vol\u00a02404. Springer, Berlin, pp\u00a0359\u2013364"},{"key":"137_CR11","series-title":"Lecture notes in computer science","first-page":"48","volume-title":"Computer aided verification","author":"R Cleaveland","year":"1991","unstructured":"Cleaveland R, Steffen B (1991) A linear-time model-checking algorithm for the alternation-free modal \u03bc-calculus. In: Larsen KG, Skou A (eds) Computer aided verification. Lecture notes in computer science, vol\u00a0575. Springer, Berlin, pp\u00a048\u201358"},{"issue":"2","key":"137_CR12","doi-asserted-by":"crossref","first-page":"112","DOI":"10.1007\/s100090100056","volume":"3","author":"R Drechsler","year":"2001","unstructured":"Drechsler R, Sieling D (2001) Binary decision diagrams in theory and practice. Int J Softw Tools Technol Transf 3(2):112\u2013136","journal-title":"Int J Softw Tools Technol Transf"},{"key":"137_CR13","series-title":"Lecture notes in computer science","first-page":"3","volume-title":"Automata, logics, and infinite games","author":"B Farwer","year":"2001","unstructured":"Farwer B (2001) \u03c9-automata. In: Gr\u00e4del E, Thomas W, Wilke T (eds) Automata, logics, and infinite games. Lecture notes in computer science, vol\u00a02500. Springer, Berlin, pp\u00a03\u201320"},{"key":"137_CR14","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/978-3-642-02658-4_22","volume-title":"Computer aided verification","author":"E Filiot","year":"2009","unstructured":"Filiot E, Jin N, Raskin JF (2009) An antichain algorithm for LTL realizability. In: Computer aided verification. Lecture notes in computer science, vol\u00a05643. Springer, Berlin, pp\u00a0263\u2013277"},{"key":"137_CR15","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"112","DOI":"10.1007\/978-3-642-15643-4_10","volume-title":"ATVA","author":"E Filiot","year":"2010","unstructured":"Filiot E, Jin N, Raskin JF (2010) Compositional algorithms for LTL synthesis. In: Bouajjani A, Chin WN (eds) ATVA. Lecture notes in computer science, vol\u00a06252. Springer, Berlin, pp\u00a0112\u2013127"},{"key":"137_CR16","volume-title":"Automated formal methods (AFM)","author":"B Finkbeiner","year":"2007","unstructured":"Finkbeiner B, Schewe S (2007) SMT-based synthesis of distributed systems. In: Automated formal methods (AFM)"},{"key":"137_CR17","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","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 (2001) Fast LTL to B\u00fcchi automata translation. In: Computer aided verification. Lecture notes in computer science, vol\u00a02102. Springer, Berlin, pp\u00a053\u201365"},{"key":"137_CR18","author":"Y Godhal","year":"2011","unstructured":"Godhal Y, Chatterjee K, Henzinger T (2011) Synthesis of AMBA AHB from formal specification: a case study. Int J Softw Tools Technol Transf. doi: 10.1007\/s10009-011-0207-9","journal-title":"Int J Softw Tools Technol Transf"},{"key":"137_CR19","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/11901914_17","volume-title":"ATVA","author":"M Helmert","year":"2006","unstructured":"Helmert M, Mattm\u00fcller R, Schewe S (2006) Selective approaches for solving weak games. In: Graf S, Zhang W (eds) ATVA. Lecture notes in computer science, vol\u00a04218. Springer, Berlin, pp\u00a0200\u2013214"},{"key":"137_CR20","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1007\/11874683_26","volume-title":"CSL","author":"TA Henzinger","year":"2006","unstructured":"Henzinger TA, Piterman N (2006) Solving games without determinization. In: \u00c9sik Z (ed) CSL. Lecture notes in computer science, vol\u00a04207. Springer, Berlin, pp\u00a0395\u2013410"},{"key":"137_CR21","first-page":"117","volume-title":"FMCAD","author":"B Jobstmann","year":"2006","unstructured":"Jobstmann B, Bloem R (2006) Optimizations for LTL synthesis. In: FMCAD. IEEE Computer Society Press, Los Alamitos, pp\u00a0117\u2013124"},{"key":"137_CR22","series-title":"Lecture notes in computer science","volume-title":"HVC","author":"U Klein","year":"2010","unstructured":"Klein U, Pnueli A (2010) Revisiting synthesis of GR(1) specifications. In: HVC. Lecture notes in computer science, vol\u00a06504. Springer, Berlin"},{"key":"137_CR23","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/10722167_12","volume-title":"Computer aided verification","author":"JH Kukula","year":"2000","unstructured":"Kukula JH, Shiple TR (2000) Building circuits from relations. In: Emerson EA, Sistla AP (eds) Computer aided verification. Lecture notes in computer science, vol\u00a01855. Springer, Berlin, pp\u00a0113\u2013123"},{"key":"137_CR24","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1007\/3-540-48683-6_17","volume-title":"Computer aided verification","author":"O Kupferman","year":"1999","unstructured":"Kupferman O, Vardi MY (1999) Model checking of safety properties. In: Halbwachs N, Peled D (eds) Computer aided verification. Lecture notes in computer science, vol\u00a01633. Springer, Berlin, pp\u00a0172\u2013183"},{"key":"137_CR25","first-page":"531","volume-title":"FOCS","author":"O Kupferman","year":"2005","unstructured":"Kupferman O, Vardi MY (2005) Safraless decision procedures. In: FOCS. IEEE Press, New York, pp\u00a0531\u2013542"},{"key":"137_CR26","doi-asserted-by":"crossref","unstructured":"Kupferman O, Lustig Y, Vardi M (2006) On locally checkable properties. In: Logic for programming, artificial intelligence, and reasoning, pp\u00a0302\u2013316. doi: 10.1007\/11916277_21","DOI":"10.1007\/11916277_21"},{"key":"137_CR27","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic model checking","author":"KL McMillan","year":"1993","unstructured":"McMillan KL (1993) Symbolic model checking. Kluwer Academic, Dordrecht"},{"key":"137_CR28","doi-asserted-by":"crossref","unstructured":"Piterman N (2007) From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. Log Methods Comput Sci 3(3)","DOI":"10.2168\/LMCS-3(3:5)2007"},{"key":"137_CR29","series-title":"Lecture notes in computer science","first-page":"364","volume-title":"VMCAI","author":"N Piterman","year":"2006","unstructured":"Piterman N, Pnueli A, Sa\u2019ar Y (2006) Synthesis of reactive(1) designs. In: Emerson EA, Namjoshi KS (eds) VMCAI. Lecture notes in computer science, vol\u00a03855. Springer, Berlin, pp\u00a0364\u2013380"},{"key":"137_CR30","first-page":"46","volume-title":"FOCS","author":"A Pnueli","year":"1977","unstructured":"Pnueli A (1977) The temporal logic of programs. In: FOCS. IEEE Press, New York, pp\u00a046\u201357"},{"key":"137_CR31","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"652","DOI":"10.1007\/BFb0035790","volume-title":"ICALP","author":"A Pnueli","year":"1989","unstructured":"Pnueli A, Rosner R (1989) On the synthesis of an asynchronous reactive module. In: Ausiello G, Dezani-Ciancaglini M, Rocca SRD (eds) ICALP. Lecture notes in computer science, vol\u00a0372. Springer, Berlin, pp\u00a0652\u2013671"},{"key":"137_CR32","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"474","DOI":"10.1007\/978-3-540-75596-8_33","volume-title":"ATVA","author":"S Schewe","year":"2007","unstructured":"Schewe S, Finkbeiner B (2007) Bounded synthesis. In: Namjoshi KS, Yoneda T, Higashino T, Okamura Y (eds) ATVA. Lecture notes in computer science, vol\u00a04762. Springer, Berlin, pp\u00a0474\u2013488"},{"key":"137_CR33","first-page":"31","volume-title":"Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen","author":"K Schneider","year":"1999","unstructured":"Schneider K, Logothetis G (1999) Abstraction of systems with counters for symbolic model checking. In: Mutz M, Lange N (eds) Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen. Shaker, Braunschweig, pp\u00a031\u201340"},{"key":"137_CR34","first-page":"39","volume-title":"PODC","author":"AP Sistla","year":"1985","unstructured":"Sistla AP (1985) On characterization of safety and liveness properties in temporal logic. In: PODC, pp\u00a039\u201348"},{"key":"137_CR35","first-page":"77","volume-title":"FMCAD","author":"S Sohail","year":"2009","unstructured":"Sohail S, Somenzi F (2009) Safety first: A two-stage algorithm for LTL games. In: FMCAD. IEEE Computer Society Press, Los Alamitos, pp\u00a077\u201384"},{"key":"137_CR36","unstructured":"Somenzi F (2009) CUDD: CU decision diagram package, release 2.4.2"},{"key":"137_CR37","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1007\/3-540-45657-0_5","volume-title":"Computer aided verification","author":"W Thomas","year":"2002","unstructured":"Thomas W (2002) Infinite games and verification (extended abstract of a tutorial). In: Brinksma E, Larsen KG (eds) Computer aided verification. Lecture notes in computer science, vol\u00a02404. Springer, Berlin, pp\u00a058\u201364"},{"key":"137_CR38","volume-title":"New perspectives on games and interaction","author":"W Thomas","year":"2008","unstructured":"Thomas W (2008) Solution of Church\u2019s problem: a tutorial. In: Apt K, Rooij RV (eds) New perspectives on games and interaction. Amsterdam University Press, Amsterdam"},{"issue":"1","key":"137_CR39","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"MY Vardi","year":"1994","unstructured":"Vardi MY, Wolper P (1994) Reasoning about infinite computations. Inf Comput 115(1):1\u201337","journal-title":"Inf Comput"},{"key":"137_CR40","doi-asserted-by":"crossref","DOI":"10.1137\/1.9780898719789","volume-title":"Branching programs and binary decision diagrams","author":"I Wegener","year":"2000","unstructured":"Wegener I (2000) Branching programs and binary decision diagrams. SIAM, Philadelphia"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-011-0137-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-011-0137-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-011-0137-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,29]],"date-time":"2020-06-29T01:36:19Z","timestamp":1593394579000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-011-0137-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,12,21]]},"references-count":40,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,4]]}},"alternative-id":["137"],"URL":"https:\/\/doi.org\/10.1007\/s10703-011-0137-x","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,12,21]]}}}