Requirements Specification

This section describes a BNF-grammar for the requirement specification language used in the verifier of UPPAAL.

Symbolic Queries

Symbolic queries are performed using symbolic operations based on symbolic semantics of timed automata and correspond to a mathematically rigorous proof.

SymbQuery ::=
        'A[]' Expression Subjection
      | 'E<>' Expression Subjection
      | 'E[]' Expression Subjection
      | 'A<>' Expression Subjection
      | Expression --> Expression Subjection

      | 'sup' ':' List Subjection
      | 'sup' '{' Expression '}' ':' List Subjection

      | 'inf' ':' List Subjection
      | 'inf' '{' Expression '}' ':' List Subjection

List ::= Expression | Expression ',' List

Subjection ::=
	    // empty for no subjection
	  | under StrategyName

Subjection

indicates whether the query should be subjected to a strategy.

For sup properties, expression may not contain clock constraints and must evaluate to either an integer or a clock.

See also: Semantics of the Symbolic Queries

Examples

A[] 1<2

invariantly 1<2.

E<> p1.cs and p2.cs

true if the system can reach a state where both process p1 and p2 are in their locations cs.

A[] p1.cs imply not p2.cs

invariantly process p1 in location cs implies that process p2 is not in location cs.

A[] not deadlock

invariantly the process is not deadlocked.

sup: list

the property is always true and returns the suprema of the expressions (maximal values in case of integers, upper bounds, strict or not, for clocks).

sup{expression}: list

The expressions in the list are evaluated only on the states that satisfy the the expression (a state predicate) that acts like an observation.

The inf formula

is similar to sup but for infima. A state predicate should be used when a clock infimum is asked otherwise the trivial result is ≥0.

Controller Synthesis Queries

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.

TIGAQuery ::=
        ControlSpecifier Goal Subjection
      | CollaborativeControlSpecifier Goal Subjection
      | PartialControlSpecifier Goal Subjection
      | TimeEfficientGameSpecifier Goal

ControlSpecifier ::=
        'control:'

CollaborativeControlSpecifier ::=
        'E<>' 'control:'

PartialControlSpecifier ::=
        '{' List '}' 'control:'

TimeEfficientGameQuery ::=
        'control_t*' '(' GameTimeLimitExpression ',' LocalGameTimeLimitExpression '):'
      | 'control_t*' '(' u '):'
      | 'control_t*:'

Goal ::=
        'A<>' WinExpression
      | 'A[' NotLooseExpression 'U' WinExpression ']'
      | 'A[' NotLooseExpression 'W' WinExpression ']'
      | 'A[]' NotLooseExpression

WinExpression ::= Expression

NotLooseExpression ::= Expression

GameTimeLimitExpression ::= Expression

LocalGameTimeLimitExpression ::= Expression

Subjection ::=
	    // empty for no subjection
	  | under StrategyName

GameTimeLimitExpression

describes a time limit within the game must be won. This expression is only evaluated once at the beginning, thus should not depend on the current state.

LocalGameTimeLimitExpression

describes an additional time limit such that the game can be won within GameTimeLimitExpression - LocalGameTimeLimitExpression time units. This expression is evaluated in each state, and can therefore depend on state or clock constraints. Must be side-effect free.

Examples

control: E<> goal

compute a strategy where goal 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[] safe

compute a strategy where safe state predicate is always true no matter what the oponent/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.

See also Strategy Queries below on how to store and query the properties of the computed strategies.

Statistical Queries

Statistical queries are decided using concrete semantics of stochastic hybrid automata over a number of bounded concrete simulation runs and correspond to empirical measurements of the system performance. The results are of statistical estimate nature and may vary across different executions based on uncertainties specified in Statistical parameters.

SMCQuery ::=
	    Simulate Subjection
      | Probability Subjection
      | ProbUntil Subjection
      | Probability ( '<=' | '>=' ) PROB Subjection
      | Probability Subjection '>=' Probability Subjection
      | Estimate Subjection

Simulate ::= 'simulate'  '[' SMCBounds ']' '{' List '}' [ ':' [ SATRUNS ':' ] Expression ]

Probability ::=
        'Pr' MITLExpression
      | 'Pr[' SMCBounds ']' '(' PathType Expression ')'

ProbUntil   ::= 'Pr[' SMCBounds ']' '(' Expression 'U' Expression ')'

Estimate ::= 'E[' SMCBounds ']' '(' ('min:' | 'max:') Expression ')'

SMCBounds ::= BoundType [ ; RUNS ]

BoundType ::= (  | Clock | '#' ) '<=' BOUND

PathType ::= ( '<>' | '[]' )

Subjection ::=
	    // empty for no subjection
	  | under StrategyName

BOUND

