# Exploring the temporal hierarchy of Manna & Pnueli

## Table of Contents

*A hierarchy of temporal properties* was defined by Manna & Pnueli in
their PODC'90 paper.

This hierarchy relates "properties" (i.e., omega-regular languages) to structural properties of the automata that can recognize them.

## Description of the classes

The hierarchy is built from the classes pictured in the following
diagram, where each class includes everything below it. For instance,
the *recurrence* class includes the *obligation* class which also
includes the *safety* and *guarantee* classes, as well as the unnamed
intersection of *safety* and *guarantee* (`B`

in the picture).

Forget about the LTL properties and about the red letters displayed in this picture for a moment.

- The
*reactivity*class represents all possible omega-regular languages, i.e., all languages that can be recognized by a non-deterministic Büchi automaton. - The
*recurrence*subclass contains all properties that can be recognized by a deterministic Büchi automaton. - The dual class,
*persistence*properties, are those that can be recognized by a weak Büchi automaton (i.e., in each SCC either all states are accepting, or all states are rejecting). - The intersection of
*recurrence*and*persistence*classes form the*obligation*properties: any of those can be recognized by a weak and deterministic Büchi automaton. *Guarantee*properties are a subclass of*obligation*properties that can be recognized by terminal Büchi automata (i.e., upon reaching an accepting state, any suffix will be accepted).*Safety*properties are the dual of*Guarantee*properties: they can be recognized by ω-automata that accept all their runs (i.e., the acceptance condition is "true"). Note that since these automata are not necessary complete, it is still possible for some words not to be accepted. If we interpret the ω-automata with "true" acceptance as finite automata with all states marked as final, we obtain monitors, i.e., finite automata that recognize all finite prefixes that can be extended into valid ω-words.- Finally, at the very bottom is an unnamed class that contains
*Safety*properties that are also*Guarantee*properties: those are properties that can be represented by monitors in which the only cycles are self-loops labeled by true.

The "LTL normal forms" displayed in the above figure help to visualize the type of LTL formulas contained in each of these class. But note that (1) this hierarchy applies to all omega-regular properties, not just LTL-defined properties, and (2) the LTL expression displayed in the figure are actually normal forms in the sense that if an LTL-defined property belongs to the given class, then there exists an equivalent LTL property under the stated form, were \(p\), \(q\), \(p_i\) and \(q_i\) are subexpressions that may use only Boolean operators, the next operator (\(\mathsf{X}\)), and past-LTL operators (which are not supported by Spot). The combination of these allowed operators only makes it possible to express constraints on finite prefixes.

*Obligations* can be thought of as Boolean combinations of *safety*
and *guarantee* properties, while *reactivity* properties are Boolean
combinations of *recurrence* and *persistence* properties. The
negation of a *safety* property is a *guarantee* property (and
vice-versa), and the same duality hold for *persistence* and
*recurrence* properties.

The red letters in each of these seven classes are keys used in Spot to denote the classes.

## Deciding class membership

The `--format=%h`

option can be used to display the "class key" of the
most precise class to which a formula belongs.

```
ltlfilt -f 'a U b' --format=%h
```

G

If you find hard to remember the class name corresponding to the class
keys, you can request verbose output with `%[v]h`

:

ltlfilt -f 'a U b' --format='%[v]h'

guarantee

But actually any *guarantee* property is also an *obligation*, a
*recurrence*, a *persistence*, and a *reactivity* property. You can
get the complete list of classes using `%[w]h`

or `%[vw]h`

:

ltlfilt -f 'a U b' --format='%[w]h = %[vw]h'

GOPRT = guarantee obligation persistence recurrence reactivity

This `--format`

option is also supported by `randltl`

, `genltl`

, and
`ltlgrind`

