Deterministic Parity Automata – What Are They Good For?

Deterministic parity (word) automata are often introduced as the simplest deterministic automaton model for words of infinite length that can capture all omega

-regular acceptance conditions. As such, they have an important role in formal methods and are useful in control applications (when working with omega

-regular specifications).

Most scientific papers (and lectures) that use parity word automata do not give an example that helps the reader to gain an intuition on why they are defined in the way they are and how they can be used to encode omega

-regular specifications. The role of this document is to provide an example that should help to understand them in a better way. After going through the definition of a parity automaton, we construct multiple automata that encode reactive system specifications and finally discuss what such automata can be used for.

Definition

Given a set

, we denote by S^omega

the set of infinite sequences all of whose elements are in

. A deterministic parity word automaton is defined as a tuple $mathcal{A} = langle Q, Sigma, delta, q_0, c rangle$ with the finite set of states

, the finite alphabet Sigma

, the transition function delta : Q times Sigma rightarrow Q

, the initial state q_0 in Q

, and the coloring function c : Q rightarrow mathbb{N}

A parity word automaton $mathcal{A} = langle Q, Sigma, delta, q_0, c rangle$ defines a language mathcal{L}(mathcal{A})

over words w = w_0 w_1 ldots in Sigma^omega

. Given such a word, mathcal{A}

induces a run rho = rho_0 rho_1 ldots in Q^omega

with

and for every i in mathbb{N}

, we have $rho_{i+1} = delta(rho_i,w_i)$ . We have w in mathcal{L}(mathcal{A})

if and only if rho

is accepting. We say that rho

is accepting (and hence,

is accepted) if and only if the highest value that occurs infinitely often in the sequence $c(rho_0) c(rho_1) c(rho_2) ldots in mathbb{N}^omega$ is even.

Remarks:

The definition of the parity acceptance condition varies slightly between the publications. In publications that contain new game-theoretic results, an infinite run is often defined to be accepting if and only if the lowest color occurring infinitely often along it is even. Likewise, a run can be defined to be accepting if and only if the lowest or highest color occurring infinitely often along it is odd. All of these possible definitions are equivalent, as we can easily translate a coloring function to another coloring function c'(q) = n - c(q) for sufficiently high n in mathbb{N} to switch between whether we are interested in the highest or the lowest color. Likewise, when switching between oddness and evenness for the highest or lowest color occurring infinitely often along a run, we just need to add to all color values.

Colors are also often called priorities in the literature.

Sometimes, deterministic automata do not need to have successor states for every combination of predecessor state and alphabet symbol. If no transition is present, the automaton rejects a word. The model above is equivalent in the sense that we can always introduce a rejecting sink state to which we can divert finite-length runs that should be rejecting.

In this document, we use the above definition (highest color should be even) as it seems to be most common in the area of reactive synthesis, from which we draw the example given below.

A Simple Specification for a Simple Reactive System

We consider an example in which a deterministic parity word automaton is to be constructed that encodes a specification over a reactive system. A reactive system reads, in every of its computation cycles, the values of its input propositions and writes the values of its output propositions. The propositions of the reactive system that we are concerned with in this example are depicted in the following image:

A reactive system operates in steps. In every step, the system reads the values of its input propositions and writes the values of its output propositions. The system has no designated time of going out of service, so the traces of the system that collect the input and output in every computation cycle are infinitely long. An example trace of the system is:

In every tuple, the upper-most element represents the value of

, while the other elements represent

and

. A specification now categorizes traces into those that satisfy it and those that do not. Typically, specifications are used to check some implementation of a reactive system for correctness or as a starting point to the automatic synthesis of reactive system implementations. For a specification given as a parity automaton, all traces that induce accepting runs in the automaton are said to satisfy the specification.

Let us start with a simple automaton that encodes that if

occurs infinitely often in a trace, then also

needs to occur infinitely often in the trace.

