| 摘要 |
<p>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).</p> |
