{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,5]],"date-time":"2026-01-05T22:13:34Z","timestamp":1767651214691},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540009139"},{"type":"electronic","value":"9783540365808"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36580-x_36","type":"book-chapter","created":{"date-parts":[[2007,12,9]],"date-time":"2007-12-09T12:13:36Z","timestamp":1197202416000},"page":"498-513","source":"Crossref","is-referenced-by-count":48,"title":["Model Checking LTL over Controllable Linear Systems Is Decidable"],"prefix":"10.1007","author":[{"given":"Paulo","family":"Tabuada","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"George J.","family":"Pappas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,3,14]]},"reference":[{"key":"36_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"R. Alur, C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P.H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. Hybrid automata: An algorithmic approach to specification and verification of hybrid systems. Theoretical Computer Science, 138:3\u201334, 1995.","journal-title":"Theoretical Computer Science"},{"key":"36_CR2","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"},{"doi-asserted-by":"crossref","unstructured":"Rajeev Alur, Thomas A. Henzinger, Gerardo Lafferriere, and George J. Pappas. Discrete abstractions of hybrid systems. Proceedings of the IEEE, 88:971\u2013984, 2000.","key":"36_CR3","DOI":"10.1109\/5.871304"},{"key":"36_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/3-540-45351-2_11","volume-title":"Hybrid Systems: Computation and Control","author":"E. Asarin","year":"2001","unstructured":"E. Asarin, G. Schneider, and S. Yovine. On the decidability of the reachability problem for planar differential inclusions. In M. D. Di Benedetto and A. Sangiovanni-Vincentelli, editors, Hybrid Systems: Computation and Control, volume 2034 of Lecture Notes in Computer Science, pages 89\u2013104. Springer-Verlag, 2001."},{"issue":"3","key":"36_CR5","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1016\/S0005-1098(98)00178-2","volume":"35","author":"A. Bemporad","year":"1999","unstructured":"A. Bemporad and M. Morari. Control of systems integrating logic, dynamics and constraints. Automatica, 35(3):407\u2013427, 1999.","journal-title":"Automatica"},{"key":"36_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/3-540-48983-5_9","volume-title":"Hybrid Systems: Computation and Control","author":"M. Broucke","year":"1999","unstructured":"Mireille Broucke. A geometric approach to bisimulation and verification of hybrid systems. In Fritz W. Vaandrager and Jan H. van Schuppen, editors, Hybrid Systems: Computation and Control, volume 1569 of Lecture Notes in Computer Science, pages 61\u201375. Springer-Verlag, 1999."},{"issue":"3","key":"36_CR7","first-page":"173","volume":"6","author":"P. Brunovsky","year":"1970","unstructured":"P. Brunovsky. A classification of linear controllable systems. Kybernetika, 6(3):173\u2013188, 1970.","journal-title":"Kybernetika"},{"unstructured":"Edmund M. M. Clarke, Doron Peled, and Orna Grumberg. Model Checking. MIT Press, 1999.","key":"36_CR8"},{"issue":"4","key":"36_CR9","doi-asserted-by":"publisher","first-page":"564","DOI":"10.1109\/9.664159","volume":"43","author":"J.E.R. Cury","year":"1998","unstructured":"J.E.R. Cury, B.H. Krogh, and T. Niinomi. Synthesis of supervisory controllers for hybrid systems based on approximating automata. IEEE Transactions on Automatic Control: Special Issue on Hybrid Systems, 43(4):564\u2013568, April 1998.","journal-title":"IEEE Transactions on Automatic Control: Special Issue on Hybrid Systems"},{"key":"36_CR10","first-page":"995","volume":"B","author":"E. A. Emerson","year":"1990","unstructured":"E. A. Emerson. Handbook of Theoretical Computer Science, volume B, chapter Temporal and modal logic, pages 995\u20131072. Elsevier Science, 1990.","journal-title":"Handbook of Theoretical Computer Science"},{"key":"36_CR11","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"},{"doi-asserted-by":"crossref","unstructured":"L.C.G.J.M. Habets and J. H. van Schuppen. Control of piecewise-linear hybrid systems on simplices and rectangles. In M. D. Di Benedetto and A. Sangiovanni-Vincentelli, editors, Hybrid Systems: Computation and Control, volume 2034 of Lecture Notes in Computer Sience, pages 261\u2013274. Springer-Verlag, 2001.","key":"36_CR12","DOI":"10.1007\/3-540-45351-2_23"},{"key":"36_CR13","series-title":"Lect Notes Comput Sci","volume-title":"TACAS 2000: Tools and algorithms for the construction and analysis of systems","author":"T.A. Henzinger","year":"2000","unstructured":"T.A. Henzinger and R. Majumdar. Symbolic model checking for rectangular hybrid systems. In S. Graf, editor, TACAS 2000: Tools and algorithms for the construction and analysis of systems, Lecture Notes in Computer Science, New-York, 2000. Springer-Verlag."},{"key":"36_CR14","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"T. A. Henzinger","year":"1998","unstructured":"Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, and Pravin Varaiya. What\u2019s decidable about hybrid automata? Journal of Computer and System Sciences, 57:94\u2013124, 1998.","journal-title":"Journal of Computer and System Sciences"},{"key":"36_CR15","first-page":"459","volume-title":"Ordinary Differential Equations","author":"R. E. Kalman","year":"1972","unstructured":"R. E. Kalman. Kronecker invariants and feedback. In L. Weiss, editor, Ordinary Differential Equations, pages 459\u2013471. Academic Press, New York, 1972."},{"key":"36_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1007\/3-540-44618-4_9","volume-title":"Proceedings of the 11th International Conference on Concurency Theory","author":"O. Kupferman","year":"2000","unstructured":"Orna Kupferman, P. Madhusudan, P. S. Thiagarajan, and Moshe Y. Vardi. Open systems in reactive environments: Control and synthesis. In Proceedings of the 11th International Conference on Concurency Theory, volume 1877 of Lecture Notes in Computer Science, pages 92\u2013107. Springer-Verlag, 2000."},{"issue":"1","key":"36_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/PL00009858","volume":"13","author":"G. Lafferriere","year":"2000","unstructured":"Gerardo Lafferriere, George J. Pappas, and Shankar Sastry. O-minimal hybrid systems. Mathematics of Control, Signals and Systems, 13(1):1\u201321, March 2000.","journal-title":"Mathematics of Control, Signals and Systems"},{"key":"36_CR18","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0304-3975(00)00307-8","volume":"274","author":"P. Madhusudan","year":"2002","unstructured":"P. Madhusudan and P.S. Thiagarajan. Branching time controllers for discrete event systems. Theoretical Computer Science, 274:117\u2013149, March 2002.","journal-title":"Theoretical Computer Science"},{"key":"36_CR19","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/357233.357237","volume":"6","author":"Z. Manna","year":"1984","unstructured":"Z. Manna and P. Wolper. Synthesis of communication processes from temporal logic specifications. ACM Transactions on Programming Languages and Systems, 6:68\u201393, 1984.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","key":"36_CR20","DOI":"10.1007\/978-1-4615-3190-6"},{"unstructured":"R. Milner. Communication and Concurrency. Prentice Hall, 1989.","key":"36_CR21"},{"key":"36_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45351-2_35","volume-title":"Hybrid Systems: Computation and Control","author":"T. Moor","year":"2001","unstructured":"T. Moor and J. M. Davoren. Robust controller synthesis for hybrid systems using modal logic. In M. D. Di Benedetto and A. Sangiovanni-Vincentelli, editors, Hybrid Systems: Computation and Control, volume 2034 of Lecture Notes in Computer Science. Springer-Verlag, 2001."},{"unstructured":"eorge J. Pappas. Bisimilar linear systems. Automatica, 2001. To appear.","key":"36_CR23"},{"key":"36_CR24","series-title":"Lect Notes Comput Sci","volume-title":"Concurrency and automata on infinite sequences","author":"D.M.R. Park","year":"1980","unstructured":"D.M.R. Park. Concurrency and automata on infinite sequences, volume 104 of Lecture Notes in Computer Science. Springer-Verlag, 1980."},{"doi-asserted-by":"crossref","unstructured":"A. Puri and P. Varaiya. Decidability of hybrid systems with rectangular inclusions. In Computer Aided Verification, pages 95\u2013104, 1994.","key":"36_CR25","DOI":"10.1007\/3-540-58179-0_46"},{"key":"36_CR26","volume-title":"Texts in Applied Mathematics","author":"E. D. Sontag","year":"1998","unstructured":"Eduardo D. Sontag. Mathematical Control Theory, volume 6 of Texts in Applied Mathematics. Springer-Verlag, New-York, 2nd edition, 1998.","edition":"2nd edition"},{"key":"36_CR27","doi-asserted-by":"crossref","first-page":"477","DOI":"10.1093\/oso\/9780198537618.003.0005","volume":"2","author":"C. Stirling","year":"1992","unstructured":"Colin Stirling. Handbook of logic in computer science, volume 2, chapter Modal and Temporal Logics, pages 477\u2013563. Oxford University Press, 1992.","journal-title":"Handbook of logic in computer science"},{"issue":"5","key":"36_CR28","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1002\/rnc.593","volume":"11","author":"J.A. Stiver","year":"2001","unstructured":"J.A. Stiver, X.D. Koutsoukos, and P.J. Antsaklis. An invariant based approach to the design of hybrid control systems. International Journal of Robust and Nonlinear Control, 11(5):453\u2013478, 2001.","journal-title":"International Journal of Robust and Nonlinear Control"},{"unstructured":"Paulo Tabuada and George J. Pappas. Finite bisimulations of controllable linear systems. Theoretical Computer Science, January 2003. Submitted, available at http:\/\/www.seas.upenn.edu\/~tabuadap .","key":"36_CR29"}],"container-title":["Lecture Notes in Computer Science","Hybrid Systems: Computation and Control"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36580-X_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,20]],"date-time":"2024-02-20T06:54:01Z","timestamp":1708412041000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36580-X_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540009139","9783540365808"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-36580-x_36","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}