In this chapter, we address the problem of controller synthesis for timed systems. By timed systems we refer to those systems which are subject to *quantitative* (hard) realtime constraints. We assume the reader is familiar with the basics of timed automata theory, or has read Chapters 1 and 2 of this book.

It is not always possible to use *discrete time* to specify and model timing constraints. This is why *dense-time* specification formalisms, such as timed automata [ALU 94] or time Petri nets [MER 74], were introduced some years ago. Once a system is modeled by a timed automaton or a TPN, it can be checked (Chapter 2) for quantitative properties. If a property is not satisfied, we still might be able to act on the system and *control* some of its behaviors: for example, by adding a component or a *controller*. How to compute such a timed controller is the purpose of this chapter, in which we review some algorithms for controller synthesis for TA.

A standard approach to the verification of real-time systems, called *model-checking* [SCH 99], consists of three phases: (1) build a complete model *S* for the system (e.g., a finite automaton); (2) specify the qualitative correctness property to be satisfied in a non-ambiguous logical language (e.g. temporal logics) as a formula *ψ*; and (3) check algorithmically that *S* is a *model* of *ψ,* denoted by this is the *model-checking* algorithm. Model-checking techniques ...

Start Free Trial

No credit card required