{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,6]],"date-time":"2025-01-06T05:10:18Z","timestamp":1736140218704,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540633884"},{"type":"electronic","value":"9783540695301"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0014568","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T09:17:33Z","timestamp":1132737453000},"page":"562-582","source":"Crossref","is-referenced-by-count":2,"title":["Symbolic model-checking method based on approximations and binary decision diagrams for real-time systems"],"prefix":"10.1007","author":[{"given":"Satoshi","family":"Yamane","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kazuhiro","family":"Nakamura","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur, D.L. Dill. Automata for modeling real-time systems. In Proc. of 17th ICALP, LNCS 443, pp. 322\u2013335, Springer-Verlag, 1990.","DOI":"10.1007\/BFb0032042"},{"key":"24_CR2","doi-asserted-by":"crossref","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan and D.L. Dill. Sequential Circuit Verification Using Symbolic Model Checking. In Proc. of 27th Design Automation Conference, pp. 46\u201351, 1990.","DOI":"10.1145\/123186.123223"},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, D.L. Dill. Model checking for real-time systems. In Proc. of 5th LICS, pp. 414\u2013425, 1992.","DOI":"10.1109\/LICS.1990.113766"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. In Proc. of 7th LICS, pp. 394\u2013406, 1992.","DOI":"10.1109\/LICS.1992.185551"},{"key":"24_CR5","first-page":"575","volume":"1066","author":"K. G. Larsen","year":"1996","unstructured":"Kim G. Larsen, Paul Pettersson, and Wang Yi. Diagnostic Model-Checking for Real-Time Systems. In LNCS 1066, pp. 575\u2013586, 1996.","journal-title":"LNCS"},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"H. Wong-Toi and D.L. Dill. Approximations for verifying timing properties. In Theories and Experiences for Real-Time System Development, chapter 7, pp 177\u2013204, World Scientific, 1993.","DOI":"10.1142\/9789812831583_0007"},{"key":"24_CR7","doi-asserted-by":"crossref","unstructured":"D.L. Dill and H. Wong-Toi. Verification of real-time systems by successive over and under approximation. In Proceedings of Seventh Conference on Computer-Aided Verification, Liege, Belgium. LNCS 939, pp. 409\u2013422, Springer-Verlag, 1995.","DOI":"10.1007\/3-540-60045-0_66"},{"issue":"8","key":"24_CR8","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant. Graph-based algorithms for boolean function manipulation. In IEEE Transactions on Computers. Vol. C-35, No.8, pp. 677\u2013691, IEEE Computer Society, 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"D.L. Dill. Timing assumptions and verification of finite-state concurrent systems. In Automatic Verification Methods for Finite State Systems, International Workshop. LNCS 407, pp. 197\u2013211, Springer-Verlag, 1989.","DOI":"10.1007\/3-540-52148-8_17"},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, D. Dill N. Halbwachs and H. Wong-Toi. An implementation of three algorithms for timing verification based on automata emptiness. In Proceedings of IEEE RTSS, pp. 157\u2013166, Phoenix, AZ, 1992.","DOI":"10.1109\/REAL.1992.242667"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, E. C. Browne E. A. Emerson, and A. P. Sistla. Using temporal logic for automatic verification of finite state systems. In Logics and Models of Concurrent Systems, pp. 3\u201325, Springer-Verlag, 1985","DOI":"10.1007\/978-3-642-82453-1_1"},{"key":"24_CR12","doi-asserted-by":"crossref","unstructured":"R. I. Bahar, E. A. Frohm, C. M. Gaona, G. D. Hachtel E. Macci, A. Prado, F. Somenzi. Algebraic Decision Diagrams and their application. In Proc. 33th IEEE CAD, pp. 188\u2013191, 1993.","DOI":"10.1109\/ICCAD.1993.580054"},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, K. L. McMillan, X. Zhao, M. Fujita, J. Yang. Spectral transforms for large boolean functions with applications to technology mapping. In Proc. 30th ACM\/IEEE Design Automation Conference, pp. 54\u201360, 1993.","DOI":"10.1145\/157485.164569"},{"key":"24_CR14","doi-asserted-by":"crossref","unstructured":"E. Asarin, M. Bozga, A. Kerbrat, O. Maler, A. Pnueli, A. Rasse. Data structures for the verification of timed automata. In LNCS 1201, pp. 575\u2013586, 1997.","DOI":"10.1007\/BFb0014737"},{"key":"24_CR15","doi-asserted-by":"crossref","unstructured":"S. Minato, N. Ishiura, S. Yajima. Shared Binary Decision Diagram with Attributed Edges for Efficient Boolean Function Manipulation. In Proc. 27th ACM\/IEEE Design Automation Conference, pp. 52\u201357, 1990.","DOI":"10.1145\/123186.123225"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computer Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0014568","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,5]],"date-time":"2025-01-05T21:49:52Z","timestamp":1736113792000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0014568"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540633884","9783540695301"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/bfb0014568","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}