{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,12]],"date-time":"2026-02-12T11:14:41Z","timestamp":1770894881404,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540441656","type":"print"},{"value":"9783540457398","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45739-9_15","type":"book-chapter","created":{"date-parts":[[2007,5,16]],"date-time":"2007-05-16T02:42:01Z","timestamp":1179283321000},"page":"225-243","source":"Crossref","is-referenced-by-count":29,"title":["Verification of Timed Automata via Satisfiability Checking"],"prefix":"10.1007","author":[{"given":"Peter","family":"Niebert","sequence":"first","affiliation":[]},{"given":"Moez","family":"Mahfoudh","sequence":"additional","affiliation":[]},{"given":"Eugene","family":"Asarin","sequence":"additional","affiliation":[]},{"given":"Marius","family":"Bozga","sequence":"additional","affiliation":[]},{"given":"Oded","family":"Maler","sequence":"additional","affiliation":[]},{"given":"Navendu","family":"Jain","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,10,4]]},"reference":[{"key":"15_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"478","DOI":"10.1007\/3-540-44585-4_46","volume-title":"Proc. CAV\u201901","author":"Y. Abdeddam","year":"2001","unstructured":"Y. Abdeddam and O. Maler, Job-Shop Scheduling using Timed Automata Proc. CAV\u201901, 478\u2013492, LNCS 2102, Springer 2001."},{"key":"15_CR2","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1287\/mnsc.34.3.391","volume":"34","author":"J. Adams","year":"1988","unstructured":"J. Adams, E. Balas and D. Zawack, The Shifting Bottleneck Procedure for Job Shop Scheduling, Management Science 34, 391\u2013401, 1988.","journal-title":"Management Science"},{"key":"15_CR3","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"R. Alur and D.L. Dill, A Theory of Timed Automata, Theoretical Computer Science 126, 183\u2013235, 1994.","journal-title":"Theoretical Computer Science"},{"key":"15_CR4","series-title":"Lect Notes Comput Sci","volume-title":"Proc. ECP\u201999","author":"A. Armando","year":"1999","unstructured":"A. Armando, C. Castellini and E. Giunchiglia, SAT-based Procedures for Temporal Reasoning, Proc. ECP\u201999, LNCS, Springer, 1999."},{"key":"15_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/BFb0014737","volume-title":"Proc. Hybrid and Real-Time Systems","author":"E. Asarin","year":"1997","unstructured":"E. Asarin, M. Bozga, A. Kerbrat, O. Maler, A. Pnueli, and A. Rasse, Data Structures for the Verification of Timed Automata, Proc. Hybrid and Real-Time Systems, 346\u2013360, LNCS 1201, Springer, 1997."},{"key":"15_CR6","series-title":"Lect Notes Comput Sci","first-page":"193","volume-title":"Proc. CADE\u201902","author":"G. Audemard","year":"2002","unstructured":"G. Audemard, P. Bertoli, A. Cimatti, A. Kornilowics and R. Sebastiani, ASAT-Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions, in Proc. CADE\u201902, 193\u2013208, LNCS 2392, Springer, 2002."},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"G. Audemard, A. Cimatti, A. Kornilowics and R. Sebastiani, Bounded Model Checking for Timed Systems, Technical report ITC-0201-05, IRST, Trento, 2002.","DOI":"10.1007\/3-540-36135-9_16"},{"key":"15_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"174","DOI":"10.1007\/3-540-45319-9_13","volume-title":"Proc. TACAS 2001","author":"G. Behrmann","year":"2001","unstructured":"G. Behrmann, A. Fehnker T.S. Hune, K.G. Larsen, P. Pettersson and J. Romijn, Efficient Guiding Towards Cost-Optimality in UPPAAL, Proc. TACAS 2001, 174\u2013188, LNCS 2031, Springer, 2001."},{"key":"15_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"485","DOI":"10.1007\/BFb0055643","volume-title":"Proc. Concur\u201998","author":"J. Bengtsson","year":"1998","unstructured":"J. Bengtsson, B. Jonsson, J. Lilius and W. Yi, Partial Order Reductions for Timed Systems, Proc. Concur\u201998, 485\u2013500, LNCS 1466, Springer, 1998."},{"key":"15_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1007\/3-540-48683-6_8","volume-title":"Proc. CAV\u201999","author":"A. Biere","year":"1999","unstructured":"A. Biere, E.M. Clarke, R. Raimi, and Y. Zhu, Verifying Safety Properties of a PowerPC Microprocessor using Symbolic Model Checking without BDDs, Proc. CAV\u201999, 60\u201371, LNCS 1633, Springer, 1999."},{"key":"15_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Proc. TACAS\u201999","author":"A. Biere","year":"1999","unstructured":"A. Biere, A. Cimatti, E.M. Clarke and Y. Zhu, Symbolic Model Checking without BDDs, Proc. TACAS\u201999, 193\u2013207, LNCS 1579, Springer, 1999."},{"key":"15_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"793","DOI":"10.1007\/3-540-45022-X_66","volume-title":"Proc. IC ALP 2000","author":"O. Bournez","year":"2000","unstructured":"O. Bournez and O. Maler, On the Representation of Timed Polyhedra, Proc. IC ALP 2000, 793\u2013807, LNCS 1853, Springer, 2000."},{"key":"15_CR13","series-title":"Lect Notes Comput Sci","volume-title":"Proc. CAV\u201998","author":"M. Bozga","year":"1998","unstructured":"M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, and S. Yovine, Kronos: a Mo del-Checking Tool for Real-Time Systems, Proc. CAV\u201998, LNCS 1427, Springer, 1998."},{"key":"15_CR14","series-title":"Lect Notes Comput Sci","volume-title":"Proc. CAV\u201900","author":"M. Bozga","year":"2000","unstructured":"M. Bozga, J.-C. Fernandez, L. Ghirvu, S. Graf, J.-.P. Krimm and L. Mounier, IF: A Validation Environment for Timed Asynchronous Systems, Proc. CAV\u201900, LNCS, Springer, 2000."},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"M. Bozga, H. Jianmin, O. Maler and S. Yovine, Verification of Asynchronous Circuits using Timed Automata, Proc. TPTS\u201902, 2002.","DOI":"10.1016\/S1571-0661(04)80468-7"},{"key":"15_CR16","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant, Graph-based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers 35, 677\u2013691, 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"J.A. Brzozowski and C-J.H. Seger, Asynchronous Circuits, Springer, 1994.","DOI":"10.1007\/978-1-4612-4210-9"},{"key":"15_CR18","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang, Symbolic Model-Checking: 1020 States and Beyond, Proc. LICS\u201990, IEEE, 1990."},{"key":"15_CR19","unstructured":"T. Cormen, C. Leiserson, R. Rivest, and C. Stein. Introduction to Algorithms. MIT Press, McGraw-Hill, 2001."},{"key":"15_CR20","series-title":"Lect Notes Comput Sci","first-page":"197","volume-title":"Proc. CAV\u201989","author":"D.L. Dill","year":"1989","unstructured":"D.L. Dill, Timing Assumptions and Verification of Finite-State Concurrent Systems, Proc. CAV\u201989, 197\u2013212, LNCS 407, Springer, 1989."},{"key":"15_CR21","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E.A. Emerson","year":"1982","unstructured":"E.A. Emerson and E.M. Clarke, Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons, Science of Computer Programming 2, 241\u2013266, 1982.","journal-title":"Science of Computer Programming"},{"key":"15_CR22","unstructured":"M. Garey and D. Johnson. Computers and Intractability. W. H. Freeman, 1979."},{"key":"15_CR23","unstructured":"J.F. Groote and J.P. Warners. The Propositional Formula Checker Heer-Hugo. Technical Report 691, Centrum voor Wiskunde en Informatica (CWI) Amsterdam, 1999."},{"key":"15_CR24","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T. Henzinger","year":"1994","unstructured":"T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, Symbolic Model-checking for Real-time Systems, Information and Computation 111, 193\u2013244, 1994.","journal-title":"Information and Computation"},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"J. Hooker, Logic-Based Methods for Optimization: Combining Optimization and Constraint Satisfaction, Wiley, 2000","DOI":"10.1002\/9781118033036"},{"key":"15_CR26","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1016\/0743-1066(94)90033-7","volume":"19\/20","author":"J. Jaffar","year":"1994","unstructured":"J. Jaffar and M. J. Maher. Constraint Logic Programming: A Survey, Journal of Logic Programming, 19\/20, 503\u2013581, 1994.","journal-title":"Journal of Logic Programming"},{"key":"15_CR27","first-page":"271","volume":"6","author":"K. Larsen","year":"1999","unstructured":"K. Larsen, J. Pearson, C. Weise, and W. Yi, Clock difference diagrams. Nordic Journal of Computing 6, 271\u2013298, 1999.","journal-title":"Nordic Journal of Computing"},{"key":"15_CR28","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein, A. Pnueli, Checking that Finite-state Concurrent Programs Satisfy their Linear Specification, Proc. POPL\u201984, 97\u2013107, ACM, 1984.","DOI":"10.1145\/318593.318622"},{"key":"15_CR29","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/3-540-60385-9_12","volume-title":"Proc. CHARME\u201995","author":"O. Maler","year":"1995","unstructured":"O. Maler and A. Pnueli, Timing Analysis of Asynchronous Circuits using Timed Automata, Proc. CHARME\u201995, 189\u2013205, LNCS 987, Springer, 1995."},{"key":"15_CR30","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J.P. Marques-Silva","year":"1999","unstructured":"J.P. Marques-Silva and K.A. Sakallah, GRASP: A Search Algorithm for Propositional Satisfiability, IEEE Transactions on Computers 48, 506\u201321, 1999.","journal-title":"IEEE Transactions on Computers"},{"key":"15_CR31","doi-asserted-by":"crossref","unstructured":"K.L. McMillan, Symbolic Model-Checking: an Approach to the State-Explosion problem, Kluwer, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"15_CR32","doi-asserted-by":"crossref","unstructured":"J. M\u00f8ller, J. Lichtenberg, H. Andersen, and H. Hulgaard, Difference Decision Diagrams, Proc. CSL\u201999, 1999.","DOI":"10.1007\/3-540-48168-0_9"},{"key":"15_CR33","doi-asserted-by":"crossref","unstructured":"M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang and S. Malik, Chaff: Engineering an Efficient SAT Solver, Proc. DAC 2001, 2001.","DOI":"10.1145\/378239.379017"},{"key":"15_CR34","series-title":"Lect Notes Comput Sci","first-page":"437","volume-title":"Proc. CADE\u201902","author":"L. Moura de","year":"2002","unstructured":"L. de Moura, H. Rue\u00df and M. Sorea, Lazy Theorem Proving for Bounded Model Checking over Infinite Domains, Proc. CADE\u201902, 437\u2013453, LNCS 2392, Springer, 2002."},{"key":"15_CR35","series-title":"Lect Notes Comput Sci","first-page":"337","volume-title":"Proc. 5th Int. Symp. on Programming","author":"J.P. Queille","year":"1981","unstructured":"J.P. Queille and J. Sifakis, Specification and Verification of Concurrent Systems in Cesar, Proc. 5th Int. Symp. on Programming, 337\u2013351, LNCS 137, Springer, 1981."},{"key":"15_CR36","doi-asserted-by":"crossref","unstructured":"G. St\u00e5lmarck and M. Saflund, Modeling and Verifying Systems and Software in Propositional Logic, Safety of Computer Control Systems (SAFE-COMP\u201990), 31\u201336, Pergamon Press, 1990.","DOI":"10.1016\/B978-0-08-040953-5.50011-8"},{"key":"15_CR37","doi-asserted-by":"crossref","unstructured":"O. Strichman, S.A. Seshia, and R.E. Bryant, Deciding Separation Formulas with SAT, in Proc. CAV\u20192002, Springer, 2002.","DOI":"10.1007\/3-540-45657-0_16"},{"key":"15_CR38","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R. Tarjan","year":"1972","unstructured":"R. Tarjan. Depth-first Search and Linear Graph Algorithms. SIAM J. Comput. 1, 146\u2013160, 1972.","journal-title":"SIAM J. Comput."},{"key":"15_CR39","first-page":"115","volume-title":"Studies in Constructive Mathematics and Mathematical Logic","author":"G. Tseitin","year":"1970","unstructured":"G. Tseitin, On the Complexity of Derivation in Propositional Calculus, in Studies in Constructive Mathematics and Mathematical Logic 2, 115\u2013125, Consultants Bureau, New York, 1970."},{"key":"15_CR40","first-page":"322","volume":"86","author":"M.Y. Vardi","year":"1986","unstructured":"M.Y. Vardi and P. Wolper, An Automata-theoretic Approach to Automatic Program Verification, Proc. LICS\u201986, 322\u2013331, IEEE, 1986.","journal-title":"Proc. LICS\u2019"},{"key":"15_CR41","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S. Yovine","year":"1997","unstructured":"S. Yovine, Kronos: A Verification Tool for Real-time Systems, International Journal of Software Tools for Technology Transfer 1, 123\u2013133, 1997.","journal-title":"International Journal of Software Tools for Technology Transfer"},{"key":"15_CR42","unstructured":"G. Zhang. The Davis-Putnam Resolution Procedure, In Advances in Logic Programming and Automated Reasoning, volume 2. Ablex Publishing Corporation, 1995."}],"container-title":["Lecture Notes in Computer Science","Formal Techniques in Real-Time and Fault-Tolerant Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45739-9_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,11]],"date-time":"2023-05-11T21:32:40Z","timestamp":1683840760000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45739-9_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540441656","9783540457398"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/3-540-45739-9_15","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}