# 1

# Parametric Timed Automata

In this chapter, we present the formalisms used throughout this book. In particular, we present timed automata [ALU 94], a powerful modeling formalism for real-time systems. Since this book focuses on synthesizing values for timing parameters of a system, guaranteeing a good behavior, we will also use a parametric extension of timed automata, namely *parametric timed automata* [ALU 93c]. This chapter presents their syntax and semantics, and more generally all the necessary formalisms to understand the rest of this book. Any reader who is not particularly interested in theory can skip directly to Chapter 2, and return to Chapter 1 when needed.

*Outline of the chapter*

We describe clocks, parameters and constraints on the clocks and parameters in section 1.1 and labeled transition system in section 1.2. We then introduce the syntax and semantics of timed automata in section 1.3, and parametric timed automata in section 1.4. Related works, including representation of time, and formalisms related to timed automata, are discussed in section 1.5.

# 1.1. Constraints on clocks and parameters

## 1.1.1. *Clocks*

Throughout this book, we assume a fixed set *X* = {*x*_{1}, … , *x*_{H} } of *clocks*. A *clock* is a variable *x*_{i} with value in , which denotes the set of non-negative real numbers. All clocks evolve linearly at the same rate. We define a *clock valuation* as a function *w*: *X* → assigning ...