Controller synthesis queries are decided using symbolic techniques over Timed Game (TIGA) automata, where the discrete actions are either controllable (controller’s actions, solid edges) or uncontrollable (environment actions, dashed edges). The result is either a strategy solving the game objective or that the strategy does not exist.
ControlQuery ::=
ControlSpecifier Goal Subjection
| CollaborativeControlSpecifier Goal Subjection
| PartialControlSpecifier Goal Subjection
| TimeEfficientGameSpecifier Goal
| ApproximateControlSpecifier // In section below
| TatlExpression // In section below
ControlSpecifier ::=
'control:'
CollaborativeControlSpecifier ::=
'E<>' 'control:'
PartialControlSpecifier ::=
'{' List '}' 'control:'
TimeEfficientGameQuery ::=
'control_t*' '(' GameTimeLimitExpression ',' LocalGameTimeLimitExpression '):'
| 'control_t*' '(' u '):'
| 'control_t*:'
Goal ::=
'A<>' WinExpression
| 'A[' NotLoseExpression 'U' WinExpression ']'
| 'A[' NotLoseExpression 'W' WinExpression ']'
| 'A[]' NotLoseExpression
WinExpression ::= Expression
NotLoseExpression ::= Expression
GameTimeLimitExpression ::= Expression
LocalGameTimeLimitExpression ::= Expression
Subjection ::=
// empty for no subjection
| under StrategyName
See rail road diagram for the entire ControlQuery syntax.
control: E<> goalgoal state predicate is eventually true no matter what the oponent/environment chooses to do. The resulting strategy is deterministic in a sense that for a given state the strategy proposes one action for the player/controller (while the oponent/environment may still choose from multiple actions).control: A[] safesafe state predicate is always true no matter what the opponent/environment chooses to do. The strategy is permissive in a sense that for a given state the strategy may propose multiple actions for the player/controller. Such permissive strategy can be thought of as a union of all strategies satisfying the predicate, therefore it does not have any notion of progress and may include infinite loops.A[ safe U goal ]goal is reached.A[ safe W goal ]goal) either a safety strategy is found or a safety strategy holds until the goal is reached.See also Strategy Queries below on how to store and query the properties of the computed strategies.
The query is available in the UPPAAL COSHY version only.
Synthesize a strategy to enforce a desired invariant, using approximation techniques. The strategy is a user-defined partition of hyper-rectangular “cells” of equal size. For each cell, the strategy gives a set of safe edges to take.
ApproximateControlSpecifier ::=
'acontrol : A[] ' DesiredInvariantExpression Partition
DesiredInvariantExpression ::= Expression
Partition ::=
'{' Interval (',' Interval)* '}'
Interval ::=
Identifier '[' Integer ',' Integer ']' // (1)
| Identifier '[' Double ',' Double ']' ':' Integer // (2)
| Identifier '.location' // (3)
The partition should include all state variables. Excluding state-variables may produce an invalid strategy, but can be done for e.g. cost variables that have no impact on safety. Integer variables must be included as a bounded interval (1).
Double and clock variables must be bounded and indicate the number of discrete buckets the interval will be split into (2).
For example, for clock x, the interval x[0.1, 0.2]:4 discretizes x into [0.1, 0.125), [0.125, 0.15), [0.15, 0.175) and [0.175, 0.2).
The location of processes must also be included (3). For example, WaterTank.location. Since the number of locations is discrete and bounded, nothing else needs to be specified.
strategy shield = acontrol: A[] water_level < 10 && water_level > 0 { WaterTank.location, water_level[-1, 11]:24 }
Declares a strategy called shield to enforce the desired invaraint water_level < 10 && water_level > 0. The system has two, state variables. First, the WaterTank template has 5 locations, so WaterTank.location has 5 possible values. The second variable, water_level[-1, 11]:24 is a double which gets split up into 24 intervals, with the corresponding size of 0.5. So the partition will contain 5ยท24 = 120 cells.
TATL queries are available in the UPPAAL TATL version only.
TatlExpression ::=
Expression
| ('!' | 'not') TatlExpression
| TatlExpression '&&' TatlExpression
| TatlExpression '||' TatlExpression
| Identifier '@' TatlExpression // (A)
| TatlCoalition TatlPathProp
;
TatlCoalition ::=
'<<' PlayerColorList '>>' // (B1)
| '[[' PlayerColorList ']]' // (B2)
;
TatlPathProp ::=
'[' TatlExpression 'U' TatlExpression ']' // (C1)
| '<>' TatlExpression // (C2)
| '[]' TatlExpression // (C3)
| 'X' TatlExpression // (C4)
;
PlayerColorList ::=
/* empty */
| PlayerColorListNonEmpty
;
PlayerColorListNonEmpty ::=
PlayerColor
| PlayerColorListNonEmpty ',' PlayerColor
;
PlayerColor ::=
'black' | 'lightgray' | 'darkgray' | 'red' | 'green' | 'blue' | 'yellow' | 'cyan' | 'magenta' | 'orange' | 'pink' ;
Alternating-Time Temporal Logic (ATL) is an extension of computation-tree logic (CTL), where the traditional for-all- and exists path quantifiers have been replaced with strategy quantifiers, quantifying over the possible outcome paths resulting from a coalition of players working together. The timed extension comes from the addition of the freeze operator.
z @ RHS is holds if the right-hand side holds after the clock z is reset in the current state.<< S >> rho (B1) is satisfied if there exist strategies for the players S such that all outcome paths satisfies path property rho. Can be read as “S can guarantee rho”.[[ S ]] rho (B2) is satisfied if under all strategies the players S there exists an outcome path satisfying rho. Can be read as “S cannot prevent rho”.<< >> is equivalent to A, and [[ ]] is equivalent to E.X is the next location operator.TATL queries are defined over timed multi-player games. A TATL query considers each edge color a different player (it does not matter if an edge is marked uncontrollable).
There are 11 different edge colors available in the UPPAAL GUI and they are referred to using their natural language name, i.e. red, green, blue, etc.
The semantics are similar to that of a standard 2-player game. The player red may activate enabled red edges at any time, and must do it in a timed-locked state, if any is enabled.
If two players activate an edge in the same instant, it is non-deterministic which activation happens.
If a synchronization involves more than one player, it is consider “uncontrollable”, unless they are all working together.
<< green >> [] safegreen such that only safe states are visited (despite the actions of other players).[[ red ]] [ safe U safe && goal ]safe states until eventually reaching a safe goal state despite the actions of player red.<<>> [] (<<red, blue>> <> goal)red and blue can cooperate such that goal is eventually reached.z @ (<< green, blue >> [ (safe && z <= 5) U (safe && goal) ])green and blue can cooperate to reach a safe goal state within 5 time units and only visiting safe states along the way (z is a global clock).