Analysis of Reactive Systems with n Timers

Abstract

In this paper, we develop theoretical, as well as practical, tools for the synthesis and the verification of processes that contain n timers. Such tools are equally adapted to numerical calculations as to symbolical ones, thus allowing for parametric analysis. The results we have obtained rely on a simple and efficient representation of the states of an automaton that recognizes the behaviors of the process. This representation is based on a mechanical structure which helps us encode the states in a compact manner and leads to simple algorithms.