![]()
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 = {
x1, … ,
xH } of
clocks. A
clock is a variable
xi 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 a non-negative real value to each clock variable. We will often identify a valuation
w with the point (
w(
x1), … ,
w(
xH )). Given a constant
d ∈
, we use
X +
d to denote the set {
x1 +
d, … ,
xH +
d}. Similarly, we write
w +
d to denote the valuation such that (
w +
d)(
x) =
w(
x) +
d for all
x ∈
X.
1.1.2. Parameters
Throughout this book, we assume a fixed set
P = {
p1, … ,
pM } of
parameters, that is unknown constants. A
parameter valuation π is a function
π:
P →
assigning a non-negative real value to each parameter. There is a one-to-one correspondence between valuations and points in
. We will often identify a valuation
π with the point (
π(
p1), … ,
π(
pM )).
1.1.3. Constraints
We define constraints here as a set of linear inequalities.
1.1.3.1. Syntax of constraints
D
EFINITION 1.1.–
Let V be a set of variables of the form V = {
v1, … ,
vN }. A linear inequality on the variables of
V is an inequality e e′, where
∈ {<, ≤}
and e,
e′ are two linear terms of the form:where vi ∈
V ,
αi ∈
,
for 1 ≤
i ≤
N and d ∈
.
Note that we define the coefficients of the linear inequalities as positive reals. It would be equivalent to define them as positive rationals, since we consider only linear inequalities. Both definitions are found in the literature; we suppose here that, since we are addressing the problem of the verification of real-time systems, we consider real valued constants.
We assume in the following that all inequalities are linear, and we will simply refer to linear inequalities as inequalities.
DEFINITION 1.2.– Let V be a set of variables of the form V = {v1, … , vN }. Given an inequality J on the variables of V of the form e < e′ (respectively, e ≤ e′), the negation of J, denoted by ¬J, is the linear inequality e′ ≤ e (respectively, e′ < e).
DEFINITION 1.3.– Let V be a set of variables of the form V = {v1, … , vN }. A convex linear constraint on the variables of V is a conjunction of inequalities on the variables of V.
We assume in the following that all constraints are both convex and linear, and we will simply refer to convex linear constraints as constraints.
DEFINITION 1.4.– An inequality on the clocks is an inequality on the set of clocks X. A constraint on the clocks is a constraint on the set of clocks X.
DEFINITION 1.5.– An inequality on the parameters is an inequality on the set of parameters P. A constraint on the parameters is a constraint on the set of parameters P.
DEFINITION 1.6.– An inequality on the clocks and the parameters is an inequality on X ∪ P. A constraint on the clocks and the parameters is a constraint on X ∪ P.
Throughout this book, we denote by
the set of all constraints on the clocks, by
the set of all constraints on the parameters and by
the set of all constraints on the clocks and the parameters.
In the following, the letter J will denote an inequality on the parameters, t...