is a non-negative integer constant denoting an upper bound over the absolute global time (when a variable is not specified), specific Clock (cost) variable or a number of action-transitions (#).

RUNS

is an optional positive integer constant denoting the maximum number of runs. If the number of runs is not specified, then it is decided based on Statistical parameters and the particular estimation algorithm.

SATRUNS

is an optional positive integer constant denoting the maximum number of runs that satisfy the state expression.

PROB

is a floating point number from interval [0; 1] denoting a probability bound.

’#’

means a number of simulation steps – discrete edge-transitions – in the run.

‘min:’

means the minimum value over a run of the proceeding expression.

‘max:’

means the maximum value over a run of the proceeding expression.

All expressions are state predicates and must be side effect free. It is possible to test whether a certain process is in a given location using expressions on the form process.location.

See also: Semantics of the SMC Queries

Examples

simulate [<=10] { x }

createss one stochastic simulation run of up to 10 time units in length and plot the values of x expression over time (after checking, right-click the query and choose a plot).

simulate [c<=10] { x, y+z }

creates one simulation run of up to 10 cost units in terms of clock variable c and plot the values of x and y+z expressions over the cost c.

simulate [#<=10] { x, y+z }

creates one simulation run of up to 10 edge-transitions and plot the values of x and y+z expressions over the discrete simulation steps (edge-transitions).

simulate [<=10; 100] { x, y+z } : 2 : goal

selects up to 2 simulation runs from 100 simulations of up to 10 time units in length, which satisfy goal state predicate, and then plot the values of expressions x and y+z over time. The query will also estimate a probability confidense interval of the expression goal being true just like in Pr query. The confidence level is controlled by α-level of significance in the Statistical parameters.

Pr[<=10](<> good)

runs a number of stochastic simulations and estimates the probability of good eventually becoming true within 10 time units. The number of runs is decided based on the probability interval precision (±ε) and confidence level (level of significance α in Statistical parameters), see CI Estimation for details. The query also computes a probability distribution over time when the predicate good is satisfied (right-click the property and choose a plot).

Pr[c<=10; 100]([] safe)

runs 100 stochastic simulations and estimates the probability of safe remaining true within 10 cost units in terms of clock c.

Pr[<=10](<> good) >= 0.5

checks if the probability of reaching good within 10 time units is greater than 50%. Such query uses Wald’s algorithm to decide the probability inequality and requires fewer runs than probability estimation and explicit comparison. Uses -δ, +δ, α and β Statistical parameters.

Pr[<=10](<> best) >= Pr[<=10](<> good)

checks if the probability of reaching best is greater than reaching good within 10 time units. Such query uses a sequential algorithm to decide the probability inequality and requires fewer runs than probability estimation and explicit comparison. Uses -δ, +δ, u0, u1, α and β Statistical parameters. The query also provides a probability comparison plot over time/cost (right-click the query and choose plot).

E[<=10; 100](max: cost)

estimates the maximal value of cost expression over 10 time units of stochastic simulation. Uses 100 stochastic simulations and assumes that the value follows Student’s t-distribution with 1-α confidence level.

The plots can be super-imposed using the Plot Composer from the Tools menu.

Learning Queries

LearningQuery ::=
        ExpQuantifier '(' Expression ')' '[' BoundType ']' Features? ':' PathType Expression Subjection
	  | ExpQuantifier '[' BoundType ']' Features? ':' PathType Expression Subjection
	  | ExpPrQuantifier '[' BoundType ']' Features? ':' PathType Expression Subjection

ExpQuantifier ::= ( minE | maxE )

ExpPrQuantifier ::= ( minPr | maxPr )

Features ::= '{' List '}' '->' '{' List '}'

Subjection ::=
	    // empty for no subjection
	  | under StrategyName

Features

describes a mapping (state space partition) from a partial state to a player action. The first list maps in the discrete space and trhen the second list maps in continuous space.

Examples

minE(cost) [<=10] { i, j } -> { d, f } : <> goal

learns a strategy by minimizing the expected cost value within 10 time units or when goal predicate becomes true given i, j, d and f observable state expressions. i and j are used for discrete partitioning and d and f are used in continuous partitioning. The goal predicate is deprecated, for best results use a predicate which stops together with the simulation bound, like t>=10, where t is a clock that is never reset.

minE(cost) [<=10] : <> goal

learns a strategy by minimizing the expected cost value withing 10 time units or when goal predicate becomes true given that the entire system state is observable.

maxE(gain) [<=10] : <> goal

learns a strategy by minimizing the expected gain value withing 10 time units or when goal predicate becomes true given that the entire system state is observable.

The learning queries are usually used together with strategy assignment and refinement explained below.

Strategy Queries

Strategy queries allow store, load, reuse and refine the strategies by assigning names to them.

AssignQuery ::=
	    'strategy' StrategyName '=' AssignableQuery

AssignableQuery ::=
        TIGAQuery
	  | LearningQuery
	  | 'loadStrategy' Features '(' Path ')'

NonAssignableQuery ::=
        SymbQuery
	  | SMCQuery
	  | 'saveStrategy' '(' Path ',' StrategyName ')'

StrategyName

indicates the name of a strategy.

Path

is a double-quoted character sequence (string) denoting a file system path.

Examples

strategy Safe = A[] safe

computes a safety/permissive strategy over the timed game model and stores it under the name Safe.

A[] good under Safe

checks that the predicate good is always satisfied when the player/controller sticks to actions permitted by Safe strategy.

E<> goal under Safe

checks that the goal state predicate is eventually satisfied when the player/controller uses Safe strategy.

strategy SafeCheap = minE(cost)[<=10] { i, j } -> { d, f } : <> t>=10 under Safe

refines Safe strategy into SafeCheap by minimizing estimated value of cost expression.

saveStrategy("folder/file.json", Safe)

writes Safe strategy to the file with path folder/file.json.

strategy Safe = loadStrategy{i,j}->{d,f}("folder/file.json")

reads the strategy from the file with path folder/file.json and stores it under the name Safe.