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

```
SymbolicQuery ::=
'A[]' Expression Subjection
| 'E<>' Expression Subjection
| 'E[]' Expression Subjection
| 'A<>' Expression Subjection
| Expression --> Expression Subjection
| 'sup' ':' List Subjection
| 'sup' '{' Predicate '}' ':' List Subjection
| 'inf' ':' List Subjection
| 'inf' '{' Predicate '}' ':' List Subjection
| 'bounds' ':' List Subjection
| 'bounds' '{' Predicate '}' ':' List Subjection
List ::= Expression | Expression ',' List
Predicate ::= Expression
Subjection ::=
// empty for no subjection
| under StrategyName
```

`Predicate`- an expression over a system state evaluating to either
`true`

or`false`

. The predicate typically refers to a process location, but it can also use integers, logical operations and clock constraints. `Subjection`- indicates whether the query should be subjected to a strategy.

For `sup`

and `bounds`

queries, the list of expressions may not contain clock constraints and must evaluate to either an integer or a clock.

See rail road diagram for the entire SymbolicQuery syntax.

**See also:** Semantics of the Symbolic Queries

`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: Train(1).x, Train(2).x`

- computes the suprema of
`Train(1).x`and`Train(2).x`expressions (maximal values in case of integers, upper bounds, strict or not, for clocks). `sup{Train(1).Crossing}: Train(1).x`

- computes the supremum of
`Train(1).x`but only when`Train(1)`is in`Crossing`. `inf{Gate.Occ}: Gate.len`

- similarly to
`sup`

,`inf`

query computes infimum of the given expression`Gate.len`while process`Gate`is in`Occ`location. When a clock infimum is needed, the state predicate should be used, otherwise the result is trivially`>=0`

. `bounds{Train(1).Crossing}: Train(1).x`

- computes all individual intervals of
`Train(1).x`

when`Train(1)`

is in`Crossing`

. Introduced in UPPAAL 5.1.0-beta5.