SPEAKER: Luca Aceto, BRICS, Aalborg University

DATE: 9 October 1998

PLACE and TIME: Room E3-209 at 14:00.

ABSTRACT: (to be presented at FST&TCS'98)

The main motivation for the work presented in this talk stems from our experience with the verification tool UPPAAL. In such a tool, real-time systems are specified as networks of timed automata, which are then the object of the verification effort. The core of the computational engine of UPPAAL consists of a collection of efficient algorithms that can be used to perform reachability analysis over networks of timed automata. Any other kind of verification problem that the user wants to ask UPPAAL to perform must be encoded as a suitable reachability question. A typical example of such a problem is that of model checking.

The way model checking of properties other than plain reachability ones may currently be carried out in UPPAAL is as follows. Given a property F to model-check, the user must provide a test automaton Test(F) for that property. This test automaton must be such that the original system has the property expressed by F if, and only if, none of the distinguished reject states of Test(F) can be reached when the test automaton is made to interact with the system under investigation. This approach begs the question of exactly what properties (of networks) of timed automata can be model checked in this fashion.

In this talk, I shall present a property language that completely characterizes the collection of properties (of networks) of timed automata for which model checking can be reduced to reachability testing, in the aforementioned sense. In the process of presenting our main expressive completeness result, I aim at describing some of the proof techniques, and intermediate results of independent interest which we have found useful in the proof. Some results relating to the relative expressive power of three of the property languages that we have considered, and of their relationship with preorders on timed processes will also be hinted at, if time permits.

This presentation is based upon joint work with Patricia Bouyer (LSV, ENS Cachan, France), Augusto Burgueno (Onera-Cert, Toulouse, France) and Kim. G. Larsen.