{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,23]],"date-time":"2025-02-23T05:04:07Z","timestamp":1740287047548,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540201755"},{"type":"electronic","value":"9783540399797"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39979-7_13","type":"book-chapter","created":{"date-parts":[[2010,6,22]],"date-time":"2010-06-22T18:52:22Z","timestamp":1277232742000},"page":"193-208","source":"Crossref","is-referenced-by-count":7,"title":["Can Decision Diagrams Overcome State Space Explosion in Real-Time Verification?"],"prefix":"10.1007","author":[{"given":"Dirk","family":"Beyer","sequence":"first","affiliation":[]},{"given":"Andreas","family":"Noack","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/3-540-48683-6_3","volume-title":"Computer Aided Verification","author":"R. Alur","year":"1999","unstructured":"Alur, R.: Timed automata. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 8\u201322. Springer, Heidelberg (1999)"},{"key":"13_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science\u00a0126, 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"13_CR3","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1006\/inco.1995.1059","volume":"118","author":"R. Alur","year":"1995","unstructured":"Alur, R., Itai, A., Kurshan, R.P., Yannakakis, M.: Timing verification by successive approximation. Information and Computation\u00a0118(1), 142\u2013157 (1995)","journal-title":"Information and Computation"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/3-540-45510-8_4","volume-title":"Modeling and Verification of Parallel Processes","author":"T. Amnell","year":"2001","unstructured":"Amnell, T., Behrmann, G., Bengtsson, J., D\u2019Argenio, P.R., David, A., Fehnker, A., Hune, T., Jeannet, B., Larsen, K.G., M\u00f6ller, M.O., Pettersson, P., Weise, C., Yi, W.: Uppaal - now, next, and future. In: Cassez, F., Jard, C., Rozoy, B., Dermot, M. (eds.) MOVEP 2000. LNCS, vol.\u00a02067, pp. 99\u2013124. Springer, Heidelberg (2001)"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/BFb0055642","volume-title":"CONCUR \u201998 Concurrency Theory","author":"E. Asarin","year":"1998","unstructured":"Asarin, E., Maler, O., Pnueli, A.: On discretization of delays in timed automata and digital circuits. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol.\u00a01466, pp. 470\u2013484. Springer, Heidelberg (1998)"},{"key":"13_CR6","first-page":"283","volume-title":"Proc. DAC 1994","author":"A. Aziz","year":"1994","unstructured":"Aziz, A., Tasiran, S., Brayton, R.K.: BDD variable ordering for interacting finite state machines. In: Proc. DAC 1994, pp. 283\u2013288. ACM Press, New York (1994)"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/3-540-48683-6_30","volume-title":"Computer Aided Verification","author":"G. Behrmann","year":"1999","unstructured":"Behrmann, G., Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Efficient timed reachability analysis using clock difference diagrams. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 341\u2013353. Springer, Heidelberg (1999)"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/3-540-44798-9_6","volume-title":"Correct Hardware Design and Verification Methods","author":"D. Beyer","year":"2001","unstructured":"Beyer, D.: Efficient reachability analysis and refinement checking of timed automata using BDDs. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol.\u00a02144, pp. 86\u201391. Springer, Heidelberg (2001)"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/3-540-45251-6_18","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"D. Beyer","year":"2001","unstructured":"Beyer, D.: Improvements in BDD-based reachability analysis of timed automata. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, pp. 318\u2013343. Springer, Heidelberg (2001)"},{"issue":"9","key":"13_CR10","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1109\/12.537122","volume":"45","author":"B. Bollig","year":"1996","unstructured":"Bollig, B., Wegener, I.: Improving the variable ordering of OBDDs is NP-complete. IEEE Transactions on Computers\u00a045(9), 993\u20131002 (1996)","journal-title":"IEEE Transactions on Computers"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/3-540-63166-6_19","volume-title":"Computer Aided Verification","author":"M. Bozga","year":"1997","unstructured":"Bozga, M., Maler, O., Pnueli, A., Yovine, S.: Some progress in the symbolic verification of timed automata. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 179\u2013190. Springer, Heidelberg (1997)"},{"issue":"8","key":"13_CR12","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transaction on Computers\u00a0C-35(8), 677\u2013691 (1986)","journal-title":"IEEE Transaction on Computers"},{"issue":"4","key":"13_CR13","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1109\/43.275352","volume":"13","author":"J.R. Burch","year":"1994","unstructured":"Burch, J.R., Clarke, E.M., Long, D.E., McMillan, K.L., Dill, D.L.: Symbolic model checking for sequential circuit verification. IEEE Transactions on CAD\u00a013(4), 401\u2013424 (1994)","journal-title":"IEEE Transactions on CAD"},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/3-540-52148-8_17","volume-title":"Automatic Verification Methods for Finite State Systems","author":"D.L. Dill","year":"1990","unstructured":"Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407, pp. 197\u2013212. Springer, Heidelberg (1990)"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"G\u00f6ll\u00fc, A., Puri, A., Varaiya, P.: Discretization of timed automata. In: Proc. Decision and Control, pp. 957\u2013958 (1994)","DOI":"10.1109\/CDC.1994.410933"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1007\/3-540-55719-9_103","volume-title":"Automata, Languages and Programming","author":"A. Thomas","year":"1992","unstructured":"Thomas, A., Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In: Kuich, W. (ed.) ICALP 1992. LNCS, vol.\u00a0623, pp. 545\u2013558. Springer, Heidelberg (1992)"},{"key":"13_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/3-540-48168-0_9","volume-title":"Computer Science Logic","author":"J.B. M\u00f8ller","year":"1999","unstructured":"M\u00f8ller, J.B., Lichtenberg, J., Andersen, H.R., Hulgaard, H.: Difference Decision Diagrams. In: Flum, J., Rodr\u00edguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol.\u00a01683, pp. 111\u2013125. Springer, Heidelberg (1999)"},{"key":"13_CR18","first-page":"235","volume-title":"Proc. FORTE 2001","author":"F. Wang","year":"2001","unstructured":"Wang, F.: Symbolic verification of complex real-time systems with clockrestriction diagram. In: Proc. FORTE 2001, pp. 235\u2013250. Kluwer, Dordrecht (2001)"},{"issue":"1-2","key":"13_CR19","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S. Yovine","year":"1997","unstructured":"Yovine, S.: Kronos: A verification tool for real-time systems. Software Tools for Technology Transfer\u00a01(1-2), 123\u2013133 (1997)","journal-title":"Software Tools for Technology Transfer"},{"key":"13_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/3-540-65193-4_20","volume-title":"Lectures on Embedded Systems","author":"S. Yovine","year":"1998","unstructured":"Yovine, S.: Model checking timed automata. In: Rozenberg, G. (ed.) EEF School 1996. LNCS, vol.\u00a01494, pp. 114\u2013152. Springer, Heidelberg (1998)"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Networked and Distributed Systems - FORTE 2003"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39979-7_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T04:47:23Z","timestamp":1740199643000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39979-7_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540201755","9783540399797"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39979-7_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}