Using interval diagram techniques for the symbolic verification of timed automata

Abstract

In this report, we suggest interval diagram techniques for formal verification 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. We present the methods necessary for our approach and compare its results to another, similar verification technique.