{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,7]],"date-time":"2026-05-07T02:44:48Z","timestamp":1778121888555,"version":"3.51.4"},"reference-count":26,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[1999,6,1]],"date-time":"1999-06-01T00:00:00Z","timestamp":928195200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":5160,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[1999,6]]},"DOI":"10.1016\/s0304-3975(99)00038-9","type":"journal-article","created":{"date-parts":[[2003,4,7]],"date-time":"2003-04-07T15:40:02Z","timestamp":1049730002000},"page":"369-392","source":"Crossref","is-referenced-by-count":73,"title":["Discrete-time control for rectangular hybrid automata"],"prefix":"10.1016","volume":"221","author":[{"given":"Thomas A.","family":"Henzinger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter W.","family":"Kopke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(99)00038-9_bib1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","article-title":"The algorithmic analysis of hybrid systems","volume":"138","author":"Alur","year":"1995","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(99)00038-9_bib2","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A theory of timed automata","volume":"126","author":"Alur","year":"1994","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(99)00038-9_bib3","series-title":"Proc. CONCUR: Concurrency Theory","first-page":"74","article-title":"Modularity for timed and hybrid systems","volume":"vol. 1243","author":"Alur","year":"1997"},{"key":"10.1016\/S0304-3975(99)00038-9_bib4","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1109\/32.489079","article-title":"Automatic symbolic verification of embedded systems","volume":"22","author":"Alur","year":"1996","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/S0304-3975(99)00038-9_bib5","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1145\/320613.320614","article-title":"On the membership problem for functional and multivalued dependencies in relational databases","volume":"5","author":"Beeri","year":"1980","journal-title":"ACM Trans. Database Systems"},{"key":"10.1016\/S0304-3975(99)00038-9_bib6","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","article-title":"Symbolic model checking: 1020 states and beyond","volume":"98","author":"Burch","year":"1992","journal-title":"Inform. Comput."},{"key":"10.1016\/S0304-3975(99)00038-9_bib7","series-title":"Proc. CAV: Computer-Aided Verification","first-page":"197","article-title":"Minimal model generation","volume":"vol. 531","author":"Bouajjani","year":"1990"},{"key":"10.1016\/S0304-3975(99)00038-9_bib8","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1145\/322234.322243","article-title":"Alternation","volume":"28","author":"Chandra","year":"1981","journal-title":"J. ACM"},{"key":"10.1016\/S0304-3975(99)00038-9_bib9","series-title":"Proc. ICALP: Automata, Languages, and Programming","first-page":"324","article-title":"Hybrid automata with finite bisimulations","volume":"vol. 944","author":"Henzinger","year":"1995"},{"key":"10.1016\/S0304-3975(99)00038-9_bib10","series-title":"Proc. LICS: Logic in Computer Science","first-page":"278","article-title":"The theory of hybrid automata","author":"Henzinger","year":"1996"},{"key":"10.1016\/S0304-3975(99)00038-9_bib11","doi-asserted-by":"crossref","first-page":"540","DOI":"10.1109\/9.664156","article-title":"Algorithmic analysis of nonlinear hybrid systems","volume":"43","author":"Henzinger","year":"1998","journal-title":"IEEE Trans. Automat. Control"},{"key":"10.1016\/S0304-3975(99)00038-9_bib12","first-page":"110","article-title":"HyTech: a model checker for hybrid systems, Software Tools","volume":"1","author":"Henzinger","year":"1997","journal-title":"Technol. Transfer"},{"key":"10.1016\/S0304-3975(99)00038-9_bib13","series-title":"Proc. CONCUR: Concurrency Theory","first-page":"530","article-title":"State equivalences for rectangular hybrid automata","volume":"vol. 1119","author":"Henzinger","year":"1997"},{"key":"10.1016\/S0304-3975(99)00038-9_bib14","series-title":"Proc. STOC: Theory of Computing","first-page":"373","article-title":"What's decidable about hybrid automata?","author":"Henzinger","year":"1995"},{"key":"10.1016\/S0304-3975(99)00038-9_bib15","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1006\/inco.1994.1045","article-title":"Symbolic model checking for real-time systems","volume":"111","author":"Henzinger","year":"1994","journal-title":"Inform. Comput."},{"key":"10.1016\/S0304-3975(99)00038-9_bib16","series-title":"Proc. RTSS: Real-time Systems Symp.","first-page":"256","article-title":"The input-output control of real-time discrete-event systems","author":"Hoffmann","year":"1992"},{"key":"10.1016\/S0304-3975(99)00038-9_bib17","doi-asserted-by":"crossref","first-page":"384","DOI":"10.1016\/0022-0000(81)90039-8","article-title":"Number of quantifiers is better than number of tape cells","volume":"22","author":"Immerman","year":"1981","journal-title":"J. Comput. System Sci."},{"key":"10.1016\/S0304-3975(99)00038-9_bib18","series-title":"Hybrid Systems","first-page":"179","article-title":"Integration graphs: a class of decidable hybrid systems","volume":"vol. 736","author":"Kesten","year":"1993"},{"key":"10.1016\/S0304-3975(99)00038-9_bib19","article-title":"Model checking for branching-time temporal logics","author":"Kupferman","year":"1995"},{"key":"10.1016\/S0304-3975(99)00038-9_bib20","series-title":"Proc. POPL: Principles of Programming Languages","first-page":"97","article-title":"Checking that finite-state concurrent programs satisfy their linear specification","author":"Lichtenstein","year":"1985"},{"key":"10.1016\/S0304-3975(99)00038-9_bib21","series-title":"Proc. STACS: Theoretical Aspects of Computer Science","first-page":"229","article-title":"On the synthesis of discrete controllers for timed systems","volume":"vol. 900","author":"Maler","year":"1995"},{"key":"10.1016\/S0304-3975(99)00038-9_bib22","series-title":"Hybrid Systems III","first-page":"362","article-title":"\u025b-Approximation of differential inclusions","volume":"vol. 1066","author":"Puri","year":"1996"},{"key":"10.1016\/S0304-3975(99)00038-9_bib23","series-title":"Proc. CAV: Computer-Aided Verification","first-page":"95","article-title":"Decidability of hybrid systems with rectangular differential inclusions","volume":"vol. 818","author":"Puri","year":"1994"},{"key":"10.1016\/S0304-3975(99)00038-9_bib24","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1137\/0325013","article-title":"Supervisory control of a class of discrete-event processes","volume":"25","author":"Ramadge","year":"1987","journal-title":"SIAM J. Control Optim."},{"key":"10.1016\/S0304-3975(99)00038-9_bib25","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/BF01691346","article-title":"Generalized finite-automata theory with an application to a decision problem of second-order logic","volume":"2","author":"Thatcher","year":"1968","journal-title":"Math. Systems Theory"},{"key":"10.1016\/S0304-3975(99)00038-9_bib26","series-title":"Proc. STACS: Theoretical Aspects of Computer Science","first-page":"1","article-title":"On the synthesis of strategies in infinite games","volume":"vol. 900","author":"Thomas","year":"1995"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397599000389?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397599000389?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,29]],"date-time":"2019-04-29T03:27:35Z","timestamp":1556508455000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397599000389"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,6]]},"references-count":26,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1999,6]]}},"alternative-id":["S0304397599000389"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(99)00038-9","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[1999,6]]}}}