{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:30:54Z","timestamp":1761597054872,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665366"},{"type":"electronic","value":"9783540481683"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48168-0_9","type":"book-chapter","created":{"date-parts":[[2007,12,1]],"date-time":"2007-12-01T11:30:26Z","timestamp":1196508626000},"page":"111-125","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":54,"title":["Difference Decision Diagrams"],"prefix":"10.1007","author":[{"given":"Jesper","family":"M\u00f8ller","sequence":"first","affiliation":[]},{"given":"Jakob","family":"Lichtenberg","sequence":"additional","affiliation":[]},{"given":"Henrik Reif","family":"Andersen","sequence":"additional","affiliation":[]},{"given":"Henrik","family":"Hulgaard","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,5,13]]},"reference":[{"key":"9_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/BFb0031986","volume-title":"Real-Time: Theory in Practice","author":"R. Alur","year":"1991","unstructured":"R. Alur and D. Dill. The theory of timed automata. In Real-Time: Theory in Practice, LNCS 600, pages 28\u201373. Springer-Verlag, 1991."},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"E. Asarin, M. Bozga, A. Kerbrat, O. Maler, A. Pnueli, and A. Rasse. Data-structures for the verification of timed automata. In Int. Workshop on Hybrid and Real-Time System, 1997.","DOI":"10.1007\/BFb0014737"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"F. Balarin. Approximate reachability analysis of timed automata. In Real-Time Systems Symposium, pages 52\u201361. IEEE, 1996.","DOI":"10.1109\/REAL.1996.563700"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"G. Behrmann, K. G. Larsen, J. Pearson, C. Weise, and Wang Yi. Efficient timed reachability analysis using clock difference diagrams. Technical Report 99\/105, Uppsala Univ., 1999.","DOI":"10.1007\/3-540-48683-6_30"},{"key":"9_CR5","unstructured":"W. Belluomini and C. J. Myers. Efficient timing analysis algorithms for timed state space exploration. In Int. Symposium on Advanced Research in Asynchronous Circuits and Systems, April 1997."},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"W. Belluomini and C. J. Myers. Verification of timed systems using POSETs. In Computer Aided Verfication (CAV), June 1998.","DOI":"10.1007\/BFb0028762"},{"issue":"3","key":"9_CR7","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1109\/32.75415","volume":"17","author":"B. Berthomieu","year":"1991","unstructured":"B. Berthomieu and M. Diaz. Modeling and verification of time dependent systems using time Petri nets. IEEE Transactions on Software Engineering, 17(3):259\u2013273, 1991.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"9_CR8","series-title":"Lect Notes Comput Sci","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":"M. Bozga, O. Maler, A. Pnueli, and S. Yovine. Some progress in the symbolic verification of timed automata. In Computer Aided Verification, LNCS 1254, pages 179\u2013190, 1997."},{"issue":"8","key":"9_CR9","doi-asserted-by":"publisher","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. IEEE Transactions on Computers, C-35(8):677\u2013691, 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"J. R. Burch. Trace Algebra for Automatic Verification of Real-Time Concurrent Systems. PhD thesis, Carnegie Mellon, August 1992.","DOI":"10.21236\/ADA256199"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"S. V. Campos, E. Clarke, W. Marrero, M. Minea, and H. Hiraishi. Computing quantitative characteristics of finite-state real-time systems. In Real-Time Systems Symposium, pages 266\u201370. IEEE, December 1994.","DOI":"10.1109\/REAL.1994.342709"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"W. Chan, R. Anderson, P. Beame, and D. Notkin. Combining constraint solving and symbolic model checking for a class of systems with non-linear constraints. In Computer Aided Verification, pages 316\u201327, 1997.","DOI":"10.1007\/3-540-63166-6_32"},{"key":"9_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Workshop on Logics of Programs","author":"E.M. Clarke","year":"1981","unstructured":"E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Workshop on Logics of Programs, LNCS 131, pages 52\u201371. Springer-Verlag, 1981."},{"key":"9_CR14","unstructured":"T. Cormen, C. Leiserson, and R. Rivest. Introduction to Algorithms. MIT Press, 1994."},{"key":"9_CR15","series-title":"Lect Notes Comput Sci","volume-title":"Automatic Verification Methods for Finite State Systems","author":"D. L. Dill","year":"1989","unstructured":"D. L. Dill. Timing assumptions and verification of finite-state concurrent systems. In Automatic Verification Methods for Finite State Systems, LNCS 407. Springer, 1989."},{"key":"9_CR16","unstructured":"J.B.J. Fourier. Second extrait. In Oeuvres, pages 325\u2013328, Paris, 1890. Gauthiers-Villars."},{"issue":"2","key":"9_CR17","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T. A. Henzinger","year":"1994","unstructured":"T. A. Henzinger, Z. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193\u2013244, 1994.","journal-title":"Information and Computation"},{"key":"9_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/3-540-60249-6_41","volume-title":"Conference on Fundamentals of Computation Theory","author":"K. G. Larsen","year":"1995","unstructured":"K. G. Larsen, P. Pettersson, and W. Yi. Model-checking for real-time systems. In Conference on Fundamentals of Computation Theory, LNCS 965, pages 62\u201388, August 1995."},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Kim G. Larsen, Paul Pettersson, and Wang Yi. Uppaal in a nutshell. Springer International Journal of Software Tools for Technology Transfer, 1(1+2), 1997.","DOI":"10.1007\/s100090050010"},{"key":"9_CR20","unstructured":"Robin Milner. Communication and Concurrency. Prentice Hall, 1989."},{"key":"9_CR21","volume-title":"Technical Report IT-TR-1999-023, Department of Information Technology","author":"J. M\u00f8ller","year":"1999","unstructured":"J. M\u00f8ller, J. Lichtenberg, H. R. Andersen, and H. Hulgaard. Difference decision diagrams. Technical Report IT-TR-1999-023, Department of Information Technology, Technical University of Denmark, Building 344, DK-2800 Lyngby, Denmark, February 1999."},{"key":"9_CR22","unstructured":"J. M\u00f8ller, J. Lichtenberg, H. R. Andersen, and H. Hulgaard. Fully symbolic model checking of timed systems using difference decision diagrams. In FLoC\u201999 Workshop on Symbolic Model Checking, July 1999. Available from the Electronic Notes in Theoretical Computer Science repository: http:\/\/www.elsevier.nl\/locate\/entcs ."},{"key":"9_CR23","unstructured":"T. G. Rokicki. Representing and Modeling Digital Circuits. PhD thesis, Stanford University, 1993."},{"key":"9_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"468","DOI":"10.1007\/3-540-58179-0_76","volume-title":"Computer Aided Verification (CAV)","author":"T. G. Rokicki","year":"1994","unstructured":"T. G. Rokicki and C. J. Myers. Automatic verification of timed circuits. In D. L. Dill, editor, Computer Aided Verification (CAV), LNCS 818, pages 468\u2013480, 1994."},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"R. L. Spelberg, H. Toetenel, and M. Ammerlaan. Partition refinement in real-time model checking. In Proceedings of FTRTFT\u201998, pages 143\u201357, 1998.","DOI":"10.1007\/BFb0055344"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"E. Verlind, G. de Jong, and B. Lin. Efficient partial enumeration for timing analysis of asynchronous systems. In ACM\/IEEE Design Automation Conference, 1996.","DOI":"10.1145\/240518.240529"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"H. Wong-Toi and D.L. Dill. Approximations for verifying timing properties. In Theories and Experiences for Real-Time Systems Development.World Scientific Publishing, 1994.","DOI":"10.1142\/9789812831583_0007"},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"S. Yovine. Kronos:A verification tool for real-time systems. Springer Int. Journal of Software Tools for Technology Transfer, 1(1\/2), October 1997.","DOI":"10.1007\/s100090050009"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48168-0_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T03:46:18Z","timestamp":1737603978000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48168-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665366","9783540481683"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-48168-0_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"13 May 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}