. So for instance if you want to classify the 55 LTL
patterns of Dwyers et al. (FMSP'98) using this hierarchy, try:

```
genltl --dac-patterns --format='%[v]h' | sort | uniq -c
```

1 guarantee 2 obligation 1 persistence 2 reactivity 12 recurrence 37 safety

In this output, the most precise class is given for each formula, and
the count of formulas for each subclass is given. We have to remember
that the recurrence class also includes obligation, safety, and
guarantee properties. In this list, there are no formulas that belong
to the intersection of the *guarantee* and *safety* classes (it would
have been listed as `guarantee safety`

).

From this list, only 3 formulas are not recurrence properties (i.e.,
not recognized by deterministic Büchi automata): one of them is a
persistence formula, the other two cannot be classified better than in
the *reactivity* class. Let's pretend we are interested in those
three non-recurrence formulas, we can use `ltlfilt -v --recurrence`

to
remove all recurrence properties from the `genltl --dac-pattern`

output:

```
genltl --dac-patterns |
ltlfilt -v --recurrence --format='%[v]h, %f'
```

persistence, G!p0 | F(p0 & (!p1 W p2)) reactivity, G(p0 -> ((p1 -> (!p2 U (!p2 & p3 & X(!p2 U p4)))) U (p2 | G(p1 -> (p3 & XFp4))))) reactivity, G(p0 -> ((p1 -> (!p2 U (!p2 & p3 & !p4 & X((!p2 & !p4) U p5)))) U (p2 | G(p1 -> (p3 & !p4 & X(!p4 U p5))))))

Similar filtering options exist for other classes. Since these tests are automata-based, they work with PSL formulas as well. For instance, here is how to generate 10 random recurrence PSL formulas that are not LTL formulas, and that are not obligations:

randltl --psl -n -1 a b | ltlfilt -v --ltl | ltlfilt -v --obligation | ltlfilt --recurrence -n10

{[*]}<>-> (!a & XG!Ga) F({[*2][*]}[]-> (b M 1)) {[*0] | b[*]}<>-> GFb F{1:{{a | !b} | [*0]}} W (a & b) X{b | [*0]} & GF!b {a[*]}[]-> !Gb !({{[*] & b[*]}[:*1..2]}<>-> F(Ga R b)) a -> G(G{{!{a xor b}}[*]} -> Gb) ({[*]}[]-> a) & GFb XXGF!XX({[*]}[]-> a)

Note that the order of the `ltlfilt`

filters could be changed provided
the `-n10`

stays at the end. For instance we could first keep all
recurrence before removing obligations and then removing LTL formulas.
The order given above actually starts with the easier checks first and
keep the most complex tests at the end of the pipeline so they are
applied to fewer formulas. Testing whether a formula is an LTL
formula is very cheap, testing if a formula is an obligation is harder
(it may involves a translation to automata and a powerset
construction), and testing whether a formula is a recurrence is the
most costly procedure (it involves a translation as well, plus
conversion to deterministic Rabin automata, and an attempt to convert
the automaton back to deterministic Büchi). As a rule of thumb,
testing classes that are lower in the hierarchy is cheaper.

Since option `-o`

(for specifying output file) also honors `%`

-escape
sequences, we can use it with `%h`

to split a list of formulas in 7
possible files. Here is a generation of 200 random LTL formulas
binned into aptly named files:

randltl -n 200 a b -o random-%h.ltl wc -l random-?.ltl

59 random-B.ltl 46 random-G.ltl 11 random-O.ltl 19 random-P.ltl 15 random-R.ltl 44 random-S.ltl 6 random-T.ltl 200 total

## Deciding classes membership syntactically

LTL formulas can also be classified into related classes which we
shall call *syntactic-safety*, *syntactic-guarantee*, etc. See tl.pdf
for the grammar of each syntactic class. Any LTL-definable property
of class C can be defined by an LTL formulas in class syntactic-C, but
an LTL formula can describe a property of class C even if that formula
is not in class syntactic-C (we just know that some equivalent formula
is in class syntactic-C).

`ltlfilt`

has options like `--syntactic-guarantee`

,
`--syntactic-persistence`

, etc. to match formulas from this classes.

Here is how to generate 10 random LTL formulas that describe safety properties but that are not in the syntactic-safety class:

randltl -n-1 a b | ltlfilt -v --syntactic-safety | ltlfilt --safety -n10

F!(!b <-> FGb) !Fb xor G((b xor (Xa M b)) U b) a W F(a -> b) ((0 R Xa) R a) -> Fa X(Xb & (!Ga R Ga)) !Fb <-> (Fb | !X(0)) (1 U b) | F(Fb W (a <-> FXa)) (a M 1) | (!a W a) (G!a W ((b M 1) -> Fa)) -> !a !a -> ((a xor !GFa) W 0)

Since all those formulas describe safety properties, an exercise would
be to suggest equivalent formulas that are in the syntactic-safety
fragment. For instance `b M Gb`

can be rewritten as just `Gb`

, which
belongs to this fragment. In this particular case, ```
ltlfilt
--simplify
```

recognizes this:

```
ltlfilt --simplify -f 'b M Gb'
```

Gb

However in the general case Spot is not able to provide the equivalent formula from the appropriate syntactic class.

## What to do with each class?

### Obligation

Spot implements algorithms from Löding (*Efficient minimization of
deterministic weak ω-automata*, IPL 2001) and Dax et al. (*Mechanizing
the powerset constructions for restricted classes of ω-automata*,
ATVA'07) in order to detect obligation properties, and produce minimal
weak deterministic automata for them.

When running `ltl2tgba -D`

on a formula that represents an
obligation property, you are guaranteed to obtain a minimal (in the
number of states) deterministic weak Büchi automaton that recognizes
it. Note that since the *obligation* class includes the *safety* and
*guarantee* classes, minimal deterministic automata will also be
produced for those classes. Dax et al.'s determinization of obligation
properties combined with Löding's minimization renders obsolete
older algorithms (and tools) that produced minimal deterministic
automata but only for the subclasses of *safety* or *guarantee*.

If `ltl2tgba`

is run without `-D`

(but still with the default `--high`

optimization level), the minimal weak deterministic automaton will
only be output if it is smaller than the non-deterministic automaton
the translator could produce before determinization and minimization.

For instance `Fa R b`

is an obligation:

ltlfilt -f 'Fa R b' --format='%[v]h'

obligation

If we translate it without `-D`

we get a 3-state non-deterministic
automaton (here we use `autfilt --highlight-nondet`

to show where the
non-determinism occurs):

```
ltl2tgba 'Fa R b' | autfilt --highlight-nondet -d
```

Note that the default translation used by `ltl2tgba`

will turn any
syntactic persistence formulas (this includes obligations formulas)
into a weak automaton. In a weak automaton, the acceptance condition
could be defined in term of SCCs, i.e., the cycles of some SCCs are
either all accepting, or all rejecting. As a consequence, it there is
no incentive to use transition-based acceptance; instead, state-based
acceptance is output by default.

With `ltl2tgba -D`

we get a (minimal) deterministic weak Büchi
automaton instead.

```
ltl2tgba -D 'Fa R b' -d
```

When we called `ltl2tgba`

, without the option `-D`

, the two automata
(non-deterministic and deterministic) were constructed, but the
deterministic one was discarded because it was bigger. Using `-D`

forces the deterministic automaton to be used regardless of its size.

The detection and minimization of obligation properties is also used
by `autfilt`

when simplifying deterministic automata (they need to be
deterministic so that `autfilt`

can easily compute their complement).

For instance, let us use `ltl2dstar`

to construct a Streett automaton
for the obligation property `Ga | XFb`

.

ltldo 'ltl2dstar --automata=streett' -f 'Ga | XFb' -d

We can now minimize this automaton with:

ltldo 'ltl2dstar --automata=streett' -f 'Ga | XFb' | autfilt -D -C -d

Here we have used option `-C`

to keep the automaton complete, so that
the comparison with `ltl2dstar`

is fair, since `ltl2dstar`

always
output complete automata.

### Guarantee

*Guarantee* properties can be translated into terminal automata.
There is nothing particular in Spot about *guarantee* properties, they
are all handled like *obligations*.

Again, using `-D`

will always produce (minimal) deterministic Büchi
automata, even if they are larger than the non-deterministic version.
The output should be a terminal automaton in either case,

An example is `a U Xb`

:

ltlfilt -f 'a U Xb' --format='%[v]h'

guarantee

```
ltl2tgba 'a U Xb' | autfilt --highlight-nondet -d
```

```
ltl2tgba -D 'a U Xb' -d
```

### Safety

*Safety* properties also form a subclass of *obligation* properties,
and again there is no code specific to them in the translation.
However, the *safety* class corresponds to what can be represented
faithfully by monitors, i.e., automata that accept all their infinite
runs.

For most safety formulas, the acceptance output by `ltl2tgba`

will
already be `t`

(meaning that all runs are accepting). However since
the translator does not do anything particular about safety formulas,
it is possible to find some pathological formulas for which the
translator outputs a non-deterministic Büchi automaton where not all
run are accepting.

Here is an example:

ltlfilt -f '(a W Gb) M b' --format='%[v]h'

safety

```
ltl2tgba '(a W Gb) M b' | autfilt --highlight-nondet -d
```

Actually, marking all states of this automaton as accepting would not be wrong, the translator simply does not know it.

Using `-D`

will fix that: it then produces a deterministic automaton
that is guaranteed to be minimal, and where all runs are accepting.

```
ltl2tgba -D '(a W Gb) M b' -d
```

If you are working with safety formula, and know you want to work with
monitors, you can use the `-M`

option of `ltl2tgba`

. In this case
this will output the same automaton, but using the universal
acceptance (i.e. `t`

). You can interpret this output as a monitor
(i.e., a finite automaton that accepts all prefixes that can be
extended into valid ω-words).

```
ltl2tgba -M '(a W Gb) M b' | autfilt --highlight-nondet -d
```

```
ltl2tgba -M -D '(a W Gb) M b' -d
```

Note that the `-M`

option can be used with formulas that are not
safety properties. In this case, the output monitor will recognize a
language larger than that of the property.

### Recurrence

*Recurrence* properties can be represented by deterministic Büchi
automata.

For the subclass of *obligation* properties, using `-D`

is a sure way
to obtain a deterministic automaton (and even a minimal one), but for
the *recurrence* properties that are not *obligations* the translator
does not make *too much* effort to produce deterministic automata,
even with `-D`

(this might change in the future).

All properties that are not in the *persistence* class (this includes
the *recurrence* properties that are not *obligations*) can benefit
from transition-based acceptance. In other words using
transition-based acceptance will often produce shorter automata.

The typical example is `GFa`

, which can be translated into a 1-state
transition-based Büchi automaton:

ltlfilt -f 'GFa' --format='%[v]h'

recurrence

```
ltl2tgba 'GFa' -d
```

Using state-based acceptance, at least two states are required. For instance:

```
ltl2tgba -S 'GFa' -d
```

Here is an example of a formula for which `ltl2tgba`

does not produce a
deterministic automaton, even with `-D`

.

ltlfilt -f 'G(Gb | Fa)' --format='%[v]h'

recurrence

```
ltl2tgba -D 'G(Gb | Fa)' | autfilt --highlight-nondet -d
```

One way to obtain a deterministic Büchi automaton (it has to exist, since this is
a *recurrence* property), is to request a deterministic automaton with parity
acceptance using `-P`

. The number of color output with `-P`

is always reduced
to the minimal number possible, so for a *recurrence* property the output
automaton can only have one of three possible acceptance: `Inf(0)`

, `t`

, or `f`

.

```
ltl2tgba -P -D 'G(Gb | Fa)' -d
```

Note that if the acceptance is `t`

, the property is a monitor, and if
its `f`

, the property is `false`

. In any way, if you would like to
obtain a DBA for any recurrent property, a sure way to avoid these
difference is to pipe the result through `autfilt -B`

```
ltl2tgba -P -D 'G(Gb | Fa)' | autfilt -B -d
```

It is likely that `ltl2tgba -B -D`

will implement these steps in the
future, but so originally `-D`

was only expressing a preference not a
requirement.

### Persistence

Since *persistence* properties are outside of the *recurrence* class,
they cannot be represented by deterministic Büchi automata. The typical
persistence formula is `FGa`

, and using `-D`

on this is hopeless.

ltl2tgba -D FGa -d

However since the **negation** of `FGa`

is a *recurrence*, this negation
can be represented by a deterministic Büchi automaton, which means
that `FGa`

could be represented by a deterministic co-Büchi automaton.
`ltl2tgba`

does not generate co-Büchi acceptance, but we can do the
complementation ourselves:

ltl2tgba --negate -D FGa | autfilt --complement -d

Note that in this example, we know that `GFa`

is trivial enough that
`ltl2tgba -D GFa`

will generate a deterministic automaton. In the
general case we might have to determinize the automaton using `-P -D`

as
we did in the previous section. For persistence properties, `-P -D`

should
return an automaton whose acceptance is one of `Fin(0)`

, `t`

, or `f`

.

*Persistence* properties can be represented by weak Büchi automata.
The translator is aware of that, so when it detects that the input
formula is a syntactic-persistence, it simplifies its translation
slightly to ensure that the output will use at most one acceptance
set. (It is possible to define a persistence properties using an LTL
formula that is not a syntactic-persistence, in that case this
optimization is simply not applied.)

If the input is a weak property that is not syntactically weak, the output will not necessarily be weak. One costly way to obtain a weak automaton for a formula \(\varphi\) would be to first compute a deterministic co-Büchi automaton \(\varphi\) then transform that into a Büchi automaton.

Let's do that on the persistence formula `F(G!a | G(b U a))`

, just for
the fun of it.

ltlfilt -f 'F(G!a | G(b U a))' --format='%[v]h'

persistence

Unfortunately the default output of the translation is not weak:

```
ltl2tgba 'F(G!a | G(b U a))' -d
```

So let's determinize using parity acceptance:

```
ltl2tgba -P -D 'F(G!a | G(b U a))' -d
```

And finally we convert the result back to Büchi with `autfilt -B`

.

```
ltl2tgba -P -D 'F(G!a | G(b U a))' | autfilt -B --highlight-nondet --small -d
```

That is indeed, a weak non-deterministic automaton.