{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T00:29:36Z","timestamp":1755217776569,"version":"3.43.0"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2003,7,1]],"date-time":"2003-07-01T00:00:00Z","timestamp":1057017600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,7,1]],"date-time":"2003-07-01T00:00:00Z","timestamp":1057017600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2003,7]]},"DOI":"10.1023\/a:1024437214071","type":"journal-article","created":{"date-parts":[[2003,9,15]],"date-time":"2003-09-15T13:22:37Z","timestamp":1063632157000},"page":"67-108","source":"Crossref","is-referenced-by-count":7,"title":["Symbolic Verification and Analysis of Discrete Timed Systems"],"prefix":"10.1007","volume":"23","author":[{"given":"J\u00fcrgen","family":"Ruf","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Kropf","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"5127650_CR1","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R. Alur","year":"1993","unstructured":"R. Alur, C. Courcoubetis, and D. Dill, \u201cModel checking in dense real time,\u201d Information and Computation, Vol. 104, No. 1, pp. 2\u201334, 1993. Academic Press.","journal-title":"Information and Computation"},{"key":"5127650_CR2","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1007\/BFb0014737","volume-title":"Hybrid and Real-Time Systems","author":"E. Asarin","year":"1997","unstructured":"E. Asarin, M. Bozga, A. Kerbrat, O. Maler, M. Pnueli, and A. Rasse, \u201cData structures for the verification of timed automata,\u201d in O. Maler (Ed.), Hybrid and Real-Time Systems, Grenoble, France, Springer Verlag, LNCS 1201, 1997, pp. 346\u2013360."},{"key":"5127650_CR3","doi-asserted-by":"crossref","unstructured":"R. Bahar, E. Frohm, C. Gaona, G. Hachtel, E. Macii, A. Pardo, and F. Somenzi, \u201cAlgebraic decision diagrams and their applications,\u201d in IEEE\/ACM International Conference on Computer Aided Design (ICCAD), Santa Clara, California, November 1993, pp. 188\u2013191. ACM\/IEEE, IEEE Computer Society Press.","DOI":"10.1109\/ICCAD.1993.580054"},{"key":"5127650_CR4","doi-asserted-by":"crossref","unstructured":"W. Belluomini and C. Myers, \u201cTimed state space exploration using POSETs,\u201d IEEE Transaction on CAD, Vol. 19, No. 5, 2000.","DOI":"10.1109\/43.845076"},{"key":"5127650_CR5","doi-asserted-by":"crossref","unstructured":"J. Bengtsson, K.G. Larsen, F. Larsson, P. Pettersson, and W. Yi, \u201cUppaal\u2014A tool suite for automatic verification of real-time systems,\u201d in Proc. of Workshop on Verification and Control of Hybrid Systems III, Number 1066 in Lecture Notes in Computer Science, Springer-Verlag, October 1995, pp. 232\u2013243.","DOI":"10.1007\/BFb0020949"},{"key":"5127650_CR6","unstructured":"M. Bozga, \u201cSMI: An open toolbox for symbolic protocol verification,\u201d Technical Report, VERIMAG, 1997."},{"key":"5127650_CR7","first-page":"260","volume-title":"IEEE Symposium on Logic in Computer Science (LICS)","author":"M. Browne","year":"1986","unstructured":"M. Browne, \u201cAn improved algorithm for automatic verification of finite-state machines using temporal logic,\u201d in IEEE Symposium on Logic in Computer Science (LICS), Boston, Massachusetts, IEEE Computer Society Press, June 1986, pp. 260\u2013266."},{"issue":"8","key":"5127650_CR8","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. Bryant","year":"1986","unstructured":"R. Bryant, \u201cGraph-based algorithms for boolean function manipulation,\u201d IEEE Transactions on Computers, Vol. C-35, No. 8, pp. 677\u2013691, 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"5127650_CR9","first-page":"1","volume-title":"IEEE Symposium on Logic in Computer Science (LICS)","author":"J. Burch","year":"1990","unstructured":"J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang, \u201cSymbolic model checking: 1020 states and beyond,\u201d in IEEE Symposium on Logic in Computer Science (LICS), Washington, DC, IEEE Computer Society Press, June 1990, pp. 1\u201333."},{"key":"5127650_CR10","doi-asserted-by":"crossref","unstructured":"S. Campos and E. Clarke, \u201cReal-time symbolic model checking for discrete time models,\u201d in T. Rus and C. Rattray (Eds.), Theories and Experiences for Real-Time System Development, AMAST Series in Computing. World Scientific Press, AMAST Series in Computing, May 1994.","DOI":"10.1142\/9789812831583_0005"},{"key":"5127650_CR11","doi-asserted-by":"crossref","unstructured":"S. Campos, E. Clarke, and M. Minea, \u201cThe verus tool: A quantitative approach to the formal verification of real-time systems,\u201d in O. Grumberg, (Ed.), Conference on Computer Aided Verification (CAV), Vol. 1254, pp. 452\u2013455 of Lecture Notes in Computer Science, Springer Verlag, June 1997.","DOI":"10.1007\/3-540-63166-6_46"},{"key":"5127650_CR12","doi-asserted-by":"crossref","unstructured":"E. Clarke, E. Emerson, and A. Sistla, \u201cAutomatic verification of finite-state concurrent systems using temporal logic,\u201d in ACM Symposium on Principles of Programming Languages (POPL), 1983.","DOI":"10.1145\/567067.567080"},{"key":"5127650_CR13","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, D.E. Long, \u201cModel checking,\u201d in Springer-Verlag Nato ASI Series F, Vol. 152, 1996 (A survey on model checking, abstraction and composition).","DOI":"10.1007\/978-3-642-61455-2_16"},{"key":"5127650_CR14","doi-asserted-by":"crossref","unstructured":"E. Clarke, K. McMillian, X. Zhao, M. Fujita, and J.-Y. Yang, \u201cSpectral transforms for large Boolean functions with application to technology mapping,\u201d in ACM\/IEEE Design Automation Conference (DAC), Dallas, TX, June 1993, pp. 54\u201360.","DOI":"10.1145\/157485.164569"},{"key":"5127650_CR15","doi-asserted-by":"crossref","unstructured":"S. Davari and L. Sha, \u201cSources of unbounded priority inversion in real-time systems and a comperative study of possible solutions,\u201d in ACM Operating Systems Review, April 1992, pp. 110\u2013120.","DOI":"10.1145\/142111.142126"},{"key":"5127650_CR16","doi-asserted-by":"crossref","unstructured":"C. Daws, A. Olivero, S. Tripakis, and S. Yovine, \u201cThe tool KRONOS,\u201d in Hybrid Systems III, Vol. 1066 LNCS. Springer, 1996.","DOI":"10.1007\/BFb0020947"},{"key":"5127650_CR17","first-page":"996","volume-title":"Handbook of Theoretical Computer Science","author":"E. Emerson","year":"1990","unstructured":"E. Emerson, \u201cTemporal and modal logic,\u201d in Handbook of Theoretical Computer Science, J. van Leeuwen (Ed.), Vol. B, pp. 996\u20131072, Amsterdam, Elsevier Science Publishers, 1990."},{"key":"5127650_CR18","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1007\/BF00355298","volume":"4","author":"E. Emerson","year":"1992","unstructured":"E. Emerson, A. Mok, A. Sistla, and J. Srinivasan, \u201cQuantitative temporal reasoning,\u201d Journal of Real-Time Systems, Vol. 4, pp. 331\u2013352, 1992.","journal-title":"Journal of Real-Time Systems"},{"key":"5127650_CR19","first-page":"15","volume-title":"European Design and Test Conference (EDTC)","author":"J. Fr\u00f6 \u03b2l","year":"1996","unstructured":"J. Fr\u00f6 \u03b2l, J. Gerlach, and T. Kropf, \u201cAn efficient algorithm for real-time model checking,\u201d in European Design and Test Conference (EDTC), Paris, France, IEEE Computer Society Press (Los Alamitos, California), March 1996, pp. 15\u201321."},{"key":"5127650_CR20","first-page":"394","volume-title":"IEEE Symposium on Logic in Computer Science (LICS)","author":"T. Henzinger","year":"1992","unstructured":"T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, \u201cSymbolic model checking for real-time systems,\u201d in IEEE Symposium on Logic in Computer Science (LICS), Santa-Cruz, California, IEEE Computer Scienty Press, June 1992, pp. 394\u2013406."},{"key":"5127650_CR21","doi-asserted-by":"crossref","unstructured":"S. Johnson, P. Miner, and A. Camilleri, \u201cStudies of the single pulser in various reasoning systems,\u201d in T. Kropf and R. Kumar (Eds.), International Conference on Theorem Provers in Circuit Design (TPCD), Volume 901 of Lecture Notes in Computer Science, Bad Herrenalb, Germany, September 1994. Springer-Verlag, pp. 126\u2013145, published 1995.","DOI":"10.1007\/3-540-59047-1_46"},{"key":"5127650_CR22","doi-asserted-by":"crossref","unstructured":"C. Lewerentz and T. Lindner (Eds.), Formal Development of Reactive Systems\u2014Case Study Production Cell, number 891 in Lecture Notes in Computer Science (LNCS). Springer Verlag, 1995.","DOI":"10.1007\/3-540-58867-1"},{"key":"5127650_CR23","unstructured":"J. Lipson (Ed.), Elements of Algebra and Algebraic Computing. The Benjamin\/Cummings Publishing Company, Inc., 1981."},{"key":"5127650_CR24","unstructured":"K. McMillan, \u201cThe SMV system, symbolic model checking\u2014An approach,\u201d Technical Report CMU-CS-92-131, Carnegie Mellon University, 1992."},{"key":"5127650_CR25","unstructured":"J. Moller, J. Lichtenberg, H.R. Andersen, and H. Hulgaard, \u201cFully symbolic model checking of timed systems using difference decision diagrams,\u201d in Electronic Notes in Theoretical Computer Science, Vol 23, 1999, Elsevier Science B. V."},{"key":"5127650_CR26","doi-asserted-by":"crossref","unstructured":"D. Peled, V. Pratt, and G. Holzman, (Eds.), Partial Order Methods in Verification, Volume 29 of DIMACS. AMS, 1996.","DOI":"10.1090\/dimacs\/029"},{"key":"5127650_CR27","volume-title":"Formal Methods in Computer Auded Design (FMCAD)","author":"W. Reif","year":"2000","unstructured":"W. Reif, J. Ruf, G. Schellhorn, and T. Vollmer, \u201cDo you trust your model checker?\u201d in S. Johnson and W.A. Hunt (Eds.), Formal Methods in Computer Auded Design (FMCAD), Lecture Notes in Computer Science, Heidelberg, Springer-Verlag, November 2000."},{"key":"5127650_CR28","unstructured":"J. Ruf, \u201cRAVEN: Real-time analyzing and verification environment,\u201d Technical Report, WSI 2000-3, University of T\u00fcbingen, Germany, 2000."},{"key":"5127650_CR29","volume-title":"Workshop on Methods and Languages for Modeling and Verification of Circuits and Systems","author":"J. Ruf","year":"2001","unstructured":"J. Ruf, \u201cData analysis of timed finite state systems,\u201d in Workshop on Methods and Languages for Modeling and Verification of Circuits and Systems,\u201d February 2001, Meissen, Germany. MoPress"},{"key":"5127650_CR30","doi-asserted-by":"crossref","unstructured":"J. Ruf and T. Kropf, \u201cSymbolic model checking for a discrete clocked temporal logic with intervals,\u201d in E. Cerny and D. Probst (Eds.), Conference on Correct Hardware Design and Verification Methods (CHARME), Montreal, Canada, IFIP WG 10.5, Chapman and Hall, October 1997, pp. 146\u2013166","DOI":"10.1007\/978-0-387-35190-2_10"},{"key":"5127650_CR31","doi-asserted-by":"crossref","unstructured":"J. Ruf and T. Kropf, \u201cUsing MTBDDs for composition and model checking of real-time systems,\u201d in FMCAD 1998, Springer, November 1998.","DOI":"10.1007\/3-540-49519-3_13"},{"key":"5127650_CR32","unstructured":"J. Ruf and T. Kropf, \u201cUsing MTBDDs for discrete timed symbolic model checking,\u201d Multiple-Valued Logic\u2014An International Journal. Special Issue on Decision Diagrams. Gordon and Breach Publishers, 1998."},{"key":"5127650_CR33","first-page":"256","volume-title":"Correct Hardware Design and Verification Methods (CHARME)","author":"J. Ruf","year":"1999","unstructured":"J. Ruf and T. Kropf, \u201cModeling and checking networks of communicating real-time processes.\u201d in Correct Hardware Design and Verification Methods (CHARME), L. Pierre and T. Kropf (Eds.), Volume 1703, pp. 256\u2013279 of Lecture Notes in Computer Science, Heidelberg, Germany, Springer-Verlag, September 1999."},{"key":"5127650_CR34","unstructured":"SAE, \u201cJ1850 class B data communication network interface,\u201d The Engineering Society For Advancing Mobility Land Sea Air and Space, October 1995."},{"key":"5127650_CR35","doi-asserted-by":"crossref","unstructured":"Karsten Strehl, \u201cInterval diagrams: Increasing efficiency of symbolic real-time verification,\u201d in 6th International Conference on Real-Time Computing Systems and Applications (RTCSA '99), Hong Kong, December 13-15, 1999, pp. 488\u2013491.","DOI":"10.1109\/RTCSA.1999.811303"},{"key":"5127650_CR36","doi-asserted-by":"crossref","unstructured":"F. Wang, \u201cEfficient data structure for fully symbolic verification of real-time software systems,\u201d in Proceedings of TACAS'2000, LNCS 1785, Springer-Verlag.","DOI":"10.1007\/3-540-46419-0_12"},{"key":"5127650_CR37","volume-title":"7th International Conference on Formal Description Techniques","author":"W. Yi","year":"1994","unstructured":"W. Yi, P. Petterson, and M. Davis, \u201cAutomatic verification of real-time communicating systems by constraint solving,\u201d in 7th International Conference on Formal Description Techniques, Bern, Switzerland, Springer, October 1994."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1024437214071.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1024437214071\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1024437214071.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T19:06:35Z","timestamp":1754420795000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1024437214071"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,7]]},"references-count":37,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,7]]}},"alternative-id":["5127650"],"URL":"https:\/\/doi.org\/10.1023\/a:1024437214071","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2003,7]]}}}