Extending synchronous languages for generating abstract real-time models

We present an extension of synchronous programming lan-guages that can be used to declare program locations irrel-evant for verification. An efficient algorithm is proposed to generate from the output of the usual compilation an abstract real-time model by ignoring the irrelevant states, while retaining the quantitative information. Our tech-nique directly generates a single real-time transition sys-tem, thus overcoming the known problem of composing sev-eral real-time models. A major application of this approach is the verification of real-time properties by symbolic model checking. 1