$text{ begin{tikzpicture} node[draw,shape=circle,fill=blue!20!white] (a) at (0,0) {makemath{q_0}}; node[draw,shape=circle,fill=blue!20!white] (b) at (2,0) {makemath{q_1}}; node[draw,shape=circle,fill=blue!20!white] (c) at (4,0) {makemath{q_2}}; draw[thick,->,bend left=10] (a) to node[above] {makemath{r overline{g}}} (b); draw[thick,->,bend right=70] (a) to node[below] {makemath{g}} (c); draw[thick,->] (c) to[loop right] node[right] {makemath{g}} (c); draw[thick,->] (b) to[loop above] node[above] {makemath{roverline{g}}} (b); draw[thick,->,bend left=10] (b) to node[above] {makemath{g}} (c); draw[thick,->,bend left=10] (c) to node[below] {makemath{r overline{g}}} (b); draw[thick,->,bend right=70] (c) to node[above] {makemath{overline{rg}}} (a); draw[thick,->,bend left=10] (b) to node[below] {makemath{overline{rg}}} (a); draw[thick,->] (a) to[loop left] node[left] {makemath{overline{rg}}} (a); draw[thick,->] (-0.6,0.6) -- (a); draw[thick,->,fill=black] (-0.6,0.6) circle (0.05cm); end{tikzpicture} }$

The automaton has three states, where all states with the names q_i

for some

have color

. All edges in the automaton are labeled by Boolean formulas that describes the trace characters under which the transition should be taken. So a overline{rg}

transition is taken if both

and

have

values in the trace.

The automaton looks complicated, but is in fact quite simple. Whenever overline{rg}

holds on an element of a trace, the automaton switches to state q_0

. Whenever roverline{g}

holds, it switches to state q_1

, and whenever

holds, it switches to state q_2

Let us now analyze whether the automaton represents the specification that we want it to encode. By the definition of the automaton, we have that q_2

is visited infinitely often if

occurs infinitely often along a trace. Since

is the highest color in the automaton, this means that the automaton accepts such a run. Since

is odd, the only other way for the automaton to accept is if state q_0

is visited infinitely often, but states q_1

and

are not. This means that eventually, states q_1

and

are not visited any more. This happens if neither

nor

appear infinitely often, in which case the specification is fulfilled. If color

is the highest color visited infinitely often, then we know by the structure of the automaton that

appears infinitely often along a trace, but not

. In this case, the trace is rightfully rejected.

Now does this specification make any sense in the real world? If we interpret

as a request signal and

as a grant signal, then the specification tells us that if requests keep coming, a grant should eventually be issued. So the specification could be a part of the properties that some hardware arbiter should fulfill, but the specification is not complete yet.

So let us now make it more complete. Let us assume that the mathit{init}

signal should symbolize whether the system has been correctly initialized. The system is allowed to switch the signal from

a couple of times, but eventually, the signal must stay at a

level. This requirement comes in addition to the one that we already gave above.

Let us implement the additional specification part by modifying the parity automaton from above using intuition. We can do so by adding a state with a color of

that should be visited whenever mathit{init}

was just observed to have a value of

. Thus, if mathit{init}

does not at some point stay at

, we have that the state with color

is visited infinitely often, and hence the trace is rejected. Otherwise, a run of the automaton stays in the states that we already had in the automaton above. The new parity automaton looks as follows:

