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   

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 are similar to sup but for infima. A state predicate should be used when a clock infimum is asked otherwise the trivial result is >= 0.

Subjection

indicates whether the query should be subjected to a strategy.

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.

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 the 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 an interval [0;1] denoting a probability bound.

'#'

means a number of simulation steps -- discrete action-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

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 from partial state to .

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.