{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,5]],"date-time":"2026-08-05T10:50:10Z","timestamp":1785927010997,"version":"3.56.0"},"reference-count":26,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1995,2,1]],"date-time":"1995-02-01T00:00:00Z","timestamp":791596800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[1995,2,1]],"date-time":"1995-02-01T00:00:00Z","timestamp":791596800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[1999,12,16]],"date-time":"1999-12-16T00:00:00Z","timestamp":945302400000},"content-version":"vor","delay-in-days":1779,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[1995,2]]},"DOI":"10.1016\/0304-3975(94)00202-t","type":"journal-article","created":{"date-parts":[[2003,4,30]],"date-time":"2003-04-30T21:37:28Z","timestamp":1051738648000},"page":"3-34","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":1329,"title":["The algorithmic analysis of hybrid systems"],"prefix":"10.1016","volume":"138","author":[{"given":"R.","family":"Alur","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"C.","family":"Courcoubetis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"N.","family":"Halbwachs","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"T.A.","family":"Henzinger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"P.-H.","family":"Ho","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"X.","family":"Nicollin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"A.","family":"Olivero","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"J.","family":"Sifakis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"S.","family":"Yovine","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"78","reference":[{"key":"10.1016\/0304-3975(94)00202-T_BIB1","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1006\/inco.1993.1024","article-title":"Model checking in dense real time","volume":"104","author":"Alur","year":"1993","journal-title":"Inform. and Comput."},{"key":"10.1016\/0304-3975(94)00202-T_BIB2","series-title":"CONCUR 92: Theories of Concurrency","first-page":"340","article-title":"Minimization of timed transition systems","volume":"Vol. 630","author":"Alur","year":"1992"},{"key":"10.1016\/0304-3975(94)00202-T_BIB3","series-title":"Workshop on Theory of Hybrid Systems","first-page":"209","article-title":"Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems","volume":"Vol. 736","author":"Alur","year":"1993"},{"key":"10.1016\/0304-3975(94)00202-T_BIB4","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\/0304-3975(94)00202-T_BIB5","series-title":"Proc. 1st AMAST Workshop on Real-time Systems","article-title":"Real-time system = discrete system + clock variables","author":"Alur","year":"1994"},{"key":"10.1016\/0304-3975(94)00202-T_BIB6","series-title":"Proc. 14th Ann. Real-time Systems Symposium","first-page":"2","article-title":"Automatic symbolic verification of embedded systems","author":"Alur","year":"1993"},{"key":"10.1016\/0304-3975(94)00202-T_BIB7","series-title":"Proc. 2nd Ann. Workshop on Computer-Aided Verification","first-page":"197","article-title":"Minimal model generation","volume":"Vol. 531","author":"Bouajjani","year":"1990"},{"key":"10.1016\/0304-3975(94)00202-T_BIB8","series-title":"Proc. 4th Ann. Workshop on Computer-Aided Verification","first-page":"269","article-title":"Decidability of bisimulation equivalences for parallel timer processes","volume":"Vol. 663","author":"C\u0306er\u00e3ns","year":"1992"},{"key":"10.1016\/0304-3975(94)00202-T_BIB9","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","article-title":"A calculus of durations","volume":"40","author":"Chaochen","year":"1991","journal-title":"Inform. Processing Lett."},{"key":"10.1016\/0304-3975(94)00202-T_BIB10","series-title":"Proc. 4th Ann. Symp. on Prnciples of Programming Languages","article-title":"Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints","author":"Cousot","year":"1977"},{"key":"10.1016\/0304-3975(94)00202-T_BIB11","series-title":"Proc. 5th Ann. Symp. on Principles of Programming Languages","article-title":"Automatic discovery of linear constraints among variables of a program","author":"Cousot","year":"1978"},{"key":"10.1016\/0304-3975(94)00202-T_BIB12","series-title":"Proc. 5th Ann. Conf. on Computer-Aided Verification","first-page":"333","article-title":"Delay analysis in synchronous programs","volume":"Vol. 697","author":"Halbwachs","year":"1993"},{"key":"10.1016\/0304-3975(94)00202-T_BIB13","series-title":"Proc. Internat. Symp. on Static Analysis","first-page":"223","article-title":"Verification of linear hybrid systems by means of convex approximations","volume":"Vol. 818","author":"Halbwachs","year":"1994"},{"key":"10.1016\/0304-3975(94)00202-T_BIB14","series-title":"Presented at the 7th Internat. Conf. on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems","article-title":"Model-checking strategies for linear hybrid systems","author":"Henzinger","year":"1994"},{"key":"10.1016\/0304-3975(94)00202-T_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. and Comput."},{"key":"10.1016\/0304-3975(94)00202-T_BIB16","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1109\/32.75414","article-title":"Software requirements analysis for real-time process-control systems","volume":"17","author":"Jaffe","year":"1991","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/0304-3975(94)00202-T_BIB17","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\/0304-3975(94)00202-T_BIB18","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/7351.7352","article-title":"A fast mutual-exclusion algorithm","volume":"5","author":"Lamport","year":"1987","journal-title":"ACM Trans. Comput. Systems"},{"key":"10.1016\/0304-3975(94)00202-T_BIB19","series-title":"Proc. 24th Ann. Symp. on Theory of Computing","first-page":"264","article-title":"Online minimization of transition systems","author":"Lee","year":"1992"},{"key":"10.1016\/0304-3975(94)00202-T_BIB20","article-title":"A note on Chernikova's algorithm","author":"LeVerge","year":"1992"},{"key":"10.1016\/0304-3975(94)00202-T_BIB21","series-title":"Proc. REX Workshop Real-Time: Theory in Practice","first-page":"447","article-title":"From timed to hybrid systems","volume":"Vol. 600","author":"Maler","year":"1992"},{"key":"10.1016\/0304-3975(94)00202-T_BIB22","series-title":"Hybrid Systems","first-page":"149","article-title":"An approach to the description and analysis of hybrid systems","volume":"Vol. 736","author":"Nicollin","year":"1993"},{"key":"10.1016\/0304-3975(94)00202-T_BIB23","doi-asserted-by":"crossref","first-page":"794","DOI":"10.1109\/32.159837","article-title":"Compiling real-time specifications into extended automata","volume":"18","author":"Nicollin","year":"1992","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/0304-3975(94)00202-T_BIB24","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1007\/BF01178579","article-title":"From ATP to timed graphs and hybrid systems","volume":"30","author":"Nicollin","year":"1993","journal-title":"Acta Inform."},{"key":"10.1016\/0304-3975(94)00202-T_BIB25","series-title":"Proc. 6th Ann. Conf. on Computer-Aided Verification","first-page":"81","article-title":"Using abstractions for the verification of linear hybrid systems","volume":"Vol. 818","author":"Olivero","year":"1994"},{"key":"10.1016\/0304-3975(94)00202-T_BIB26","series-title":"Proc. 6th Ann. Conf. on Computer-Aided Verification","first-page":"95","article-title":"Decidability of hybrid systems with rectangular differential inclusions","volume":"Vol. 818","author":"Puri","year":"1994"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:030439759400202T?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:030439759400202T?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,9,10]],"date-time":"2025-09-10T04:17:45Z","timestamp":1757477865000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/030439759400202T"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,2]]},"references-count":26,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1995,2]]}},"alternative-id":["030439759400202T"],"URL":"https:\/\/doi.org\/10.1016\/0304-3975(94)00202-t","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[1995,2]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"The algorithmic analysis of hybrid systems","name":"articletitle","label":"Article Title"},{"value":"Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/0304-3975(94)00202-T","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 1995 Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}