Skip to main content.


In this help section we give a BNF-grammar for the requirement specification language used in the verifier of UPPAAL.

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

All expressions 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 Requirement Specification Language


  • 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.