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 regular acceptance conditions. As such, they have an important role in formal methods and are useful in control applications (when working with 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 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. DefinitionBefore we can give an example, we need to define what we are talking about. Given a set , we denote by the set of infinite sequences all of whose elements are in . A deterministic parity word automaton is defined as a tuple with the finite set of states , the finite alphabet , the transition function , the initial state , and the coloring function . A parity word automaton defines a language over words . Given such a word, induces a run with and for every , we have . We have if and only if is accepting. We say that is accepting (and hence, is accepted) if and only if the highest value that occurs infinitely often in the sequence is even. Remarks: The definition of the parity acceptance condition varies slightly between the publications. In publications that contain new gametheoretic 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 for sufficiently high 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 finitelength 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 SystemWe 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 uppermost 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. The automaton has three states, where all states with the names 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 transition is taken if both and have values in the trace. The automaton looks complicated, but is in fact quite simple. Whenever holds on an element of a trace, the automaton switches to state . Whenever holds, it switches to state , and whenever holds, it switches to state . 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 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 is visited infinitely often, but states and are not. This means that eventually, states 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 signal should symbolize whether the system has been correctly initialized. The system is allowed to switch the signal from to 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 was just observed to have a value of . Thus, if 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: It may look surprising at first that from state , the automaton always transitions to . This is because it does not really matter where the transition goes to. If 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 infinitely often has a value of , then state is visited at least on every second occurrence of a trace element in which has a value of , so the automaton rejects the word. The specification encoded by the automaton is still relatively simple. Realworld practical specifications consist of many more properties, and the resulting parity automata are much more complicated then. In particular, socalled 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 nonsafety properties are more rare, this means that parity automata for reallife 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.
In LTL, these properties can be written as: 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 () of LTL is written as [] in this command, while the finally operator () 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 LTLtoparityautomaton tool produces a smaller automaton for this specification, note that pretty much all automata that encode interesting specifications are quite large, which explains why realworld examples of parity automata are seldomly found in the literature. At this point, I would like to thank Alexandre DuretLutz 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.
