{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:40:34Z","timestamp":1754487634473,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540651918"},{"type":"electronic","value":"9783540495192"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-49519-3_13","type":"book-chapter","created":{"date-parts":[[2007,10,20]],"date-time":"2007-10-20T10:37:12Z","timestamp":1192876632000},"page":"185-202","source":"Crossref","is-referenced-by-count":5,"title":["Using MTBDDs for Composition and Model Checking of Real-Time Systems"],"prefix":"10.1007","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","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"key":"13_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/3-540-63166-6_19","volume-title":"Conference on Computer Aided Verification (CAV)","author":"M. Bozga","year":"1997","unstructured":"M. Bozga, O. Maler, A. Pnueli, and S. Yovine. Some progress in the symbolic verification of timed automata. In O. Grumberg, editor, Conference on Computer Aided Verification (CAV), volume 1254 of Lecture Notes in Computer Science, pages 179\u2013190. Springer Verlag, June 1997."},{"key":"13_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"456","DOI":"10.1007\/3-540-63166-6_47","volume-title":"Conference on Computer Aided Verification (CAV)","author":"K. Larsen","year":"1997","unstructured":"K. Larsen, P. Pettersson, and W. Yi. UPPAAL: Status & developments. In O. Grumberg, editor, Conference on Computer Aided Verification (CAV), volume 1254 of Lecture Notes in Computer Science, pages 456\u2013459. Springer Verlag, June 1997."},{"key":"13_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"452","DOI":"10.1007\/3-540-63166-6_46","volume-title":"Conference on Computer Aided Verification (CAV)","author":"S. Campos","year":"1997","unstructured":"S. Campos, E. Clarke, and M. Minea. The verus tool: A quantitative approach to the formal verification of real-time systems. In O. Grumberg, editor, Conference on Computer Aided Verification (CAV), volume 1254 of Lecture Notes in Computer Science, pages 452\u2013455. Springer Verlag, June 1997."},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetics, and D. Dill. Model Checking for Real-Time Systems. In IEEE Symposium on Logic in Computer Science (LICS), pages 414\u2013425, Washington, D.C., June 1990. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1990.113766"},{"key":"13_CR5","unstructured":"J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang. Symbolic Model Checking: 1020 States and Beyond. In IEEE Symposium on Logic in Computer Science (LICS), pages 1\u201333, Washington, D.C., June 1990. IEEE Computer Society Press."},{"key":"13_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","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. Data structures for the verification of timed automata. In O. Maler, editor, Hybrid and Real-Time Systems, pages 346\u2013360, Grenoble, France, 1997. Springer Verlag, LNCS 1201."},{"key":"13_CR7","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/BF00355298","volume":"4","author":"E. Emerson","year":"1992","unstructured":"E. Emerson, A. Mok, A. Sistla, and J. Srinivasan. Quantitative Temporal Reasoning. Journal of Real-Time Systems, 4:331\u2013352, 1992.","journal-title":"Journal of Real-Time Systems"},{"key":"13_CR8","first-page":"15","volume-title":"European Design and Test Conference (EDTC)","author":"J. Fr\u00f6\\l","year":"1996","unstructured":"J. Fr\u00f6\\l, J. Gerlach, and T. Kropf. An Efficient Algorithm for Real-Time Model Checking. In European Design and Test Conference (EDTC), pages 15\u201321, Paris, France, March 1996. IEEE Computer Society Press (Los Alamitos, California)."},{"key":"13_CR9","unstructured":"T. Kropf and J. Ruf. Using MTBDDs for discrete timed symbolic model checking. Technical Report SFB358-C2-5\/96, Universit\u00c4t Karlsruhe, Institut f\u00fcr Rechnerentwurf und Fehlertoleranz, August 1996. ftp:\/\/goethe.ira.uka.de\/pub\/hvg\/techreports\/SFB358-C2-5-6.ps.gz ."},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"J. Ruf and T. Kropf. Symbolic model checking for a discrete clocked temporal logic with intervals. In E. Cerny and D. Probst, editors, Conference on Correct Hardware Design and Verification Methods (CHARME), pages 146\u2013166, Montreal, Canada, October 1997. IFIP WG 10.5, Chapman and Hall.","DOI":"10.1007\/978-0-387-35190-2_10"},{"key":"13_CR11","unstructured":"J. Lipson, editor. Elements of Algebra and Algebraic Computing. The Benjamin\/ Cummings Publishing Company, Inc., 1981."},{"issue":"8","key":"13_CR12","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R. Bryant","year":"1986","unstructured":"R. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, C-35(8):677\u2013691, August 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"E. Clarke, K. McMillian, X. Zhao, M. Fujita, and J.-Y. Yang. Spectral Transforms for large Boolean Functions with Application to Technologie Mapping. In ACM\/IEEE Design Automation Conference (DAC), pages 54\u201360, Dallas, TX, June 1993.","DOI":"10.1145\/157485.164569"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"R. Bahar, E. Frohm, C. Gaona, G. Hachtel, E. Macii, A. Pardo, and F. Somenzi. Algebraic Decision Diagrams and Their Applications. In IEEE\/ACM International Conference on Computer Aided Design (ICCAD), pages 188\u2013191, Santa Clara, California, November 1993. ACM\/IEEE, IEEE Computer Society Press.","DOI":"10.1109\/ICCAD.1993.580054"},{"key":"13_CR15","unstructured":"J. Ruf and T. Kropf. Using MTBDDs for composition and model checking of real-time systems. Technical Report SFB358-C2-1\/98, Universit\u00c4t Karlsruhe, Institut f\u00fcr Rechnerentwurf und Fehlertoleranz, January 1998. ftp:\/\/goethe.ira.uka.de\/pub\/hvg\/techreports\/SFB358-C2-1-98.ps.gz ."},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In O. Grumberg, editor, Conference on Computer Aided Verification (CAV), volume 1254 of Lecture Notes in Computer Scienece, pages 72\u201383. Springer Verlag, June 1997.","DOI":"10.1007\/3-540-63166-6_10"},{"key":"13_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/BFb0031809","volume-title":"International Conference on Formal Methods in Computer Aided Design (FMCAD)","author":"K. Schneider","year":"1996","unstructured":"K. Schneider and T. Kropf. A unified approach for combining different formalisms for hardware verification. In M. Srivas and A. Camilleri, editors, International Conference on Formal Methods in Computer Aided Design (FMCAD), volume 1166 of Lecture Notes in Computer Science, pages 202\u2013217, Palo Alto, USA, November 1996. Springer Verlag."}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49519-3_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T19:50:27Z","timestamp":1737489027000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49519-3_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651918","9783540495192"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-49519-3_13","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1998]]}}}