# GPSL syntax: LTL & Buchi

**Generic Property Specification Language** (GPSL) is the language used by OBP2 for specifying the properties that should be verified during the analysis. Currently it supports Linear Temporal Logic and Buchi Automata specifications.

GPSL is **only** a *property-specification* language. Methodologically it is orthogonal from the formalisms used for *capturing the operational environment* (xGDL scenarios) and for *taming the state-space explosion* problem during model-checking (state-space decomposition, pruning through state-constraints - TLA, etc.).

The main characteristic of GPSL is its independence from the formalism used for model-specification. To achieve this independece relation, the GPSL language delegates the evaluation of the atomic properties to the *verification model* semantics. Thus, from the perspective of the specification language, the atomic proposition are simply a mapping of names to booleans. In other words, the GPSL semantics binds the *property* to the *verification model* through a semantics-driven evaluation function.

In GPSL each property is associated with a named variable. All these variables form the *property set*
Any *property* can be verified during an analysis run.

### Propositional Logic: Syntax & Semantics

There are two Boolean constants predefined in the language: **true** and **false**

Atomic proposition in GPSL are strings of characters enclosed between pairs of `|`

(ie. `| string of characters |`

). Each atomic proposition can be prefixed with two identifiers specifying the atomic proposition language and the ‘verification’ module on which it should be interpreted.

### Boolean Operators

Two expressions f and g can be combined using the following Boolean operators

Operation | syntax0 | syntax1 | syntax2 | syntax3 | syntax4 |
---|---|---|---|---|---|

negation | not f | !f | ~f | ||

disjunction | f or g | f | g | f \/ g | f + g | |

conjunction | f and g | f & g | f && g | f /\ g | f * g |

exclusion | f xor g | f ^ g | |||

implication | f implies g | f -> g | f => g | ||

equivalence | f iff g | f <-> g | f <=> g |

### Let Expressions

To simplify the expression of large formula GPSL uses Let expression forms to introduce variables.

```
let
v1 = expr
v2 = expr
...
vn = expr
in
v1 op v2
```

## Temporal Logic: Syntax & Semantics

The support for LTL is enabled using LTL3Buchi conversion [1].

### Temporal Logic Operators

Two expressions f and g can be combined using the following Boolean operators

operation | syntax0 | syntax1 | syntax2 |
---|---|---|---|

Next | X f | next f | () f |

Eventually | F f | eventually f | <> f |

Always | G f | globally f | [] f |

Strong Until | f U g | f until g | |

Weak Until | f W g | ||

Weak Release | f R g | f release g | f V g |

Strong Release | f M g |

#### Some LTL examples

```
aliceCS = |{Alice}1@CS|
bobCS = |{Bob}1@CS|
exclusionI = []!(|{Alice}1@I| && |{Bob}1@I|)
exclusion = []!(aliceCS && bobCS)
eventuallyOneInCS = []<>(aliceCS || bobCS)
fairness =
let
aliceFlagUP=|{sys}1:flags[0] = true|,
bobFlagUP=|{sys}1:flags[1] = true|
in
([] ( (aliceFlagUP -> (<> aliceCS) )
&& (bobFlagUP -> (<> bobCS))))
idling = let
aliceFlagUP=|{sys}1:flags[0]=true|,
bobFlagUP=|{sys}1:flags[1]=true|
in
([] (!aliceFlagUP -> (![] aliceCS))
&& (!bobFlagUP -> (![] bobCS)) )
infoften = [] <> bobCS
all = (exclusion & eventuallyOneInCS & fairness & idling)
```

### Buchi Automata

Buchi Automata can be used for expressing properties. In this case the syntax for atomic propositions stays the same. The named variables, used in the automaton, are restricted to propositional logic constructs. The in clause of the let construct is extended with the syntactical term for describing the automaton. In this context an automaton is composed of 4 parts :

- the set of states
- the initial state(s)
- the accepting state(s)
- the guarded transitions

The set of state is defined by the keyword *states* followed by a comma delimited list of identifiers (state names)

```
states_rule := 'states' identifier (',' identifier)*
```

The initial state(s) are introduced with the keyword *initial* followed by a comma delimited list of state names

```
initial_rule := 'initial' identifier (',' identifier)*
```

The accepting state(s) are introduced with the keyword *accept* followed by a comma delimited list of state names

```
accept_rule := 'accept' identifier (',' identifier)*
```

Each transition is specified by the source state, the guard expression, and the target state, where the source and target state are state identifiers, and the guard expression is a propositional logic expression composed using literals (true, false), atomic propositions (|…|), propositional operators (!, and, or, ->, etc), and named variable references.

```
transition_rule := identifier '[' expression ']' identifier
```

The automaton is defined by the following syntax:

```
automaton_rule :=
states_rule ';'
initial_rule ';'
accept_rule ';'
transition_rule (';' transition_rule)*
```

#### Buchi Automaton Example

Automaton as named property :

```
aut1 =
states s0, s1;
initial s0;
accept s1;
s0 [ |a=5| ] s1;
s0 [ true ] s0;
s1 [ |b=7| and |c=2| ] s1
```

Automaton in let expression :

```
b1 = let
a1 = |P_1!=wait|,
a2 = |P_0=choose|,
a3 = |P_2!=choose|,
a4 = |number[1]<0|,
p1 = !a3 and !a4,
p2 = a3 and a4,
in
states s0, s1, s2, s3;
initial s0;
accept s2, s3;
s0 [!a2 and !a1] s1;
s0 [(!a1 and p1) or (!a1 and p2)] s2;
s0 [a1] s3;
s1 [!a2] s1;
s1 [|P_1==wait|] s2;
s2 [p1] s2;
s3 [true] s3
```

## References

[1] Babiak, Tomáš, et al. “LTL to Büchi automata translation: Fast and more deterministic.” International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, Berlin, Heidelberg, 2012.