{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,12,19]],"date-time":"2024-12-19T05:29:17Z","timestamp":1734586157975,"version":"3.30.2"},"reference-count":38,"publisher":"Elsevier BV","issue":"6","license":[{"start":{"date-parts":[[2002,6,1]],"date-time":"2002-06-01T00:00:00Z","timestamp":1022889600000},"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":4076,"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":[[2002,6]]},"DOI":"10.1016\/s1571-0661(04)80468-7","type":"journal-article","created":{"date-parts":[[2004,9,28]],"date-time":"2004-09-28T19:29:25Z","timestamp":1096399765000},"page":"47-59","source":"Crossref","is-referenced-by-count":20,"title":["Verification of Asynchronous Circuits using Timed Automata"],"prefix":"10.1016","volume":"65","author":[{"given":"Marius","family":"Bozga","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hou","family":"Jianmin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oded","family":"Maler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sergio","family":"Yovine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB1","doi-asserted-by":"crossref","unstructured":"R. Alur, Timed Automata, Proc. CAV'99 LNCS 1633, 8\u201322, Springer, 1999.","DOI":"10.1007\/3-540-48683-6_3"},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB2","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":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB3","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1006\/inco.1995.1059","article-title":"Timing Verification by Successive Approximation","volume":"118","author":"Alur","year":"1995","journal-title":"Information and Computation"},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB4","doi-asserted-by":"crossref","unstructured":"E. Asarin, O. Maler and A. Pnueli, On the Discretization of Delays in Timed Automata and Digital Circuits, in R. de Simone and D. Sangiorgi (Eds), Proc. Concur'98, LNCS 1466, 470\u2013484, Springer, 1998.","DOI":"10.1007\/BFb0055642"},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB5","doi-asserted-by":"crossref","unstructured":"F. Balarin, Approximate Reachability Analysis of Timed Automata, Proc. RTSS'96, 52\u201361, IEEE, 1996.","DOI":"10.1109\/REAL.1996.563700"},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB6","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1109\/32.75415","article-title":"Modeling and Verification of Time Dependent Systems using Time Petri Nets","volume":"17","author":"Berthomieu","year":"1991","journal-title":"IEEE Trans. on Software Engineering"},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB7","doi-asserted-by":"crossref","unstructured":"W. Belluomini and C.J. Myers, Verification of Timed Systems Using POSETs, in A.J. Hu and M.Y. Vardi (Eds.), Proc. CAV'98, 403\u2013415, LNCS 1427, Springer, 1997.","DOI":"10.1007\/BFb0028762"},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB8","doi-asserted-by":"crossref","unstructured":"M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, and S. Yovine, Kronos: a Model-Checking Tool for Real-Time Systems, Proc. CAV'98, LNCS 1427, Springer, 1998.","DOI":"10.1007\/BFb0055357"},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB9","doi-asserted-by":"crossref","unstructured":"M. Bozga, O. Maler, A. Pnueli, S. Yovine, Some Progress in the Symbolic Verification of Timed Automata, in O. Grumberg (Ed.) Proc. CAV'97, 179\u2013190, LNCS 1254, Springer, 1997.","DOI":"10.1007\/3-540-63166-6_19"},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB10","series-title":"Proc. CHARME'99","first-page":"125","article-title":"Efficient Verification of Timed Automata using Dense and Discrete Time Semantics","author":"Bozga","year":"1999"},{"year":"1994","series-title":"Asynchronous Circuits","author":"Brzozowski","key":"10.1016\/S1571-0661(04)80468-7_NEWBIB11"},{"issue":"No. 3","key":"10.1016\/S1571-0661(04)80468-7_NEWBIB12","first-page":"315","article-title":"Petrify: a tool for manipulating concurrent specifications and synthesis of asynchronous controllers","volume":"Vol. E80-D","author":"Cortadella","year":"1997","journal-title":"IEICE Transactions on Information and Systems"},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB13","doi-asserted-by":"crossref","unstructured":"J. Cortadella, M. Kishinevsky, A. Kondratyev, L. Lavagno, A. Taubin and A. Yakovlev, Lazy Transition Systems: Application to Timing Optimization of Asynchronous Circuits, in Proc. ICCAD'98, 324\u2013331, 1998.","DOI":"10.1145\/288548.288633"},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB14","series-title":"Automatic Verification Methods for Finite State Systems","first-page":"197","article-title":"Timing Assumptions and Verification of Finite-State Concurrent Systems","author":"Dill","year":"1989"},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB15","series-title":"\u201cHybrid Systems III, Verification and Control\u201d","article-title":"The tool Kronos","author":"Daws","year":"1996"},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB16","doi-asserted-by":"crossref","unstructured":"H. Hulgaard and S.M. Burns, Efficient Timing Analysis of a Class of Petri Nets, Proc. CAV'95, 1995.","DOI":"10.1007\/3-540-60045-0_67"},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB17","unstructured":"H. Kim and P.A. Beerel, Relative Timing Based Verification of Timed Circuits and Systems, Proc. IWLS'99, June 1999."},{"year":"1993","series-title":"Concurrent Hardware: The Theory and Practice of Self-Timed Design","author":"Kishinevsky","key":"10.1016\/S1571-0661(04)80468-7_NEWBIB18"},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB19","article-title":"UPPAAL in a Nutshell","volume":"1\/2","author":"Larsen","year":"1997","journal-title":"Software Tools for Technology Transfer"},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB20","unstructured":"H.R. Lewis, Finite-state Analysis of Asynchronous Circuits with Bounded Temporal Uncertainty, TR15-89, Harvard University, 1989."},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB21","doi-asserted-by":"crossref","unstructured":"O. Maler and A. Pnueli, Timing Analysis of Asynchronous Circuits using Timed Automata, in P.E. Camurati, H. Eveking (Eds.), Proc. CHARME'95, LNCS 987, 189\u2013205, Springer, 1995.","DOI":"10.1007\/3-540-60385-9_12"},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB22","doi-asserted-by":"crossref","unstructured":"O. Maler and S. Yovine, Hardware Timing Verification using KRONOS, In Proc. 7th Israeli Conference on Computer Systems and Software Engineering, Herzliya, Israel, June 1996.","DOI":"10.1109\/ICCSSE.1996.554845"},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB23","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1109\/92.238425","article-title":"Synthesis of Timed Asynchronous Circuits","volume":"1","author":"Myers","year":"1993","journal-title":"IEEE Transactions on VLSI Systems"},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB24","unstructured":"D.E. Muller and W.S. Bartky, A theory of Asynchronous Circuits, in Proc. of an Int. Symposium on the Theory of Switching, 204\u2013243, Harvard University Press, 1959."},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB25","doi-asserted-by":"crossref","unstructured":"M.A. Pena, J. Cortadella, A. Kondratyev and E. Pastor, Formal Verification of Safety Properties in Timed Circuits, Proc. Async'00, 2\u201311, IEEE Press, 2000.","DOI":"10.1109\/ASYNC.2000.836774"},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB26","doi-asserted-by":"crossref","unstructured":"T.G. Rokicki and C.J. Myers, Automatic Verification of Timed Circuits, Proc. CAV'94, June, 1994.","DOI":"10.1007\/3-540-58179-0_76"},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB27","unstructured":"A. Semenov and A. Yakovlev, Verification of Asynchronous Circuits based on Timed Petri Net Unfolding, Proc. TAU'95, 199\u2013210, 1995."},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB28","doi-asserted-by":"crossref","unstructured":"K.S. Stevens, R. Ginosar, and S. Rotem, Relative Timing, Proc. Async'99, 1999.","DOI":"10.1109\/ASYNC.1999.761535"},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB29","doi-asserted-by":"crossref","unstructured":"E.M. Sentovich, K.J. Singh, L. Lavagno, C. Moon, R. Murgai, A. Saldanha, H. Savoj, P.R. Stephan, R.K. Brayton and A. Sangiovanni-Vincentelli, SIS: A System for Sequential Circuit Synthesis, Technical Report UCB\/ERL M92\/41, University of California, Berkeley, May 1992.","DOI":"10.1109\/ICCD.1992.276282"},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB30","doi-asserted-by":"crossref","unstructured":"S. Tasiran, R. Alur, R.P. Kurshan and R. Brayton, Verifying Abstractions of Timed Systems, in Proc. CONCUR'96, 546\u2013562, Springer, 1996.","DOI":"10.1007\/3-540-61604-7_75"},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB31","doi-asserted-by":"crossref","unstructured":"S. Tasiran and R.K. Brayton, STARI: A Case Study in Compositional and Hierarchical Timing Verification, in O. Grumberg (Ed.) Proc. CAV'97, 191\u2013201, LNCS 1254, Springer, 1997.","DOI":"10.1007\/3-540-63166-6_20"},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB32","unstructured":"S. Tasiran, Y. Kukimoto and R.K. Brayton, Computing Delay with Coupling using Timed Automata, Proc. TAU'97, 1997."},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB33","doi-asserted-by":"crossref","unstructured":"S. Tasiran, S. P. Khatri, S. Yovine, R.K. Brayton and A. Sangiovanni-Vincentelli, A Timed Automaton-Based Method for Accurate Computation of Circuit Delay in the Presence of Cross-Talk, FMCAD'98, 1998.","DOI":"10.1007\/3-540-49519-3_11"},{"year":"1969","series-title":"Asynchronous Sequential Switching Circuits","author":"Unger","key":"10.1016\/S1571-0661(04)80468-7_NEWBIB34"},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB35","series-title":"Theories and Experiences for Real-Time System Development","article-title":"Approximations for Verifying Timing Properties","author":"Wong-Toi","year":"1994"},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB36","doi-asserted-by":"crossref","unstructured":"T. Yoneda and H. Ryu, Timed Trace Theoretic Verication using Partial Order Reduction, Proc. Async'99, 108\u2013121, IEEE, 1999.","DOI":"10.1109\/ASYNC.1999.761527"},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB37","series-title":"Lectures on Embedded Systems","article-title":"Model-checking timed automata","author":"Yovine","year":"1998"},{"key":"10.1016\/S1571-0661(04)80468-7_NEWBIB38","doi-asserted-by":"crossref","unstructured":"H. Zheng and C.J. Myers, Automatic Abstraction for Synthesis and Verification of Deterministic Timed Systems, Proc. TAU'2000, December, 2000.","DOI":"10.1007\/3-540-44585-4_16"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104804687?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104804687?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2024,12,18]],"date-time":"2024-12-18T19:37:30Z","timestamp":1734550650000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104804687"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,6]]},"references-count":38,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2002,6]]}},"alternative-id":["S1571066104804687"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80468-7","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[2002,6]]}}}