DDDLIB: A Library for Solving Quantified Difference Inequalities

  • Jesper B. Møller
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2392)


DDDLIB is a library for manipulating formulae in a first-order logic over Boolean variables and inequalities of the form x 1 x 2d, where x 1,x 2 are real variables and d is an integer constant. Formulae are represented in a semi-canonical data structure called difference decision diagrams (DDDs) which provide efficient algorithms for constructing formulae with the standard Boolean operators (conjunction, disjunction, negation, etc.), eliminating quantifiers, and deciding functional properties (satisfiability, validity and equivalence). The library is written in C and has interfaces for C++, Standard ML and Objective Caml.


Boolean Variable Binary Decision Diagram Reachability Analysis Symbolic Model Checker Integer Constant 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    P.A. Abdulla and A. Nylén. Better is better than well: On efficient verification of infinite-state systems. In Proc. 15th LICS, pages 132–140, 2000.Google Scholar
  2. 2.
    J.F. Allen, H. Kautz, R.N. Pelavin, and J. Tenenberg, editors. Reasoning about Plans. Morgan Kaufmann, San Mateo, California, 1991.zbMATHGoogle Scholar
  3. 3.
    R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In Proc. 5th LICS, pages 414–425, 1990.Google Scholar
  4. 4.
    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–353, 1999.CrossRefGoogle Scholar
  5. 5.
    R. Bellman. On a routing problem. Quarterly of Applied Math., 16(1):87–90, 1958.zbMATHGoogle Scholar
  6. 6.
    R.E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, 1986.CrossRefGoogle Scholar
  7. 7.
    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–71. Springer-Verlag, 1981.CrossRefGoogle Scholar
  8. 8.
    A. Dolzmann and T. Sturm. Redlog user manual. Technical Report MIP-9905, FMI, Universität Passau, D-94030 Passau, Germany, April 1999.Google Scholar
  9. 9.
    J.B.J. Fourier. Second extrait. In Oeuvres, pages 325–328. Gauthiers-Villars, 1890.Google Scholar
  10. 10.
    M.S. Fox. Constraint-directed Search: A Case Study of Job-Shop Scheduling. Morgan Kaufmann Publishers, 1987.Google Scholar
  11. 11.
    M. Koubarakis. Complexity results for first-order theories of temporal constraints. In Principles of Knowledge Representation and Reasoning, pages 379–390, 1994.Google Scholar
  12. 12.
    R.A. Kowalski and M.J. Sergot. A logic-based calculus of events. In Proc. Foundations of Knowledge Base Management, pages 23–55, 1985.Google Scholar
  13. 13.
    L. Lamport. A fast mutual exclusion algorithm. ACM Trans. on Comp. Systems, 5(1):1–11, 1987.CrossRefGoogle Scholar
  14. 14.
    K.G. Larsen, J. Pearson, C. Weise, and W. Yi. Clock difference diagrams. Nordic Journal of Computing, 6(3):271–298, 1999.zbMATHMathSciNetGoogle Scholar
  15. 15.
    K.G. Larsen, P. Pettersson, and W. Yi. Uppaal in a nutshell. International Journal on Software Tools for Technology Transfer, 1(1–2):134–152, 1997.zbMATHGoogle Scholar
  16. 16.
    J. Lind-Nielsen. BuDDy: Binary Decision Diagram package. IT University of Copenhagen, Glentevej 67, DK-2400 Copenhagen NV, May 2001.Google Scholar
  17. 17.
    I. Meiri. Combining qualitative and quantitative constraints in temporal reasoning. Artificial Intelligence, 87(1–2):343–385, 1996.CrossRefMathSciNetGoogle Scholar
  18. 18.
    J. Møller, J. Lichtenberg, H.R. Andersen, and H. Hulgaard. Difference decision diagrams. In Proc. Computer Science Logic, LNCS 1683, pages 111–125, 1999.CrossRefGoogle Scholar
  19. 19.
    J.B. Møller. Simplifying fixpoint computations in verification of real-time systems. Technical Report TR-2002-15, IT University of Copenhagen, April 2002.Google Scholar
  20. 20.
    A. Pnueli. The temporal logic of programs. In Proc. 18th IEEE Symposium on the Foundations of Computer Science, pages 46–57, 1977.Google Scholar
  21. 21.
    W. Pugh. The Omega Test: A fast and practical integer programming algorithm for dependence analysis. Comm. of the ACM, 35(8):102–114, August 1992.Google Scholar
  22. 22.
    S. Romanenko, C. Russo, and P. Sestoft. Moscow ML Owner’s Manual, June 2000.Google Scholar
  23. 23.
    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.Google Scholar
  24. 24.
    S. Yovine. Kronos: A verification tool for real-time systems. International Journal on Software Tools for Technology Transfer, 1(1–2):123–133, October 1997.Google Scholar
  25. 25.
    H. Zhang. SATO: An efficient propositional prover. In Proc. Conference on Automated Deduction, pages 272–275, 1997.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Jesper B. Møller
    • 1
  1. 1.Department of InnovationIT University of CopenhagenDenmark

Personalised recommendations