To define timed I/O automata, timed game automata of TIGA with the following constraints are used:

  • Invariants may not be strict.
  • Inputs must use controllable edges.
  • Outputs must use uncontrollable edges.
  • All channels must be declared broadcast.
  • The system is implicitly input enabled due to broadcast communication but for refinement checking purposes, the relevant inputs must be explicit in the model.
  • In the case of parallel composition of several components, a given output must be exclusive to one component.
  • For implementations, outputs must be urgent.
  • For implementations, every state must have independent time progress, i.e., progress must be ensured by either an output or infinite delay.
  • Tau transitions (no output or input) are forbidden.
  • Global variables are forbidden.

The grammar for specifying property is given by:

Property := 'consistency:' System | 'refinement:' System '<=' System | 'specification:' System | 'implementation:' System  
System := ID | '(' System Expr ')' | '(' Composition Expr ')' | '(' Conjunction Expr ')' | '(' Quotient Expr ')'  
Composition := System '||' System | Composition '||' System  
Conjunction := System '&&' System | Conjunction '&&' System  
Quotient := System '\' System  
Expr := /* nothing */ | ':' tctl  

In particular the grammar can generate expressions of the type refinement: (A || B) <= (C : A[] not C.unsafe). As a reminder the tctl formulas supported are

  • A[ p U q ]
    For all path p must be satisfied until q with the twist (due to the game setting) that p must still hold when q holds.
  • A<> q
    Equivalent to A[ true U q ].
  • A[ p W q ]
    The weak until variant.
  • A[] p
    Equivalent to A[ p W false ].
  • A[] (p && A<> q)
    This is the Büchi objective formula with safety. for all path p must always hold and q must always be reachable from all states.
  • A[] A<> q
    Equivalent to A[] (true && A<> q).

The formulas involving a Büchi objective can be used to constrain the behaviours to be non-zeno by adding an observer automata that visits a state when time elapses.</e<=i)>

Known Issues