Project topics and materials
Get Complete Project Material File(s) Now! »
Modelling real-time constraints
Let X = fx1; : : : ; xng be a finite, non-empty set of variables called clocks. A valuation : X ! R>0 is a mapping from clocks to non-negative real numbers, such that (x1); : : : ; (xn) are called the coordinates of . Equivalently, can be seen as a point in space RX>0. We denote 0 the valuation such that for all x 2 X , (x) = 0. Given a real number d 2 R, we define + d as the valuation such that 8x 2 X ; ( + d)(x) = (x) + d if it exists.1 If d is non-negative, we say that we performed a time elapse of delay d. The time-successors of are the valuations + d with d > 0. Similarly, we refer to all + d in RX>0 with d 6 0 as time-predecessors of . The set of points that are either time-predecessors or time-successors of a valuation form the unique diagonal line in RX>0 that contains . If Y is a subset of X , we define [Y := 0] as the valuation such that 8x 2 Y; ( [Y := 0])(x) = 0 and 8x 2 X nY; ( [Y := 0])(x) = (x). This operation is called a reset of clocks Y. We extend those notions to sets of valuations in a natural way. The set of time-successors of Z RX>0, denoted PostTime(Z), contains the valuations that are time-successors of valuations in Z. The reset of Z RX>0 by Y, denoted Z[Y := 0], contains the valuations [Y := 0] such that 2 Z.
The term atomic constraint will refer to a linear inequality in one of the following forms:
• A strict (resp. non-strict) non-diagonal atomic constraint over clock x 2 X and constant c 2 Q is an inequality of the form x ./ c with ./ 2 f>; <g (resp. ./ 2 f>; 6g).
• A strict (resp. non-strict) diagonal atomic constraint over clocks x and y 2 X and constant c 2 Q is an inequality of the form x y ./ c with ./ 2 f>; <g (resp. ./ 2 f>; 6g). Let > and ? denote two special atomic constraints, defined as x > 0 and x < 0 for an arbitrary x 2 X . A guard g over X is a finite conjunction of atomic constraints over clocks in X . In particular, guards let us define x = c as shorthand for x 6 c ^ x > c, and 1if d is negative, + d may not belong to RX>0 c1 < x < c2 as shorthand for x > c1 ^ x < c2 . A guard is said strict (resp. non-strict, diagonal, non-diagonal) if all of its atomic constraints are strict (resp. non-strict, diagonal, non-diagonal). Guards(X ) denotes the set of all guards over X , and Guardsnd(X ) the subset of non-diagonal guards. For all constants c 2 Q and ./ 2 f>; 6; >; <g, we say that valuation 2 R>X 0 satisfies the atomic constraint x ./ c (resp. x y ./ c), and write j= x ./ c (resp. j= x y ./ c), if (x) ./ c (resp. (x) (y) ./ c). We say that valuation 2 X satisfies guard g , and write = g , if satisfies all atomic constraints g R>0 j g 2 Guards( X ) g X = g in . For , let denote the set of all 2 R>0 such that j . Such sets are called zones and form convex polyhedra of R>X 0. A guard g is said satisfiable when the zone g is non-empty, and a zone is called rectangular when the associated J K guard is non-diagonal. The universal zone refers to > =R>X 0 and the empty zone refers to ? = ;. Guard is the closed version of a satisfiable guard g where every strict g J K 6 or > . constraint of comparison operator < or > is replaced by its non-strict version The zone g J K is the topological closure of Z = g , and is also denoted Z. J K Zones are closed by intersection as g \ g0 = g ^ g 0 Zones are closed by time-successors as PostTime( g ) is equal to g0 , where g0 is obtained from g J K J K c. Zones by removing every non-diagonal atomic constraint of the form x < c or x J K J K J K g g = 6 g = are also closed by reset of clocks J, Kas g [ := 0] = 0 , where 0 if , Y J K ? ; Y X JK J K JK and otherwise g0 is obtained from g by removing every non-diagonal atomic constraint of the form x > c or x > c with x 2 Y, replacing every diagonal atomic constraint of the form x y ./ c with y 2 Y (resp. x 2 Y ) by x ./ c (resp. y 6./ c), and adding the constraint x 6 0 for every x 2 Y . Note that encoding zones by storing their associated guard syntactically as a formula is not efficient, as guards can contain useless constraints. Moreover, it is possible to have different guards associated to the same zone, and for example testing if a zone is equal to another zone is non-trivial in this form.
Encoding constraints as DBMs
A bound (over R) is a pair ( ; c) with 2 f<; 6g and c 2 R. It represents the (open or large) upper bound c in a linear inequality. We introduce additional bounds (<; +1) and (<; ) that will be used for trivial inequalities, and let Bounds(R) denote (f<; 6g R) [ f(<; +1); (<; )g. We say that a real number a 2 R satisfies ( ; c) 2 f<; 6g R if the inequality a c holds. The bound (<; +1) is satisfied by every real and (<; ) is never satisfied. We say that bound ( ; c) is at least as strong as ( 0; c0), denoted ( ; c) 4 ( 0; c0), if all reals satisfying ( ; c) satisfy ( 0; c0), equivalently if c = _ c0 = +1 _ c < c0 _ (c = c0 ^ ( = 0 _ = <)) : This forms a total order over bounds, where the strongest bound is (<; ) and the weakest one is (<; +1). We define a binary operator min over bounds that returns the strongest bound out of its arguments, and an infimum inf over sets of bounds that returns the weakest bound that is at least as strong as every bound in the set. We also define an addition + such that ( ; c) + ( 0; c0) = ( 00; c + c0) ; with 00 set to 6 if = 0 = 6 and to < otherwise, and where c + c0 uses the + operator of the tropical semiring (R [ f ; +1g; min; +).3 The min operation admits (<; +1) as neutral element and (<; ) as absorbing element, and + admits (6; 0) as neutral element and (<; +1) as absorbing element.
Then, (Bounds(R); min; +) is a semiring that we call the tropical semiring of bounds over R. It is an ordered semiring because min is selective. The order v induced by min in (Bounds(R); min; +) is f(a; b) j b 4 ag. Then, (Bounds(R); min; +) forms a complete join semilattice with v where join is the inf operator. Therefore, (Bounds(R); min; +) is an ordered semiring with closure. The closure of a bound ( ; c) is equal to: (<; 0) if ( ; c) = (<; 0); (<; ) if c < 0; and (6; 0) otherwise (i.e. if (6; 0) 4 ( ; c)). )g We define bounds over a subset Q of R with Bounds(Q) = (f<; 6g Q)[f(<; +1); (<; in a similar fashion. Recall that QN denotes the rational numbers of granularity 1=N with N 2 N>0, and consider the tropical semiring of bounds over QN , defined as (Bounds(QN ); min; +). It inherits the properties of (Bounds(R); min; +) and is an ordered semiring with closure.
Zone abstraction, symbolic algorithms
While the region abstraction gives optimal complexity results for reachability and Büchi conditions, techniques based on constructing the region abstraction struggle with run-time efficiency, mostly because of the large state-space to explore. Practical implementations rely on so-called symbolic techniques instead, where zones are used to represent sets of regions and where the region abstraction is constructed on the fly. Let ZonesN (X ; M) be the set of zones associated with guards in GuardsN (X ; M). This is a finite set since these zones are finite unions of regions in RegN (X ; M). Let Zones(X ; M) denote Zones1(X ; M). The following elementary operations can be defined on zones Z 2 Zones(X ; M):
• Time elapse, as PostTime<M (Z) = PostTime(Z) \ RX>0;<M .
• Intersection with a guard g 2 Guardsnd1(X ; M), as Z \ JgK.
• Reset of Y X , with ResetY(Z) = Z[Y := 0].
Their output is also a zone in Zones(X ; M), which let us define the successor of a zone Z by an edge e = (‘; a; g; Y; ‘0) as Poste(Z) = ResetY(JgK \ PostTime<M (Z)). Given a timed automaton A = hL; X ; ; E i such that all clocks are bounded by M and all guards belong to Guardsnd1(X ; M), we define the zone abstraction7 of A as the transition system hL Zones(X ; M); T i labelled over E, where states (‘; Z) are called zone states and where T contains all transitions (‘; Z!)e (‘0; Z0) such that e is an edge of A from ‘ to ‘0 , Z0 = Poste(Z) and Z0 6= ;. The zone abstraction of A is a finite transition system, and can be seen as a symbolic representation of the region abstraction of A by interpreting zones as sets of regions. Recall that if is a valuation then the region [ ] is a zone that contains . The zone abstraction inherits properties from the region abstraction, most notably its language over starting from (‘0; [ 0]) is equal to the untimed language of A starting from (‘0; 0), and therefore the zone abstraction is equivalent to A w.r.t. the emptiness and model-checking problems.
Given an initial configuration (‘0; 0), we say that a zone state (‘; Z) is reachable from (‘0; 0) if there exists a path in the zone abstraction from (‘0; [ 0]) to (‘; Z). The zone abstraction contains a number of states exponential in the size of A, but the ones not reachable from (‘0; 0) can be ignored. Algorithm 2.1 describes the classical forward exploration technique, computing the set of all zone states reachable from an initial configuration (‘0; 0). It uses two sets of zone states, Passed and Waiting, to explore the zone abstraction, starting from (‘0; Z0) = (‘0; [ 0]). At every step, we select a zone state (‘; Z) of Waiting, check if it is in Passed, and if not we add (‘; Z) to Passed and its successors to Waiting. All elementary operations on zones can be implemented efficiently using DBMs in normal form (see Section 2.2).
Table of contents :
Remerciements
Résumé
Abstract
Introduction
I. Controller synthesis and timed systems
1. Finite systems
1.1. Transition systems
1.2. Weighted transition systems
1.2.1. Semirings, closure operation
1.2.2. Transition systems labelled over a semiring
1.3. Turn-based game on a transition system
1.3.1. Attractors
2. Timed systems
2.1. Modelling real-time constraints
2.2. Encoding constraints as DBMs
2.3. Timed automata
2.3.1. Bounded clocks
2.3.2. Regions
2.3.3. Region abstraction, region automaton
2.3.4. Integer constants
2.3.5. Zone abstraction, symbolic algorithms
II. Robust controller synthesis
3. The perturbation game
4. A region-based approach
4.1. Robustness of region paths
4.1.1. Controllable predecessors
4.1.2. Shrunk DBMs
4.1.3. Non-punctual region path
4.2. Aperiodic cycles
4.3. Generalization from region paths to paths
5. A symbolic approach
5.1. Reachability relation of a path
5.1.1. Constraint graphs
5.1.2. Encoding paths
5.1.3. From constraint graphs to reachability relations
5.1.4. Checking inclusion
5.1.5. Computation of Pre and Post
5.2. Robust iterability of a lasso
5.2.1. Controllable predecessors and their greatest fixpoints
5.2.2. Branching constraint graphs
5.2.3. Solving the qualitative problem for a lasso
5.3. Synthesis of robust controllers
5.3.1. Abstraction of lassos
5.3.2. Forward Analysis
5.3.3. Robust cycle search
5.4. Case study
6. The quantitative problem
6.1. Parametric DBMs
6.1.1. Piecewise affine bounds
6.1.2. Piecewise affine DBMs
6.2. Largest admissible perturbation of a lasso
III.Weighted timed games
7. Finite weighted games
7.1. The untimed setting
7.1.1. Problems
7.2. Solving weighted games
7.2.1. Value iteration
7.2.2. Optimal strategies
7.2.3. Safely removing states of infinite value
7.3. Divergent weighted games
7.3.1. SCC analysis
7.3.2. Computing values in polynomial time
7.3.3. Polynomial lower bound
7.3.4. Deciding divergence
7.4. Almost-divergent weighted games
7.4.1. SCC analysis
7.4.2. Kernel of an almost-divergent weighted game
7.4.3. Semi-unfolding
7.4.4. Deciding almost-divergence
8. Weighted timed games
8.1. The timed setting
8.1.1. Region and corner-point abstractions
8.1.2. Problems
8.1.3. Related work
9. Analysable classes of WTGs
9.1. Main results
9.1.1. On the value problem
9.1.2. On the value approximation problem
9.2. Cycle-based analysis
9.2.1. Cycles in a 0-isolated WTG
9.2.2. SCC-based characterisations
9.3. The membership problem
9.3.1. Deciding divergence
9.3.2. Deciding almost-divergence
10.Computing values
10.1. Symbolic value iteration
10.1.1. Value functions as nested partitions
10.1.2. Operations over value functions
10.1.3. Tubes and diagonals
10.1.4. Exponential vs doubly-exponential
10.1.5. Bounding partial derivatives
10.2. Divergent weighted timed games
11.Approximating values
11.1. Kernel of an almost-divergent WTG
11.2. Semi-unfolding of almost-divergent WTGs
11.2.1. Semi-unfolding construction
11.2.2. Semi-unfolding correctness
11.3. Approximation of almost-divergent WTGs
11.3.1. Approximation of kernels
11.3.2. Approximation of almost-divergent WTGs
11.4. Example of an execution of the approximation schema
11.5. Symbolic approximation algorithm
11.5.1. Discussion
Conclusion
