Modal Automata: Analysing Modal Fixpoint Logics, One Step at a Time

There is a long tradition in theoretical computer science connecting the research fields of automata theory and logic. This link becomes particularly strong when automata are used to classify (possibly) infinite objects like streams, trees or graphs. Interestingly, this research area has provided not only fundamental theoretical results, such as Rabin’s decidability theorem, but also quite concrete applications in computer science, such as tools for the automatic verification of reactive systems.

Building on this tradition, and in particular on the work by Janin & Walukiewicz [8, 9] and D’Agostino & Hollenberg [3] on the modal $\mu$-calculus, we present and investigate a general framework for studying modal fixpoint logics, and some versions of monadic second-order logic, by means of certain finite automata that operate on Kripke structures.

Characteristic of the modal automata that we are about to introduce is that the co-domain of their transition function is a set of formulas in a simple formalism that we call a one-step logic. The concept of a one-step logic was developed by several authors, including Cîrstea, Pattinson and Schröder, in the setting of coalgebraic modal logic.

In addition to the monotonicity requirement, we impose some natural coherence conditions on one-step logics; for instance, we require that $𝙻(A)\subseteq 𝙻(B)$ if $A\subseteq B$, that the truth relation is invariant under isomorphism, etc. We will usually blur the distinction between one-step logics and one-step languages, since the semantics of one-step formulas is generally fixed.

We will use the term “modal automaton” as a generic name for $𝙻$-automata for some one-step logic $𝙻$. The operational semantics of these automata is given in terms of parity games.

Explained in words, the acceptance game $𝒜(𝔸,𝕊)$ proceeds in rounds, each round moving from one basic position $(a,s)\in A\times S$ to the next. At such a basic position, it is $\exists$’s task to turn the set $R(s)$ of successors of $s$ into the domain of a one-step model for the formula $\mathrm{\Theta }(a,\kappa (s))\in 𝙻(A)$. That is, she needs to come up with a marking $m:R[s]\to \mathrm{\wp }(A)$ such that $(R[s],m){⊩}_1\mathrm{\Theta }(a,\kappa (s))$ (and if she cannot find such a valuation, she looses immediately). One may think of the set $\{(b,t)\mid b\in m(t)\}$ as a collection of witnesses to her claim that, indeed, the one-step formula $\mathrm{\Theta }(a,\kappa (s))$ is true of $(R[s],m)$. The round ends with $\forall$ picking one of these witnesses, which then becomes the basic position at the start of the next round. (Unless, of course, $\exists$ managed to satisfy the formula $\mathrm{\Theta }(a,\kappa (s))$ with the empty set of witnesses, in which case $\forall$ gets stuck and looses immediately.)

If $\exists$ and $\forall$ play the acceptance game $𝒜(𝔸,𝕊)$ and neither of them gets stuck, the resulting match $\pi$ will take infinitely long. In this case we use the parity condition to assign a winner to $\pi$: we consider the set $\mathrm{𝖨𝗇𝖿}(\pi )$ of states that occur infinitely often in $\pi$, and declare $\exists$ to be the winner of $\pi$ if the maximal priority of the states in $\mathrm{𝖨𝗇𝖿}(\pi )$ is even, and $\forall$ if this maximum priority is odd.

We say that a logic is characterised by a class of modal automata if for every formula of the logic we can find an equivalent automaton n the class, and vice versa. Some well-known logics are of this kind.

The motivation for studying logics from the perspective of modal automata is that much of their sometimes complex behaviour is already determined at the far simpler one-step level. This means that, in order to establish some property of a class of modal automata – or of the logic it characterises – it may suffice to prove a similar result for the one-step logic(s) underlying the automata. Here are some examples, where $𝙻$ and ${𝙻}^{\prime }$ represent arbitrary one-step logics.

Closure properties of recognisable queries

If $𝙻$ is closed under taking, respectively, disjunctions, conjunctions and boolean duals, then the class of $\mathrm{𝖠𝗎𝗍}(𝙻)$-recognizable queries is closed under taking union, intersection, and complementation.

Bisimulation invariance

We say that a one-step formula $\varphi$ is invariant under quotients if we have $(D,m){⊩}_1\varphi$ iff $(D^{\prime },m^{\prime }){⊩}_1\varphi$, whenever $(D^{\prime },m^{\prime })$ is a quotient of $(D,m)$.

If $𝙻$ is the quotient-invariant fragment of ${𝙻}^{\prime }$ (in some strong sense), then $\mathrm{𝖠𝗎𝗍}(𝙻)$ is the bisimulation-invariant fragment of $\mathrm{𝖠𝗎𝗍}({𝙻}^{\prime })$. This result lies at the heart of the proof of the Janin-Walukiewicz Theorem, which identifies the modal $\mu$-calculus as the bisimulation-invariant fragment of monadic second-order logic.

Nondeterminism

Modal automata are generally alternating in nature, but there is a natural notion of nondeterminism as well: we call a modal automaton $𝔸$ nondeterministic if in any of its acceptance games, the role of $\forall$ is essentially reducible to that of a pathfinder. At the level of one-step logic, we introduce the notion of a disjunctive formula; roughly the idea is that if a disjunctive formula holds of some model then we can also satisfy it in a related model where the marking assigns to each element of the domain either the empty set or some singleton. It is easy to see that a modal automaton $𝔸=(A,\mathrm{\Theta },\mathrm{\Omega },a_I)$ is nondeterministic if the codomain of $\mathrm{\Theta }$ consists of disjunctive formulas.

Disjunctive bases and simulation

Assume that ${𝙻}^{\prime }\subseteq 𝙻$ and that ${𝙻}^{\prime }$ consists of disjunctive formulas and is closed under disjunctions. If $𝙻$ and ${𝙻}^{\prime }$ satisfy some natural distributive laws we call $𝙻$ a disjunctive basis for $𝙻$.

If $𝙻$ has a disjunctive basis ${𝙻}^{\prime }$ then every (alternating) $𝙻$–automaton can be simulated by an equivalent (nondeterministic) ${𝙻}^{\prime }$-automaton. Furthermore, the fixpoint logic characterised by $𝙻$ has several nice properties, such as the finite model property and uniform interpolation. This is how D’Agostino and Hollenberg established this property for the modal $\mu$-calculus.