$text{ begin{tikzpicture} node[draw,shape=circle,fill=blue!20!white] (a) at (-1,0) {makemath{q_0}}; node[draw,shape=circle,fill=blue!20!white] (b) at (2,0) {makemath{q_1}}; node[draw,shape=circle,fill=blue!20!white] (c) at (5,0) {makemath{q_2}}; node[draw,shape=circle,fill=blue!20!white] (d) at (2,-4) {makemath{q_3}}; % draw[thick,->,bend right=20] (a) to node[above right,pos=0.8] {makemath{overline{mathit{init}}}} (d); draw[thick,->,bend left=40] (d) to node[below left,pos=0.5] {*} (a); draw[thick,->,bend left=20] (b) to node[right,pos=0.8] {makemath{overline{mathit{init}}}} (d); draw[thick,->,bend left=30] (c) to node[below right,pos=0.8] {makemath{overline{mathit{init}}}} (d); % draw[thick,->,bend left=10] (a) to node[above] {makemath{{mathit{init}},r overline{g}}} (b); draw[thick,->,bend right=60] (a) to node[above,pos=0.4] {makemath{{mathit{init}},g}} (c); draw[thick,->] (c) to[loop right] node[right] {makemath{{mathit{init}},g}} (c); draw[thick,->] (b) to[loop above] node[above] {makemath{{mathit{init}},roverline{g}}} (b); draw[thick,->,bend left=10] (b) to node[above] {makemath{{mathit{init}},g}} (c); draw[thick,->,bend left=10] (c) to node[below] {makemath{{mathit{init}},r overline{g}}} (b); draw[thick,->,bend right=70] (c) to node[above] {makemath{mathit{init},overline{rg}}} (a); draw[thick,->,bend left=10] (b) to node[below] {makemath{mathit{init},overline{rg}}} (a); draw[thick,->] (a) to[loop left] node[left] {makemath{mathit{init},overline{rg}}} (a); draw[thick,->] (-1.6,0.6) -- (a); draw[thick,->,fill=black] (-1.6,0.6) circle (0.05cm); end{tikzpicture} }$

It may look surprising at first that from state q_3

, the automaton always transitions to q_0

. This is because it does not really matter where the transition goes to. If mathit{init}

maintains a value of

at some point, then the automaton run eventually moves to the states representing the

and

values. On the other hand, if mathit{init}

infinitely often has a value of

, then state q_3

is visited at least on every second occurrence of a trace element in which mathit{init}

has a value of

, so the automaton rejects the word.

The specification encoded by the automaton is still relatively simple. Real-world practical specifications consist of many more properties, and the resulting parity automata are much more complicated then. In particular, so-called safety properties are often added to practical specifications. These state that the system under design should never perform certain specified sequences of actions. Strenghtening a specification represented as a deterministic parity automaton by some safety property can be done without changing the number of colors in the automaton (provided that there was already at least one odd color in the automaton). Since safety properties are quite frequent in practical specifications, but non-safety properties are more rare, this means that parity automata for real-life specifications can often have few colors.

We want to explore this possibility by giving a complete specification for the above arbiter scenario. We write down all requirements that the reactive system should fulfill, and formalize them in linear temporal logic (LTL). While we will not define LTL here (as probably most readers that reached this point of this page will be familiar with it), and just give the translation of the English language specification parts to LTL.

There are tools available to automatically translate LTL formulas into deterministic parity automata. One of them comes with the spot framework. For example, for spot 2.3.5, we can run the following command to compute a deterministic parity automaton for the conjunction of these five LTL properties:

ltl2tgba -G -D -S -d"avc" -f "([]<>r -> []<>g) & <>[]init & [](X X g -> init & X init & X X init ) & ! g & ! X g & [](! g | X ! g) & G(init & ! X init -> ! r & ! X r)" | dot2tex -f tikz

Note that the globally operator ( mathsf{G}

) of LTL is written as [] in this command, while the finally operator ( mathsf{F}

) is given as <>. The ltl2tgba tool of spot computed a parity automaton that looks as follows:

A PDF of the automaton is available here. Note that the graph only shows the colors of some of the states (next to the state numbers), but there are still four different colors, as in the previous automaton. Also, the sink state (from which all suffix words are rejected) is missing from the automaton. The new automaton looks a lot more complicated even though the specification is still quite simple. While at least one other LTL-to-parity-automaton tool produces a smaller automaton for this specification, note that pretty much all automata that encode interesting specifications are quite large, which explains why real-world examples of parity automata are seldomly found in the literature.

At this point, I would like to thank Alexandre Duret-Lutz for helpful suggestions on using spot to generate parity automata.

Ok, What's Their Use Now?

Deterministic parity automata can encode specifications of reactive systems, just like temporal logic formulas or other automaton types over words of infinite length (such as Büchi automata that almost every student taking a formal methods course learns about). Once a specification has been formalized, it can be used in automatic procedures for the verification and/or synthesis of reactive systems.