Communicating Embedded Systems: Software and Design

Chapter 3

Control of Timed Systems ¹

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.

3.1. Introduction

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.

3.1.1. Verification of timed systems

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 ...