Interval Diagrams: Increasing Efficiency of Symbolic Real-Time Verification

In this paper, we suggest interval diagram techniques for formal verification of real-time systems modeled by means of timed automata. Interval diagram techniques are based on interval decision diagrams (IDDs)---representing sets of system configurations of, e.g., timed automata---and interval mapping diagrams (IMDs)--- modeling their transition behavior. IDDs are canonical representations of Boolean functions and allow for their efficient manipulation. Our approach is used for performing both timed reachability analysis and real-time symbolic model checking. We present the methods necessary for our approach and compare its results to another, similar verification technique---achieving a speedup of 7 and more. 1 Introduction Especially for safety-critical real-time applications such as those in traffic control, medical engineering, or avionics, simulation often is not sufficient to guarantee the correctness of a technical system's model. In addition to simulation, formal methods are e..