{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T05:05:39Z","timestamp":1737435939755,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439318"},{"type":"electronic","value":"9783540456209"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45620-1_9","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T07:18:26Z","timestamp":1186903106000},"page":"129-133","source":"Crossref","is-referenced-by-count":0,"title":["DDDLIB: A Library for Solving Quantified Difference Inequalities"],"prefix":"10.1007","author":[{"given":"Jesper B.","family":"M\u00f8ller","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"P.A. Abdulla and A. Nyl\u00e9n. Better is better than well: On efficient verification of infinite-state systems. In Proc. 15th LICS, pages 132\u2013140, 2000.","DOI":"10.1109\/LICS.2000.855762"},{"volume-title":"Reasoning about Plans","year":"1991","key":"9_CR2","unstructured":"J.F. Allen, H. Kautz, R.N. Pelavin, and J. Tenenberg, editors. Reasoning about Plans. Morgan Kaufmann, San Mateo, California, 1991."},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In Proc. 5th LICS, pages 414\u2013425, 1990.","DOI":"10.1109\/LICS.1990.113766"},{"key":"9_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/3-540-48683-6_30","volume-title":"Proc. 11th Conference on Computer Aided Verification","author":"G. Behrmann","year":"1999","unstructured":"G. Behrmann, K.G. Larsen, J. Pearson, C. Weise, and W. Yi. Efficient timed reachability analysis using clock difference diagrams. In Proc. 11th Conference on Computer Aided Verification, LNCS 1633, pages 341\u2013353, 1999."},{"issue":"1","key":"9_CR5","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1090\/qam\/102435","volume":"16","author":"R. Bellman","year":"1958","unstructured":"R. Bellman. On a routing problem. Quarterly of Applied Math., 16(1):87\u201390, 1958.","journal-title":"Quarterly of Applied Math."},{"issue":"8","key":"9_CR6","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_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Proc. 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 Proc. Workshop on Logics of Programs, LNCS 131, pages 52\u201371. Springer-Verlag, 1981."},{"key":"9_CR8","volume-title":"Technical Report MIP-9905","author":"A. Dolzmann","year":"1999","unstructured":"A. Dolzmann and T. Sturm. Redlog user manual. Technical Report MIP-9905, FMI, Universit\u00e4t Passau, D-94030 Passau, Germany, April 1999."},{"key":"9_CR9","unstructured":"J.B.J. Fourier. Second extrait. In Oeuvres, pages 325\u2013328. Gauthiers-Villars, 1890."},{"key":"9_CR10","unstructured":"M.S. Fox. Constraint-directed Search: A Case Study of Job-Shop Scheduling. Morgan Kaufmann Publishers, 1987."},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"M. Koubarakis. Complexity results for first-order theories of temporal constraints. In Principles of Knowledge Representation and Reasoning, pages 379\u2013390, 1994.","DOI":"10.1016\/B978-1-4832-1452-8.50131-7"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"R.A. Kowalski and M.J. Sergot. A logic-based calculus of events. In Proc. Foundations of Knowledge Base Management, pages 23\u201355, 1985.","DOI":"10.1007\/978-3-642-83397-7_2"},{"issue":"1","key":"9_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/7351.7352","volume":"5","author":"L. Lamport","year":"1987","unstructured":"L. Lamport. A fast mutual exclusion algorithm. ACM Trans. on Comp. Systems, 5(1):1\u201311, 1987.","journal-title":"ACM Trans. on Comp. Systems"},{"issue":"3","key":"9_CR14","first-page":"271","volume":"6","author":"K.G. Larsen","year":"1999","unstructured":"K.G. Larsen, J. Pearson, C. Weise, and W. Yi. Clock difference diagrams. Nordic Journal of Computing, 6(3):271\u2013298, 1999.","journal-title":"Nordic Journal of Computing"},{"issue":"1\u20132","key":"9_CR15","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K.G. Larsen","year":"1997","unstructured":"K.G. Larsen, P. Pettersson, and W. Yi. Uppaal in a nutshell. International Journal on Software Tools for Technology Transfer, 1(1\u20132):134\u2013152, 1997.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"9_CR16","volume-title":"BuDDy: Binary Decision Diagram package","author":"J. Lind-Nielsen","year":"2001","unstructured":"J. Lind-Nielsen. BuDDy: Binary Decision Diagram package. IT University of Copenhagen, Glentevej 67, DK-2400 Copenhagen NV, May 2001."},{"issue":"1\u20132","key":"9_CR17","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1016\/0004-3702(95)00109-3","volume":"87","author":"I. Meiri","year":"1996","unstructured":"I. Meiri. Combining qualitative and quantitative constraints in temporal reasoning. Artificial Intelligence, 87(1\u20132):343\u2013385, 1996.","journal-title":"Artificial Intelligence"},{"key":"9_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/3-540-48168-0_9","volume-title":"Proc. Computer Science Logic","author":"J. M\u00f8ller","year":"1999","unstructured":"J. M\u00f8ller, J. Lichtenberg, H.R. Andersen, and H. Hulgaard. Difference decision diagrams. In Proc. Computer Science Logic, LNCS 1683, pages 111\u2013125, 1999."},{"key":"9_CR19","unstructured":"J.B. M\u00f8ller. Simplifying fixpoint computations in verification of real-time systems. Technical Report TR-2002-15, IT University of Copenhagen, April 2002."},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"A. Pnueli. The temporal logic of programs. In Proc. 18th IEEE Symposium on the Foundations of Computer Science, pages 46\u201357, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"W. Pugh. The Omega Test: A fast and practical integer programming algorithm for dependence analysis. Comm. of the ACM, 35(8):102\u2013114, August 1992.","DOI":"10.1145\/135226.135233"},{"key":"9_CR22","unstructured":"S. Romanenko, C. Russo, and P. Sestoft. Moscow ML Owner\u2019s Manual, June 2000."},{"key":"9_CR23","unstructured":"M. Sorea. Tempo: A model-checker for event-recording automata. In Proc. Workshop on Real-Time Tools, August 2001. Also as SRI Technical Report CSL-01-04."},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"S. Yovine. Kronos: A verification tool for real-time systems. International Journal on Software Tools for Technology Transfer, 1(1\u20132):123\u2013133, October 1997.","DOI":"10.1007\/s100090050009"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"H. Zhang. SATO: An efficient propositional prover. In Proc. Conference on Automated Deduction, pages 272\u2013275, 1997.","DOI":"10.1007\/3-540-63104-6_28"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-18"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45620-1_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T08:52:09Z","timestamp":1737363129000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45620-1_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439318","9783540456209"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-45620-1_9","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}