{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T10:31:08Z","timestamp":1648981868408},"reference-count":18,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2001,12,1]],"date-time":"2001-12-01T00:00:00Z","timestamp":1007164800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":4258,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2001,12]]},"DOI":"10.1016\/s1571-0661(04)80670-4","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T16:47:47Z","timestamp":1096476467000},"page":"75-87","source":"Crossref","is-referenced-by-count":2,"title":["Model Checking Semi-Continuous Time Models Using BDDs"],"prefix":"10.1016","volume":"23","author":[{"given":"S\u00e9rgio","family":"Campos","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M\u00e1rcio","family":"Teixeira","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marius","family":"Minea","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Kuehlmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Edmund","family":"Clarke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)80670-4_NEWBIB1","series-title":"Proc. 5th Annual IEEE Symp. on Logic in Computer Science","first-page":"414","article-title":"Model-checking for real-time systems","author":"Alur","year":"1990"},{"key":"10.1016\/S1571-0661(04)80670-4_NEWBIB2","series-title":"CONCUR'98: Concurrency Theory. 8th Int. Conf. Proc","first-page":"470","article-title":"On discretization of delays in timed automata and digital circuits","author":"Asarin","year":"1998"},{"key":"10.1016\/S1571-0661(04)80670-4_NEWBIB3","series-title":"Proc. IEEE Int. Conf. on Comput. Design","first-page":"72","article-title":"Verifying the performance of the PCI local bus using symbolic techniques","author":"Campos","year":"1995"},{"key":"10.1016\/S1571-0661(04)80670-4_NEWBIB4","doi-asserted-by":"crossref","unstructured":"S. V. Campos. A Quantitative Approach to the Formal Verification of Real-Time Systems. PhD thesis, School of Computer Science, Carnegie MellonUniv., 1996.","DOI":"10.1007\/3-540-63166-6_46"},{"key":"10.1016\/S1571-0661(04)80670-4_NEWBIB5","series-title":"Proc. Workshop on Industrial-strength Formal Specification Techniques","first-page":"97","article-title":"Timing analysis of industrial real-time systems","author":"Campos","year":"1995"},{"key":"10.1016\/S1571-0661(04)80670-4_NEWBIB6","series-title":"Proc. 15th IEEE Real-Time Systems Symp","first-page":"266","article-title":"Computing quantitative characteristics of finite-state real-time systems","author":"Campos","year":"1994"},{"key":"10.1016\/S1571-0661(04)80670-4_NEWBIB7","series-title":"Logic of Programs: Workshop","first-page":"52","article-title":"Design and synthesis of synchronization skeletons using branching time temporal logic","author":"Clarke","year":"1981"},{"issue":"2","key":"10.1016\/S1571-0661(04)80670-4_NEWBIB8","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","article-title":"Automatic verification of finite-state concurrent systems using temporal logic specifications","volume":"8","author":"Clarke","year":"1986","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/S1571-0661(04)80670-4_NEWBIB9","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1007\/BF01383942","article-title":"Modular abstractions for verifying real-time distributed systems","volume":"2","author":"De-Leon","year":"1993","journal-title":"Formal Methods in System Design"},{"key":"10.1016\/S1571-0661(04)80670-4_NEWBIB10","series-title":"Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems","first-page":"197","article-title":"Timing assumptions and verification of finite-stae concurrent systems","author":"Dill","year":"1989"},{"key":"10.1016\/S1571-0661(04)80670-4_NEWBIB11","series-title":"Proc. 16th IEEE Real-Time Systems Symp","first-page":"56","article-title":"HyTech: the next generation","author":"Henzinger","year":"1995"},{"key":"10.1016\/S1571-0661(04)80670-4_NEWBIB12","series-title":"Automata, Languages and Programming. 19th International Colloquim Proceedings","first-page":"545","article-title":"What good are digital clocks ?","author":"Henzinger","year":"1992"},{"key":"10.1016\/S1571-0661(04)80670-4_NEWBIB13","series-title":"Proc. 7th Annual IEEE Symp. on Logic in Computer Science","first-page":"394","article-title":"Symbolic model checking for real-time systems","author":"Henzinger","year":"1992"},{"key":"10.1016\/S1571-0661(04)80670-4_NEWBIB14","series-title":"Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control","first-page":"265","article-title":"Using HYTECH to synthesize control parameters for a steam boiler","author":"Henzinger","year":"1996"},{"key":"10.1016\/S1571-0661(04)80670-4_NEWBIB15","series-title":"Proc. 16th IEEE Real-Time Systems Symp","first-page":"76","article-title":"Compositional and symbolic model-checking of real-time systems","author":"Larsen","year":"1995"},{"key":"10.1016\/S1571-0661(04)80670-4_NEWBIB16","series-title":"Symbolic Model Checking","author":"McMillan","year":"1993"},{"key":"10.1016\/S1571-0661(04)80670-4_NEWBIB17","doi-asserted-by":"crossref","unstructured":"Tiziano Villa, Howard Wong-Toi, Andrea Balluchi, Joerg Preussig, Alberto Sangiovanni-Vincentelli, and Yosinori Watanabe. Formal verification of an automotive engine controller in cutoff mode. In CDC98: IEEE Conference on Decision and Control, Tampa, Florida, December 1998.","DOI":"10.1109\/CDC.1998.761976"},{"key":"10.1016\/S1571-0661(04)80670-4_NEWBIB18","article-title":"Kronos: A verification tool for real-time systems","volume":"1","author":"Yovine","year":"1997","journal-title":"Springer International Journal of Software Tools for Technology Transfer"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104806704?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104806704?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T07:10:04Z","timestamp":1585897804000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104806704"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,12]]},"references-count":18,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2001,12]]}},"alternative-id":["S1571066104806704"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80670-4","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2001,12]]}}}