{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:26Z","timestamp":1761611186501},"reference-count":85,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2006,8,31]],"date-time":"2006-08-31T00:00:00Z","timestamp":1156982400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[2006,11,3]]},"DOI":"10.1007\/s10703-006-0019-9","type":"journal-article","created":{"date-parts":[[2006,8,30]],"date-time":"2006-08-30T17:52:31Z","timestamp":1156960351000},"page":"51-81","source":"Crossref","is-referenced-by-count":7,"title":["Bounded model checking of infinite state systems"],"prefix":"10.1007","volume":"30","author":[{"given":"Tobias","family":"Schuele","sequence":"first","affiliation":[]},{"given":"Klaus","family":"Schneider","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,8,31]]},"reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"Alt M, Ferdinand C, Martin F, Wilhelm R (1996) Cache behavior prediction by abstract interpretation. In: Static analysis symposium (SAS). LNCS, vol 1145. Springer, Aachen, Germany, pp 52\u201366","DOI":"10.1007\/3-540-61739-6_33"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Amla N, Kurshan R, McMillan K, Medel R (2003) Experimental analysis of different techniques for bounded model checking. In: Garavel H, Hatcliff J (eds) Conference on tools and algorithms for the construction and analysis of systems (TACAS). LNCS, vol 2619. Springer, Warsaw, Poland, pp 34\u201348","DOI":"10.1007\/3-540-36577-X_4"},{"key":"19_CR3","unstructured":"Andrews G (1991) Concurrent programming\u2014Principles and practice. The Benjamin\/Cummings Publishing Company, Redwood City, California"},{"key":"19_CR4","unstructured":"Berry G (1999) The constructive semantics of pure Esterel. http:\/\/www-sop.inria.fr\/esterel.org"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Berthet C, Coudert O, Madre J (1990) New ideas on symbolic manipulations of finite state machines. In: International conference on computer design (ICCD). IEEE, pp 224\u2013227","DOI":"10.1109\/ICCD.1990.130210"},{"key":"19_CR6","unstructured":"Biere A, Cimatti A, Clarke E, Fujita M, Zhu Y (1999) Symbolic model checking using SAT procedures instead of BDDs. In: International design automation conference (DAC). ACM, New Orleans, Louisiana, USA, pp 317\u2013320"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke E, Strichman O, Zhu Y (2003) Bounded model checking. Adv Comput 58","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke E, Zhu Y (1999) Symbolic model checking without BDDs. In: Cleaveland R (ed) Conference on tools and algorithms for the construction and analysis of systems (TACAS). LNCS, vol 1579. Springer, Amsterdam, The Netherlands, pp 193\u2013207","DOI":"10.21236\/ADA360973"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Boigelot B, Wolper P (2002) Representing arithmetic constraints with finite automata: An overview. In: International conference on logic programming (ICPL). LNCS, vol 2401. Springer, Copenhagen, Denmark, pp 1\u201319","DOI":"10.1007\/3-540-45619-8_1"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Boudet A, Comon H (1996) Diophantine equations, Presburger arithmetic and finite automata. In: Kirchner H (ed) Colloquium on trees in algebra and programming (CAAP). LNCS, vol 1059. Springer, Link\u00f6ping, Sweden, pp 30\u201343","DOI":"10.1007\/3-540-61064-2_27"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Bradfield J (1992) Verifying temporal properties of systems. Progress in theoretical computer science. Birkh\u00e4user, Boston, Basel, Berlin","DOI":"10.1007\/978-1-4684-6819-9"},{"key":"19_CR12","unstructured":"Bradfield J, Stirling C (1991) Local model checking for infinite state spaces. In: Larsen K, Skou A (eds) Workshop on computer aided verification (CAV)"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Bryant R (1986) Graph-based algorithms for Boolean function manipulation. IEEE Trans Comput C-35(8):677\u2013691","DOI":"10.1109\/TC.1986.1676819"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Bryant R (1991) On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication. IEEE Trans Comput 40(2):205\u2013213","DOI":"10.1109\/12.73590"},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"Brzozowski J, Seger C-J (1995) Asynchronous circuits. Springer","DOI":"10.1007\/978-1-4612-4210-9"},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"Bultan T, Gerber R, Pugh W (1997) Symbolic model checking of infinite state systems using Presburger arithmetic. In: Grumberg O (ed) Conference on computer aided verification (CAV). LNCS, vol 1254. Springer, Haifa, Israel, pp 400\u2013411","DOI":"10.1007\/3-540-63166-6_39"},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"Bultan T, Gerber R, Pugh W (1999) Model-checking concurrent systems with unbounded integer variables. ACM Trans Progr Lang Syst (TOPLAS) 21(4):747\u2013789","DOI":"10.1145\/325478.325480"},{"key":"19_CR18","unstructured":"Burch J, Clarke E, McMillan K, Dill D, Hwang L (1990) Symbolic model checking: 1020 states and beyond. In: Symposium on logic in computer science (LICS). IEEE Computer Society, Washington, DC, pp 1\u201333"},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"Burch J, Clarke E, McMillan K, Dill D, Hwang L (1992) Symbolic model checking: 1020 states and beyond. Inf Comput 98(2):142\u2013170","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"Burkart O, Caucal D, Moller F, Steffen B (2001) Verification of infinite structures. In: Handbook of process algebra. Elsevier Science, pp 545\u2013623","DOI":"10.1016\/B978-044482830-9\/50027-8"},{"key":"19_CR21","unstructured":"B\u00fcchi J (1960) On a decision method in restricted second order arithmetic. In: Nagel E (ed) International Congress on logic, methodology and philosophy of science. Stanford University Press, Stanford, CA, pp 1\u201312"},{"key":"19_CR22","unstructured":"Cabodi G, Camurati P, Quer S (2002) Can BDDs compete with SAT solvers on bounded model checking? In: International design automation conference (DAC). ACM, New Orleans, Louisiana, USA, pp 117\u2013122"},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"Clarke E, Biere A, Raimi R, Zhu Y (2001) Bounded model checking using satisfiability solving. Form Meth Syst Desi 19(1):7\u201334","DOI":"10.1023\/A:1011276507260"},{"key":"19_CR24","unstructured":"Clarke E, Emerson E (1981) Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen D (ed) Workshop on logics of programs. LNCS, vol 131. Springer, Yorktown Heights, New York, pp 52\u201371"},{"key":"19_CR25","doi-asserted-by":"crossref","unstructured":"Clarke E, Grumberg O, Hamaguchi K (1994) Another look at LTL model checking. In: Dill D (ed) Conference on computer aided verification (CAV). LNCS, vol 818. Springer, Stanford, California, USA, pp 415\u2013427","DOI":"10.1007\/3-540-58179-0_72"},{"key":"19_CR26","unstructured":"Clarke E, Grumberg O, Peled D (1999) Model checking. MIT, London, England"},{"key":"19_CR27","doi-asserted-by":"crossref","unstructured":"Clarke E, Kroening D, Ouaknine J, Strichman O (2004) Completeness and complexity of bounded model checking. In: Steffen B, Levi G (eds) Verification, model checking, and abstract interpretation (VMCAI). LNCS, vol 2937. Springer, Venice, Italy, pp 85\u201396","DOI":"10.1007\/978-3-540-24622-0_9"},{"key":"19_CR28","doi-asserted-by":"crossref","unstructured":"Clarke E, Wing J (1996) Formal methods: state of the art and future directions. ACM Comput Surv, 28(4):626\u2013643","DOI":"10.1145\/242223.242257"},{"key":"19_CR29","unstructured":"Cleaveland R (1989) Tableaux-based model checking in the propositional \u03bc-calculus. Acta Informatica 27(8):725\u2013747"},{"key":"19_CR30","unstructured":"Cormen T, Leiserson C, Rivest R, Stein C (2001) Introduction to algorithms. The MIT Press"},{"key":"19_CR31","doi-asserted-by":"crossref","unstructured":"de Moura L, Rue\u00df H, Sorea M (2002) Lazy theorem proving for bounded model checking over infinite domains. In: Conference on automated deduction (CADE). LNCS, vol 2392. Springer Verlag, Copenhagen, Denmark, pp 438\u2013455","DOI":"10.1007\/3-540-45620-1_35"},{"key":"19_CR32","doi-asserted-by":"crossref","unstructured":"Emerson E (1997) Model checking and the \u03bc-calculus. In: Immerman N, Kolaitis P (eds) Symposium on descriptive complexity and finite models. American Mathematical Society (AMS), pp 185\u2013214","DOI":"10.1090\/dimacs\/031\/06"},{"key":"19_CR33","unstructured":"Enderton H (1972) A mathematical introduction to logic. Academic, New York, NY"},{"key":"19_CR34","doi-asserted-by":"crossref","unstructured":"Esparza J (2003) An automata-theoretic approach to software verification. In: Developments in language theory. LNCS, vol 2710. Springer, pp 21","DOI":"10.1007\/3-540-45007-6_2"},{"key":"19_CR35","doi-asserted-by":"crossref","unstructured":"Ganesh V, Berezin S, Dill D (2002) Deciding Presburger arithmetic by model checking and comparisons with other methods. In: Aagaard M, O'Leary J (eds) Conference on formal methods in computer aided design (FMCAD). LNCS, vol 2517. Springer, Portland, USA, pp 171\u2013186","DOI":"10.1007\/3-540-36126-X_11"},{"key":"19_CR36","doi-asserted-by":"crossref","unstructured":"Gerth R, Peled D, Vardi M, Wolper P (1995) Simple on-the-fly automatic verification of linear temporal logic. In: Symposium on protocol specification, testing, and verification (PSTV). Warsaw, North Holland","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"19_CR37","doi-asserted-by":"crossref","unstructured":"Goldberg E, Novikov Y (2002) BerkMin: a fast and robust SAT-solver. In: Design, automation and test in Europe (DATE). IEEE Computer Society, Paris, France, pp 143\u2013149","DOI":"10.1109\/DATE.2002.998262"},{"key":"19_CR38","doi-asserted-by":"crossref","unstructured":"Gr\u00e4del E, Kolaitis P, Vardi M (1997) On the decision problem for two-variable first-order logic. The Bulletin of Symbolic Logic 3(1):53\u201369","DOI":"10.2307\/421196"},{"key":"19_CR39","doi-asserted-by":"crossref","unstructured":"Gr\u00e4del E, Rosen E (1999) Preservation theorems for two-variable logic. Mathe Log Quart 45:315\u2013325","DOI":"10.1002\/malq.19990450304"},{"key":"19_CR40","doi-asserted-by":"crossref","unstructured":"Kesten Y, Pnueli A, Raviv L (1998) Algorithmic verification of linear temporal logic specifications. In: Colloquium on automata, languages and programming (ICALP). LNCS, vol 1443. Springer, Aalborg, Denmark, pp 1\u201316","DOI":"10.1007\/BFb0055036"},{"key":"19_CR41","unstructured":"Kleene S (1952) Introduction to metamathematics. North Holland"},{"key":"19_CR42","doi-asserted-by":"crossref","unstructured":"Krishnan S, Puri A, Brayton R (1994) Deterministic \u03c9-automata vis-a-vis deterministic B\u00fcchi automata. In: Symposium on algorithms and computation (ISAAC). LNCS, vol 834. Springer, Beijing, China, pp 378\u2013386","DOI":"10.1007\/3-540-58325-4_202"},{"key":"19_CR43","doi-asserted-by":"crossref","unstructured":"Kukula J, Shiple T, Aziz A (1998) Techniques for implicit state enumeration of EFSMs. In: Gopalakrishnan G, Windley P (eds) Conference on formal methods in computer aided design (FMCAD). LNCS, vol 1522. Springer, Palo Alto, California, USA, pp 469\u2013482","DOI":"10.1007\/3-540-49519-3_30"},{"key":"19_CR44","doi-asserted-by":"crossref","unstructured":"Landweber L (1969) Decision problems for \u03c9-automata. Mathe Syst Theory 3(4):376\u2013384","DOI":"10.1007\/BF01691063"},{"key":"19_CR45","doi-asserted-by":"crossref","unstructured":"Lichtenstein O, Pnueli A (1985) Checking that finite state concurrent programs satisfy their linear specification. In: Symposium on principles of programming languages (POPL). ACM, New York, pp 97\u2013107","DOI":"10.1145\/318593.318622"},{"key":"19_CR46","doi-asserted-by":"crossref","unstructured":"Malik S (1993) Analysis of cyclic combinational circuits. In: Conference on computer aided design (ICCAD). IEEE Computer Society, Santa Clara, California, pp 618\u2013625","DOI":"10.1109\/ICCAD.1993.580150"},{"key":"19_CR47","unstructured":"Manna Z, Pnueli A (1988) The anchored version of the temporal framework. In: Linear time, branching time and partial order in logics and models for concurrency. LNCS, vol 354. Springer, Noordwigherhout, Netherland, pp 428\u2013437"},{"key":"19_CR48","doi-asserted-by":"crossref","unstructured":"Manna Z, Pnueli A (1990) A hierarchy of temporal properties. In: Symposium on principles of distributed computing (PODC), pp 377\u2013408","DOI":"10.1145\/93385.93442"},{"key":"19_CR49","doi-asserted-by":"crossref","unstructured":"Marques Silva J, Sakallah K (1999) Grasp: a search algorithm for propositional satisfiability. IEEE Trans Comput 48(5):506\u2013521","DOI":"10.1109\/12.769433"},{"key":"19_CR50","unstructured":"McNaughton R, Papert S (1971) Counter-free automata. MIT"},{"key":"19_CR51","doi-asserted-by":"crossref","unstructured":"Meinel C, Theobald T (1998) Algorithms and data structures in VLSI design: OBDD\u2014foundations and applications. Springer","DOI":"10.1007\/978-3-642-58940-9"},{"key":"19_CR52","doi-asserted-by":"crossref","unstructured":"Mortimer M (1975) On languages with two variables. Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik 21:135\u2013140","DOI":"10.1002\/malq.19750210118"},{"key":"19_CR53","doi-asserted-by":"crossref","unstructured":"Moskewicz M, Madigan C, Zhao Y, Zhang L, Malik S (2001) Chaff: Engineering an efficient SAT solver. In: International design automation conference (DAC). ACM, Las Vegas, Nevada, USA, pp 530\u2013535","DOI":"10.1145\/378239.379017"},{"key":"19_CR54","doi-asserted-by":"crossref","unstructured":"Muller D, Saoudi A, Schupp P (1988) Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In: Symposium on logic in computer science (LICS), pp 422\u2013427","DOI":"10.1109\/LICS.1988.5139"},{"key":"19_CR55","doi-asserted-by":"crossref","unstructured":"Oppen D (1978) A $$2^{2^{2^{pn}}}$$ upper bound on the complexity of Presburger arithmetic. Comput Syst Sci 16:323\u2013332","DOI":"10.1016\/0022-0000(78)90021-1"},{"key":"19_CR56","doi-asserted-by":"crossref","unstructured":"Owicki S, Gries D (1976) An axiomatic proof technique for parallel programs I. Acta Informatica 6(4):319\u2013340","DOI":"10.1007\/BF00268134"},{"key":"19_CR57","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: Symposium on foundations of computer science (FOCS), vol 18. IEEE Computer Society, New York, pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"19_CR58","unstructured":"Presburger M (1930) \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Leja F (ed) Sprawozdanie z I Kongresu Matematyk\u00f3w Kraj\u00f3w S\u0142owia\u0144skich, Warszawa 1929 (Comptes\u2013rendus du I Congr\u00e8s des Math\u00e9maticiens des Pays Slaves, Varsovie 1929). Warszawa, pp 92\u2013101 (supplement on p 395)"},{"key":"19_CR59","doi-asserted-by":"crossref","unstructured":"Quielle J, Sifakis J (1981) Specification and verification of concurrent systems in CESAR. In: Symposium on programming","DOI":"10.1007\/3-540-11494-7_22"},{"key":"19_CR60","doi-asserted-by":"crossref","unstructured":"Reps T, Sagiv M, Wilhelm R (2004) Static program analysis via 3-valued logic. In: Alur R, Peled D (eds) Conference on computer aided verification (CAV). LNCS, vol 3114. Springer, Boston, MA, USA, pp 15\u201330","DOI":"10.1007\/978-3-540-27813-9_2"},{"key":"19_CR61","unstructured":"Schneider K (2000) A verified hardware synthesis for Esterel. In: Rammig F (ed) Workshop on distributed and parallel embedded systems (DIPES). Kluwer, Schlo\u00df Ehringerfeld, Germany, pp 205\u2013214"},{"key":"19_CR62","doi-asserted-by":"crossref","unstructured":"Schneider K (2001) Embedding imperative synchronous languages in interactive theorem provers. In: Conference on application of concurrency to system design (ACSD). IEEE Computer Society, Newcastle upon Tyne, UK, pp 143\u2013156","DOI":"10.1109\/CSD.2001.981772"},{"key":"19_CR63","doi-asserted-by":"crossref","unstructured":"Schneider K (2001) Improving automata generation for linear temporal logic by considering the automata hierarchy. In: International conference on logic for programming, artificial intelligence, and reasoning (LPAR). LNAI, vol 2250. Springer, Havanna, Cuba, pp 39\u201354","DOI":"10.1007\/3-540-45653-8_3"},{"key":"19_CR64","doi-asserted-by":"crossref","unstructured":"Schneider K (2002) Proving the equivalence of microstep and macrostep semantics. In: Carre\u00f1o V, Mu\u00f1oz C, Tahar S (eds) Higher order logic theorem proving and its applications (TPHOL). LNCS, vol 2410. Springer, Hampton, VA, USA, pp 314\u2013331","DOI":"10.1007\/3-540-45685-6_21"},{"key":"19_CR65","unstructured":"Schneider K (2003) Verification of reactive systems\u2014formal methods and algorithms. Texts in theoretical computer science (EATCS Series), Springer"},{"key":"19_CR66","doi-asserted-by":"crossref","unstructured":"Schneider K, Brandt J, Schuele T, Tuerk T (2005) Maximal causality analysis. In: Conference on application of concurrency to system design (ACSD). IEEE Computer Society, St. Malo, France, pp 106\u2013115","DOI":"10.1109\/ACSD.2005.24"},{"key":"19_CR67","unstructured":"Schneider K, Kumar R, Kropf T (1993) Alternative proof procedures for finite-state machines in higher-order logic. In: Joyce J, Seger C-J (eds) Higher order logic theorem proving and its applications (TPHOL). LNCS, vol 780. Springer, Vancouver, Canada, pp 213\u2013226"},{"key":"19_CR68","doi-asserted-by":"crossref","unstructured":"Schuele T, Schneider K (2004) Bounded model checking of infinite state systems: exploiting the automata hierarchy. In: Formal methods and models for codesign (MEMOCODE). IEEE, San Diego, CA, pp 17\u201326","DOI":"10.1109\/MEMCOD.2004.1459809"},{"key":"19_CR69","unstructured":"Schuele T, Schneider K (2004) Global vs. local model checking: a comparison of verification techniques for infinite state systems. In: International conference on software engineering and formal methods (SEFM). IEEE, Beijing, China, pp 67\u201376"},{"key":"19_CR70","doi-asserted-by":"crossref","unstructured":"Sheeran M, Singh S, St\u00e5lmarck G (2000) Checking safety properties using induction and a SAT-solver. In: Hunt W, Johnson S (eds) Conference on formal methods in computer aided design (FMCAD). LNCS, vol 1954. Springer, Austin, Texas, USA, pp 108\u2013125","DOI":"10.1007\/3-540-40922-X_8"},{"key":"19_CR71","unstructured":"Shiple T (1996) Formal analysis of synchronous circuits. PhD thesis, University of California at Berkeley"},{"key":"19_CR72","doi-asserted-by":"crossref","unstructured":"Shiple T, Kukula J, Ranjan R (1998) A comparison of Presburger engines for EFSM reachability. In: Hu A, Vardi M (eds) Conference on computer aided verification (CAV). LNCS, vol 1427. Springer, Vancouver, BC, Canada, pp 280\u2013292","DOI":"10.1007\/BFb0028752"},{"key":"19_CR73","doi-asserted-by":"crossref","unstructured":"Somenzi F (2001) Efficient manipulation of decision diagrams. Softw Tools Technol Trans (STTT) 3(2):171\u2013181","DOI":"10.1007\/s100090100042"},{"key":"19_CR74","doi-asserted-by":"crossref","unstructured":"Stirling C, Walker D (1989) Local model checking in the modal \u03bc-calculus. In: Diaz J, Orejas F (eds) Theory and practice of software development (TAPSOFT). LNCS, vol 351. Springer, pp 369\u2013383","DOI":"10.1007\/3-540-50939-9_144"},{"key":"19_CR75","doi-asserted-by":"crossref","unstructured":"Stirling C, Walker D (1991) Local model checking in the modal \u03bc-calculus. Theor Comput Sci 89(1):161\u2013177","DOI":"10.1016\/0304-3975(90)90110-4"},{"key":"19_CR76","doi-asserted-by":"crossref","unstructured":"Tarski A (1955) A lattice-theoretical fixpoint theorem and its applications. Pacific J Math 5:285\u2013309","DOI":"10.2140\/pjm.1955.5.285"},{"key":"19_CR77","doi-asserted-by":"crossref","unstructured":"Thomas W (1990) Automata on infinite objects, vol B, chapter automata on infinite objects, Elsevier, pp 133\u2013191","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"19_CR78","unstructured":"Thomas W (2001) A short introduction to infinite automata. In: Conference on developments in language theory. LNCS, vol 2295. Springer, pp 130\u2013144"},{"key":"19_CR79","unstructured":"Tuerk T, Schneider K (2005) Relationship between alternating omega-automata and symbolically represented nondeterministic omega-automata. Internal Report 340, Department of Computer Science, University of Kaiserslautern, http:\/\/kluedo.ub.uni-kl.de"},{"key":"19_CR80","doi-asserted-by":"crossref","unstructured":"Vardi M (1994) Nontraditional applications of automata theory. In: Symposium on theoretical aspects of computer science (STACS). LNCS, vol 789. Springer, Sendai, Japan, pp 575\u2013597","DOI":"10.1007\/3-540-57887-0_116"},{"key":"19_CR81","unstructured":"Vardi M (1996) Why is modal logic so robustly decidable? In: Descriptive complexity and finite models, no 31 in DIMACS workshop. American Mathematical Society (AMS), pp 149\u2013184"},{"key":"19_CR82","doi-asserted-by":"crossref","unstructured":"Wagner K (1979) On \u03c9-regular sets. Inform Contr 43:123\u2013177","DOI":"10.1016\/S0019-9958(79)90653-3"},{"key":"19_CR83","doi-asserted-by":"crossref","unstructured":"Wolper P (1983) Temporal logic can be more expressive. Inform Contr 56(1\u20132):72\u201399","DOI":"10.1016\/S0019-9958(83)80051-5"},{"key":"19_CR84","doi-asserted-by":"crossref","unstructured":"Wolper P (2001) Constructing automata from temporal logic formulas: A tutorial. In: Summer school on formal methods in performance analysis. LNCS, vol 2090. Springer, pp 261\u2013277","DOI":"10.1007\/3-540-44667-2_7"},{"key":"19_CR85","doi-asserted-by":"crossref","unstructured":"Wolper P, Boigelot B (2000) On the construction of automata from linear arithmetic constraints. In: Graf S, Schwartzbach M (eds) Conference on tools and algorithms for the construction and analysis of systems (TACAS). LNCS, vol 1785. Springer, Berlin, Germany, pp 1\u201319","DOI":"10.1007\/3-540-46419-0_1"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-0019-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-006-0019-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-0019-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,8]],"date-time":"2023-05-08T18:37:38Z","timestamp":1683571058000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-006-0019-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,8,31]]},"references-count":85,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2006,11,3]]}},"alternative-id":["19"],"URL":"https:\/\/doi.org\/10.1007\/s10703-006-0019-9","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,8,31]]}}}