A DATA STRUCTURE AND ITS USE

Henrik Reif Andersen (Inventor), Henrik Hulgaard (Inventor), Jakob Lichtenberg (Inventor), Jesper Blak Møller (Inventor)

    Research output: Patent

    Abstract

    A data structure and its use in for example representation, analysis and verification of systems comprising continuous variables. Continuous variables arise in many areas of computer science and mathematics as for example timers or clocks in real-time controllers and digital circuits, sensors in embedded systems, counters in concurrent protocols, variables in confuguration problems, and scheduling times in planning and optimization problems. The data structure can represent and decide validity of first order propositional formulas over difference constraints or linear inqualities. The data structure can be used in symbolic model checking of concurrent timed systems modeled as timed automata, timed Petri nets or timed guarded commands. The data structure is preferably embodied as a decision diagram similar to binary decision diagrams (BDDs).
    Original languageEnglish
    Patent numberWO2000013113
    Filing date09/03/2000
    CountryInternational Bureau of the World Intellectual Property Organization (WIPO)
    Publication statusPublished - 2000

    Cite this

    Andersen, H. R., Hulgaard, H., Lichtenberg, J., & Møller, J. B. (2000). A DATA STRUCTURE AND ITS USE. (Patent No. WO2000013113).