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

    Research output: Patent


    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
    Country/TerritoryInternational Bureau of the World Intellectual Property Organization (WIPO)
    Publication statusPublished - 2000


    Dive into the research topics of 'A DATA STRUCTURE AND ITS USE'. Together they form a unique fingerprint.

    Cite this