# Capturing Bisimulation-Invariant Complexity Classes with Higher-Order Modal Fixpoint Logic

Martin Lange, Etienne Lozes

<figure><img src="image_1.png" /></figure>

## To cite this version:

Martin Lange, Etienne Lozes. Capturing Bisimulation-Invariant Complexity Classes with Higher-Order Modal Fixpoint Logic. 8th IFIP International Conference on Theoretical Computer Science (TCS), Sep 2014, Rome, Italy. pp.90-103, 10.1007/978-3-662-44602-7_8. hal-01402031

HAL Id: hal-01402031

https://inria.hal.science/hal-01402031

Submitted on 24 Nov 2016

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Capturing Bisimulation-Invariant Complexity
Classes with Higher-Order Modal Fixpoint Logic

Martin Lange and Etienne Lozes

School of Electrical Engineering and Computer Science
University of Kassel, Germany*

**Abstract.** Polyadic Higher-Order Fixpoint Logic (PHFL) is a modal fixpoint logic obtained as the merger of Higher-Order Fixpoint Logic (HFL) and the Polyadic $\mu$-Calculus. Polyadicity enables formulas to make assertions about tuples of states rather than states only. Like HFL, PHFL has the ability to formalise properties using higher-order functions. We consider PHFL in the setting of descriptive complexity theory: its fragment using no functions of higher-order is exactly the Polyadic $\mu$-Calculus, and it is known from Otto's Theorem that it captures the bisimulation-invariant fragment of PTIME. We extend this and give capturing results for the bisimulation-invariant fragments of EXP-TIME, PSPACE, and NLOGSPACE.

## 1 Introduction

**Higher-Order Fixpoint Logic.** Higher-Order Fixpoint Logic (HFL) [1] is a modal logic obtained by combining the modal $\mu$-calculus [2] and the simply typed $\lambda$-calculus. The modal $\mu$-calculus is found in HFL as formulas only using the base type, and consequently they denote predicates over the states of a transition system. HFL formulas of higher types which are formed using $\lambda$-abstraction for example denote predicate transformers, predicate transformer transformers and so on which can be defined recursively by means of least and greatest fixpoints.

It is known that model-checking formulas with recursive predicate transformers of order at most *k* is *k*-EXPTIME complete [3]. On the other hand, its expressiveness is poorly understood and natural questions like a capturing automaton model, a capturing game semantics, the existence of an alternation hierarchy, or the role of fixpoints in a guarded fragment have not been addressed sufficiently yet. This work provides a first step towards the understanding of the expressiveness of higher-order recursive definitions in terms of descriptive complexity.

**Descriptive (Bisimulation-Invariant) Complexity.** Descriptive complexity studies characterisations of classes of decision problems through means of formal

<footnote>* The European Research Council has provided financial support under the European Community's Seventh Framework Programme (FP7/2007-2013) / ERC grant agreement no 259267.</footnote>
descriptions of such problems, for instance through logical formulas. A logic defines a class of decision problems, namely the membership problem for the class of models of each of the logic's formulas.

One of the main aims of descriptive complexity theory is to provide characterisations of complexity classes in terms of logics, for instance Fagin's Theorem [4] stating that NP consists of *exactly* those problems which can be described by a formula of existential Second-Order Logic (∃SO). Thus, ∃SO captures NP.

The benefit of such capturing results are the characterisations of complexity classes without reference to a particular machine model or typical ressource bounds in terms of time and space consumption.

Many characterisations of known complexity classes in terms of logics have been found since: Second-Order Logic (SO) captures the polynomial time hierarchy PH [5], PSPACE is captured by SO enriched with a transitive closure operator [6] or, equivalently, First-Order Logic with an operator to define partial fixpoints [7], and so on. P has yet to be captured by a logic; it is known, though, that First-Order Logic with a least fixpoint operator captures P over the class of totally ordered structures [8, 9]. For a more detailed picture of results known in the area of descriptive complexity theory we refer to the respective literature [10, 11].

Another interesting result in a similar style is Otto's Theorem [12] about the polyadic µ-calculus [12, 13]. The polyadic µ-calculus is a variant of the (monadic) µ-calculus where formulas denote predicates of any arity as opposed to just monadic ones. The polyadic µ-calculus, like the monadic one, cannot distinguish between bisimilar structures; thus, it can only define bisimulation-invariant graph problems [14, 15]. Moreover, model-checking algorithms for the polyadic µ-calculus are slightly similar to the ones for the monadic µ-calculus, and in particular all problems expressed in the modal µ-calculus can be decided in P. Otto's Theorem states the converse of these: if a problem *p* is in the class P/∼ of problems that are both bisimulation-invariant and decidable in P, then *p* can be expressed by a formula of the polyadic modal µ-calculus. In other words, the polyadic modal µ-calculus captures P/∼.

**Contributions.** Here we address the question of the expressiveness of higher-order fixpoints in HFL by extending Otto's Theorem to higher orders. We define PHFL, the polyadic version of HFL and we turn our attention to the first-order fragment PHFL(1) of PHFL. Here, the term *order* refers to the typing order of functions used in the formulas. Thus, the fragment PHFL(0) of order 0 contains no proper functions, and it is equal to the polyadic *µ*-calculus. Note that there is a difference with the term *order* used in predicate logics: the polyadic *µ*-calculus is in fact a fragment of second-*order* predicate logic. The two interpretations of the term *order* are closely related: the fragment of formulas with functions of typing order at most *k* can be seen as a fragment of order (*k* + 2) predicate logic. We simply prefer to use the typing order for the indexing of fragments because then the lowest fragment is PHFL(0) instead of PHFL(2).
Our first contribution is to show that PHFL(1) captures the complexity class EXPTIME/∼. We then turn our attention to tail-recursive functions. It is well-known that such functions are usually more space efficient than arbitrary recursive functions. Our second contribution is to give a formal account of this fact: we show that the fragment PHFL(1, tail) of order-1 tail-recursive functions captures PSPACE/∼. We also develop the idea of tail-recursiveness for the polyadic μ-calculus, i.e. the fragment without proper functions, and obtain a fragment PHFL(0, tail) that captures NLOGSPACE/∼ on structures equipped with a pre-order which induces a total order on the equivalence classes w.r.t. bisimilarity. This pre-order is to NLOGSPACE/∼ and PHFL(0, tail) what a total order is to P and FO[LFP]: it enables the definition of iterations via fixpoint operators. Interestingly, the cut-off point marking the apparent need for such an order in the bisimulation-invariant complexity hierarchy lies below that in the non-bisimulation-invariant world, namely between NLOGSPACE/∼ and P/∼ rather than between P and NP.

**Related Work.** While this paper has taken the approach of characterising complexity classes by typing and syntactic restrictions, descriptive complexity theory predominantly has characterised complexity classes in terms of fixpoint combiners (like TC, LFP, or PFP), with the notable exception of characterisations based on Horn and Krom clauses [16].

In a different setting, higher-order grammars have been a topic intensively studied in the 80s that has recently revived in the context of verification of higher-order programs. A problem still open is whether languages defined by such grammars are context sensitive, or in other words if they belong to the complexity class NLINSPACE (non-deterministic linear space). Recent progresses on this problem have been achieved by Kobayashi et al [17], who showed that this is at least the case up to order 2 for tree languages and order 3 for word languages. Beside the fact that this line of research does not target a capturing result, the most significant difference with our work is that we consider a polyadic μ-calculus, or in different words, an automaton model that uses multiple tapes, whereas collapsible pushdown automata (the automaton model for higher-order grammars) only work with one tape.

Implicit complexity is another line of research that aims at ensuring the complexity of the execution of higher-order programs through typing. Our work here is not concerned with the time complexity of performing β-reductions or the space needed to represent the reduced terms but in the complexity of the queries defined by the formulas we consider (which are invariant under β-reduction).

**Outline.** In section 2 we recall Otto's Theorem that states that the polyadic μ-calculus captures P/∼. In section 3, we introduce the higher-order polyadic μ-calculus. Section 4 establishes that order 1 captures EXPTIME/∼. Section 5 studies the tail-recursive fragment and establishes that there, order 1 captures PSPACE/∼ and order 0 NLOGSPACE/∼. Due to space constraints, some details are missing and can be found in a longer version [18].
## 2 Background

**Labeled transition systems, bisimulation, and queries.** A labeled transition system (LTS) is a tuple $\mathfrak{M} = (Q, \Sigma, P, \Delta, v)$, where $Q = \{q, r, \dots\}$ is a set of states, $\Sigma = \{a, b, \dots\}$ is a finite set of actions, $P = \{p, \dots\}$ is a finite set of propositions, $\Delta \subseteq Q \times \Sigma \times Q$ is the set of labeled transitions, and $v: P \to 2^Q$ is a valuation that associates to every proposition a set of states. We write $q_1 \xrightarrow{a} q_2$ for $(q_1, a, q_2) \in \Delta$ and $q \models p$ for $q \in v(p)$.

A binary relation $R \subseteq Q^2$ is a bisimulation if it is a symmetric relation, and for every pair of states $(q_1, q_2) \in R$, it holds that (1) for all $a \in \Sigma$, for all $q'_1 \in Q$, if $q_1 \xrightarrow{a} q'_1$, then there is $q'_2 \in Q$ such that $q_2 \xrightarrow{a} q'_2$ and $q'_1 R q'_2$, and (2) for all $p \in P$, if $q_1 \models p$, then $q_2 \models p$. Two states $q_1, q_2$ are *bisimilar*, written $q_1 \sim q_2$, if there is a bisimulation that contains the pair $(q_1, q_2)$.

We assume a fixed encoding of a finite LTS $\mathfrak{M} = (Q, \Sigma, P, \Delta, v)$ as a word $w_{\mathfrak{M}}$ such that $|w_{\mathfrak{M}}|$ is linear in $|Q| \cdot |P| + |\Delta|$ (for instance, using a sparse matrix representation). An $r$-adic query $Q$ is a set of tuples $(\mathfrak{M}, q_1, \dots, q_r)$ where $\mathfrak{M}$ is an LTS and $q_1, \dots, q_r$ are states of $\mathfrak{M}$. A query $Q$ is said to belong to a complexity class $C$ if the language of encodings of $Q$ is in $C$. A query $Q$ is said to be bisimulation-invariant if for every two tuples $(\mathfrak{M}, q)$ and $(\mathfrak{M}', q')$ such that $q_i \sim q'_i$ for all $i$, $(\mathfrak{M}, q) \in Q$ if and only if $(\mathfrak{M}', q') \in Q$.

**Example 1.** Let $Q$ be the binary query consisting of tuples $(\mathfrak{M}, q, q')$ such that $q \sim q'$. Since bisimilarity can be decided in $P$, this query is in $P$. Moreover, since bisimilarity is a transitive relation, this query is bisimulation-invariant.

**The polyadic $\mu$-calculus.** A formula of the (monadic) modal $\mu$-calculus is often interpreted as a game played by two players (sometimes called Prover and Refuter) that alternatively move a single pebble along the transitions of an LTS. The polyadic $\mu$-calculus is basically a multi-pebble version of this game: $d \ge 1$ pebbles are disposed on the states of a LTS, and for every modality $\langle a \rangle_i$ (respectively $[a]_i$), Prover (respectively Refuter) has to move the $i$-th pebble along an $a$-transition. Moreover, formulas can use the modality $\{i \leftarrow j\}$, that corresponds, in the game interpretation, to moving the $i$-th pebble to the same place as the $j$-th pebble.

Let $\mathbf{Var} = \{X, Y, Z, \dots\}$ be some fixed set of variables. Formulas of the polyadic $\mu$-calculus $\mathcal{L}_{\mu}^{\omega}$ are given by the following grammar

$$ \Phi, \Psi ::= \top \mid p_i \mid \Phi \lor \Psi \mid \neg \Phi \mid \langle a \rangle_i \Phi \mid \{i \leftarrow j\} \Phi \mid X \mid \mu X. \Phi $$

where $i = (i_1, \dots, i_n)$ and $j = (j_1, \dots, j_n)$ are equal-length tuples of natural numbers. As usual, we only consider formulas in which every bound variable occurs underneath an even number of negations counting from its $\mu$-binder. We also use standard notations for derived logical connectives, namely $\wedge$, $\Rightarrow$, $\Leftarrow$, and $[a]_i$ for conjunction, implication, equivalence, and necessity respectively. A formula is $d$-adic if in each subformula $p_i$, $\langle a \rangle_j \Phi$, and $\{i \leftarrow j\} \Phi$ the indices $i, j, i_1, \dots, i_n, j_1, \dots, j_n$ are in $\{1, \dots, d\}$.
The semantics of a *d*-adic formula $\Phi$ is a set $\llbracket \Phi \rrbracket_{\mathfrak{M}}^d$ of *d*-tuples of states (see [12], and also Section 3). The *r*-adic query $Q_{\Phi}^r$ associated to a closed *d*-adic formula $\Phi$ is the set of tuples $(\mathfrak{M}, q_1, \dots, q_r)$ such that there is $s \in \llbracket \Phi \rrbracket_{\mathfrak{M}}^d$ with $q_i = s_i$ for all $i = 1, \dots, \min(r, d)$.

**Example 2.** A standard example of a 2-adic formula is $\Phi_{\sim} =$

$$ \nu X. \bigwedge_{a \in \Sigma} [a]_1 \langle a \rangle_2 X \wedge [a]_2 \langle a \rangle_1 X \wedge \bigwedge_{p \in P} p_1 \Leftrightarrow p_2 $$

which denotes the set of pairs $(q_1, q_2)$ such that $q_1 \sim q_2$. Thus, $\Phi_{\sim}$ defines bisimilarity [12, 13], and $Q_{\Phi}^2$ is the same query as in Example 1.

**Theorem 1 (Otto [12]).** Let $\mathcal{Q}$ be an $r$-adic query. The following two are equivalent. (1) $\mathcal{Q}$ is bisimulation-invariant and in $\mathbb{P}$; (2) $\mathcal{Q} = Q_{\Phi}^r$ for some $\Phi \in \mathcal{L}_{\mu}^{\omega}$.

As a consequence of Otto's Theorem, we get for example that trace equivalence is not expressible in the polyadic modal $\mu$-calculus (unless $\mathbb{P} = \text{PSPACE}$), because of the PSPACE-completeness of trace equivalence [19].

### 3 A Polyadic Higher-Order Fixpoint Logic

In this section, we introduce the polyadic higher-order fixpoint logic, a logic that extends the polyadic modal $\mu$-calculus with higher-order fixpoints à la Viswanathan and Viswanathan [1]. In Viswanathans' logic, order-0 formulas denote predicates, order-1 formulas denote predicate transformers, i.e. functions mapping predicates to predicates, and so on for higher orders. For instance, $(\lambda F. \lambda X. F(FX)) (\lambda Y. \langle a \rangle Y) \top$ is equivalent to the formula $\langle a \rangle \langle a \rangle \top$. Moreover, the least fixpoint combinator can be applied to monotone predicate transformers of any order. For instance, the formula

$$ (\mu G. \lambda F. \lambda X. (FX) \lor (G (\lambda Z. F(FZ)) X)) (\lambda Y. \langle a \rangle Y) \top $$

is equivalent to the infinitary disjunction $\bigvee_{n \ge 0} \langle a \rangle^{2^n} \top$.

Formally, formulas $\Phi, \Psi, \dots$, types $\tau, \sigma, \dots$ and variances $v$ of the polyadic higher-order fixpoint logic $(\text{PHFL}(\omega))$ are defined by the grammar

$$ v ::= + \mid - \mid 0 \quad \sigma, \tau ::= \bullet \mid \sigma^v \rightarrow \tau \\ \Phi, \Psi ::= \top \mid p_i \mid \Phi \lor \Psi \mid \neg \Phi \mid \langle a \rangle_i \Phi \mid \{i \leftarrow j\} \Phi \mid X \mid \lambda X^{v, \tau} \Phi \mid \Phi \Psi \mid \mu X^{\tau} \Phi $$

where $X, Y, \dots$ range over a finite set of variables, and $i, j$ range over the set $\mathbb{N}$ of natural numbers. We use standard notations like $\Phi \wedge \Psi$, $[a]_i \Phi$, $\nu X^{\tau} \Phi$, or $\Phi \Leftrightarrow \Psi$ for dual and derived connectives. The maximal arity $\text{ma}(\tau)$ of a type $\tau$ is defined by induction on $\tau$: $\text{ma}(\bullet) = 1$, and $\text{ma}(\tau_1 \rightarrow \tau_2 \rightarrow \dots \rightarrow \tau_n \rightarrow \bullet) = \max(\{n\} \cup \{\text{ma}(\tau_i) \mid i = 1, \dots, n\})$. The order $\text{ord}(\tau)$ of a type $\tau$ is defined by induction on $\tau$: $\text{ord}(\bullet) = 0$, and $\text{ord}(\sigma \rightarrow \tau) = \max(1 + \text{ord}(\sigma), \text{ord}(\tau))$. The order
<figure><img src="image_3.png" /><figcaption>**Fig. 1.** The type system of PHFL(ω). The type environment $\neg\Gamma$ is the one in which every assumption $X^v : \tau$ is replaced with $X^{-v} : \tau$</figcaption></figure>

of a formula $\Phi$ is $\max\{\text{ord}(\tau) \mid \mu X^\tau.\Psi$ is a subformula of $\Phi\}$. We write PHFL($k$) for the set of formulas where recursive predicates are annotated with types of order at most $k$. In particular, PHFL(0) is the polyadic modal $\mu$-calculus $\mathcal{L}_\mu^\omega$. On the other hand, the 1-adic fragment of PHFL(ω) is exactly Viswanathans' Higher-Order Modal Fixpoint Logic.

Given a set $A$ and a boolean algebra $B$, the set of functions $f: A \to B$ is again a boolean algebra (for instance, $(\neg_{A \to B} f)(x) = \neg_B(f(x)))$. A function $f: A \to B$ has variance + if it is monotone, — if $\neg_{A \to B} f$ is monotone, and 0 in any case. We associate to every type $\tau$ the boolean algebra $D_\tau$ as follows: (1) $D_\bullet$ is the set $\mathcal{P}(Q^d)$ of all $d$-adic predicates, and (2) if $\tau = \sigma^v \to \sigma'$, then $D_\tau$ is the set of functions $f: D_\sigma \to D_{\sigma'}$ that have variance $v$.

A term $\lambda X^{v,\tau}. \Phi$ denotes a function that expects an argument of type $\tau$ and has variance $v$ in this argument. A type judgement is a judgement of the form $X_1^{v_1, \tau_1}, \dots, X_n^{v_n, \tau_n} \vdash \Phi : \tau$. We say that a type judgement is derivable if it admits a derivation tree according to the rules of Figure 1.

A formula $\Phi$ is well-typed if $\vdash \Phi : \tau$ is derivable for some $\tau$. In the remainder, we always implicitly assume that we are working with well-typed formulas and sometimes omit the type annotations.

The semantics of a well-typed formula $\Phi$ of type $\tau$ is a predicate or function living in $D_\tau$ that we are now about to define. The interpretation $\llbracket \Gamma \rrbracket$ of a type environment is the set of maps $\rho$ that send each variable $X^v : \tau \in \Gamma$ to $\rho(X) \in D_\tau$. We write $\rho[X \mapsto \mathcal{X}]$ for the map $\rho'$ that is equal to $\rho$ except for $\rho'(X) = \mathcal{X}$. The interpretation $\llbracket \Gamma \vdash \Phi : \tau \rrbracket$ is a map from $\llbracket \Gamma \rrbracket$ to $D_\tau$ defined by induction on $\Phi$ as explained of Figure 2 (remember that $D_\bullet = \mathcal{P}(Q^d)$ is the set of all $d$-adic predicates).

**Proposition 1.** For every formula $\Phi$ of ground type, for all $d \ge 1$, the query $Q_\Phi^d$ is bisimulation-invariant.
$$
\begin{align*}
& [\Gamma \vdash \top : \bullet](\rho) = Q^d \\
& [\Gamma \vdash \langle a \rangle_i \Phi : \bullet](\rho) = \{q \in Q^d \mid \exists q' \in [\Gamma \vdash \Phi : \bullet]. q \xrightarrow{a,i} q'\} \\
& [\Gamma \vdash \Phi \lor \Psi : \tau](\rho) = [\Gamma \vdash \Phi : \tau](\rho) \sqcup_{\tau} [\Gamma \vdash \Psi : \tau](\rho) \\
& [\Gamma \vdash \neg \Phi : \tau](\rho) = \neg_{\tau} [\neg(\Gamma) \vdash \Phi : \tau](\rho) \\
& [\Gamma \vdash \{i \leftarrow j\} \Phi : \bullet](\rho) = \{i \leftarrow j\}(q) \mid q \in [\Gamma \vdash \Phi : \bullet](\rho) \\
& [\Gamma, X : \tau \vdash X : \tau](\rho) = \rho(X) \\
& [\Gamma \vdash \mu X^{\tau} \Phi](\rho) = \text{LFP} [\Gamma \vdash \lambda X^{+, \tau} \Phi](\rho) \\
& [\Gamma \vdash \lambda X^{v, \sigma} \Phi : \sigma^v \to \tau](\rho) = \mathcal{X} \mapsto [\Gamma, X^v : \sigma \vdash \Phi : \tau](\rho[X \mapsto \mathcal{X}]) \\
& [\Gamma \vdash \Phi \Psi : \tau](\rho) = [\Gamma \vdash \Phi : \sigma^v \to \tau](\rho)([\Gamma \vdash \Psi : \sigma](\rho))
\end{align*}
$$

where $\boldsymbol{q} \xrightarrow{a,i} \boldsymbol{q}'$ stands for $q_i \xrightarrow{a} q'_i$ and $q_j = q'_j$ for all $j \neq i$.

<caption>Fig. 2. Semantics of PHFL($\omega$).</caption>

Proposition 1 can be proved for instance by extending Viswanathans’ proof of the bisimulation-invariance of Higher-Order Fixpoint Logic [1] to polyadic formulas. Furthermore, using fixpoint unfolding and $\beta$-reduction it is also possible to see that over every set of structures, PHFL($\omega$) is equivalent to infinitary polyadic modal logic, i.e. one with arbitrary disjuncts and conjuncts and no fixpoint quantifiers, no $\lambda$-abstraction and no formula application.

**Example 3.** Let $\Phi := (\nu F.\lambda X, Y.X \Leftrightarrow Y \wedge \bigwedge_{a \in \Sigma} F \langle a \rangle_1 X \langle a \rangle_2 Y) \top \top$. Then $\Phi$ can be unfolded to

$$
\begin{align*}
F \top \top &= \top \Leftrightarrow \top \wedge \bigwedge_{a \in \Sigma} F \langle a \rangle_1 \top \langle a \rangle_2 \top \\
&= \bigwedge_{a \in \Sigma} \langle a \rangle_1 \top \Leftrightarrow \langle a \rangle_2 \top \wedge \bigwedge_{b \in \Sigma} F \langle ba \rangle_1 \top \langle ba \rangle_2 \top \\
&= \bigwedge_{w \in \Sigma^*} \langle w \rangle_1 \top \Leftrightarrow \langle w \rangle_2 \top,
\end{align*}
$$

where $\langle w \rangle_i$ stands for $\langle w_1 \rangle_i \langle w_2 \rangle_i \dots \langle w_n \rangle_i$. Thus, $\Phi$ denotes those pairs $(q_1, q_2)$ for which $q_1$ and $q_2$ have exactly the same traces, i.e $\Phi$ defines trace equivalence.

# 4 Capturing EXPTIME/∼

The aim of this section is to show that the first-order fragment of PHFL, i.e. PHFL(1) captures the class of bisimulation-invariant queries which can be evaluated in deterministic exponential time. For one part of this result we show the stronger statement that queries of order $k$ can be evaluated in $k$-fold exponential time.

**Theorem 2.** Let $r, k \ge 1$, and $\Phi \in \text{PHFL}(k)$. Then the query $Q_{\Phi}^r$ is in $k$-EXPTIME.

The proof essentially follows the same ideas as in the case of the (1-adic) Higher-Order Fixpoint Logic [3] (see [18] for details).

Theorem 2 shows in particular that all queries expressible in PHFL(1) are in EXPTIME/∼. We now consider the converse implication and aim at a proof of
the following: if a query is in EXPTIME/~, then it can be expressed by a PHFL(1) formula. A direct, but tedious proof would encode the run of an EXPTIME Turing machine by a query. A more elegant proof can be obtained by making use of Immerman's characterisation of EXPTIME queries over structures [6] as those that are expressible in second-order logic with least fixed points (SO[LFP]). The proof then proceeds in two steps: first, we transfer Immerman's result to the logic SO[LFP]/~ defined over labeled transition systems, and second we show how to encode SO[LFP]/~ into PHFL(1).

The first step is relatively easy with the main problem simply being a correct definition of the semantics of SO[LFP]/~ over LTS. We define the formulas of SO[LFP] (resp. SO[LFP]/~) as the ones derivable from the grammar

$$ \Phi, \Psi ::= p(x) \mid a(x, y) \mid \Phi \lor \Psi \mid -\Phi \mid \exists x. \Psi \mid \\ \phantom{\Phi, \Psi ::=} \exists X. \Psi \mid \text{LFP}(F, X, \Phi)(Y)(x) \mid X(x) \mid F(X)(x) $$

The semantics of SO[LFP] on labeled graphs is as expected (see for instance [6]). Now, in order to define the semantics of SO[LFP]/~ over LTS, we just need to map every LTS to a labeled graph and interpret the formula over this graph with the SO[LFP] semantics.

We call a tuple $(\mathfrak{M}, q_1, \dots, q_r)$ reduced if all states of $\mathfrak{M}$ are reachable from at least one $q_i$, and if $\sim$ coincides with equality. To every tuple $(\mathfrak{M}, q)$, we associate the reduced tuple $\text{RED}(\mathfrak{M}, q)$ obtained by quotienting with respect to $\sim$ and pruning all states that cannot be reached from at least one $q_i$. We say that a tuple $(\mathfrak{M}, q)$ satisfies a formula $\Phi$ of SO[LFP]/~ if the graph $\text{RED}(\mathfrak{M}, q)$ satisfies $\Phi$ in the graph semantics.

**Lemma 1.** A query $Q$ is in EXPTIME/~ iff it is definable in SO[LFP]/~.

We refer to [18] for a detailed proof of this result, and now move to the more challenging part, namely the encoding of SO[LFP]/~ into PHFL(1). For every SO[LFP]/~ formula $\Phi$ with free second-order variables $X_1, \dots, X_n$, we define a PHFL(1) formula $\Psi$ with the same free (order 0) variables, so that the least fixpoint in SO[LFP]/~ is naturally represented by a least fixpoint in PHFL(1). First-order variables of SO[LFP]/~ are encoded differently. Without loss of generality, we may assume an enumeration $x_1, \dots, x_r, x_{r+1}, \dots, x_d$ of all variables of the SO[LFP] formula, such that $x_1, \dots, x_r$ are the free variables and $x_{r+1}, \dots, x_d$ are the quantified ones. We thus code $p(x_i)$ and $a(x_i, x_j)$ as $p_i$ and $\langle a \rangle_i \{1, 2 \leftarrow i, j\} \Phi$ respectively, where $\Phi$ is the formula that defines $\sim$. For $i > r$, we define the macro $\exists_i \Phi := \bigvee_{j=1}^r \{i \leftarrow j\} \mu X. \Phi \lor \bigvee_{a \in \Sigma} \langle a \rangle_i X$, where $\Phi$ is an arbitrary PHFL(1) formula in which $X$ does not occur. Then $\exists_i \Phi$ defines the set of all tuples for which $\Phi$ holds once the $i$-th component has been replaced by some state reachable from one of the states denoted by $x_1, \dots, x_r$. Due to the bisimulation-invariant semantics of SO[LFP]/~, this is enough to encode a first-order quantification.

We are thus left with the encoding of second-order quantifiers. There is no obvious way of adapting the same idea we used for first-order quantifiers, and our encoding of second-order quantifiers is significantly trickier.
Let us first recall that it is possible to define a 2-adic formula $\Phi_<$ that defines a transitive relation $<$ such that $< \cap > = \emptyset$ and $< \cup > = \aleph$; we refer to Otto's work [12] where this formula is the crux of the proof that the polyadic $\mu$-calculus captures $P/_{\sim}$. Let $\mathfrak{M}$ be a reduced LTS, so that $<$ defines a total order on states, and let $<_{lex}$ denote the lexicographic extension of $<$ over $Q^d$.

**Lemma 2.** There is a predicate transformer $\langle dec \rangle$ such that for every formula $\Phi$, $\langle dec \rangle \Phi$ denotes the upward closure of $\Phi$ with respect to $<_{lex}$.

The construction of $\langle dec \rangle$ is rather straightforward (see [18]).

**Lemma 3.** Consider the predicate transformer

$$ \text{next} := \lambda X. (\neg X \wedge \neg \langle dec \rangle \neg X) \vee (X \wedge \langle dec \rangle \neg X). $$

Then, for any predicate $\mathcal{X} \in \mathcal{P}(Q^d)$, there is $i \ge 0$ such that $\text{next}^i(\emptyset) = \mathcal{X}$.

*Proof.* Consider the bijection $f: \mathcal{P}(Q^d) \to \{0, \dots, 2^{|Q|^d} - 1\}$ defined by associating to every predicate $\mathcal{X} \in \mathcal{P}(Q^d)$ the integer $f(\mathcal{X})$ whose binary representation $b_1 b_2 \dots b_{|Q|^d}$ is such that the $i$th bit $b_i$ is equal to 1 if and only if the $i$-th element $q$ of $Q^d$ with respect to $<_{lex}$ is in $\mathcal{X}$.

Our claim is that next maps every predicate $\mathcal{X}$ to the predicate $\mathcal{Y}$ such that $f(\mathcal{Y}) = 1 + f(\mathcal{X})$ modulo $2^{|Q|^d}$. Indeed, the $i$th bit in $\mathcal{Y}$ is 1 if either it is also 1 in $\mathcal{X}$ and a lower bit is 0 in $\mathcal{X}$, or it is 0 in $\mathcal{X}$ but all lower bits are 1 in $\mathcal{X}$. $\square$

Let $\Phi$ be a PHFL(1) formula not containing the variable $H$, and let formula $\exists X. \Phi$ be defined as $(\mu H. \lambda X. \Phi \vee H (\text{next } X)) \perp$. Then, thanks to Lemma 3, $\exists X. \Phi$ encodes a second-order existential quantification.

**Lemma 4.** Let $r \ge 1$. For every formula $\Phi$ of $\text{SO}[\text{LFP}]/_{\sim}$, there is a formula $\Psi$ of PHFL(1) such that $Q_{\Phi}^r = Q_{\Psi}^r$.

**Theorem 3.** PHFL(1) captures $\text{EXPTIME}/_{\sim}$ over labeled transition systems.

*Proof.* Lemmas 1 and 4 prove that every $\text{EXPTIME}/_{\sim}$ query is expressible in PHFL(1). By Theorem 2 and Proposition 1, we know that PHFL(1) cannot express more than that. $\square$

# 5 Tail Recursion and PSPACE/$_{\sim}$

Tail-recursive functions are functions that are never called recursively in intermediate steps of their body, either for evaluating a condition on branching, or for evaluating an argument of a function call. By analogy, we define tail-recursive formulas as the ones that can be seen as non-deterministic tail-recursive functions.

We assume from now on that the logical connective $\wedge$ is primitive in the syntax (and not just the dual of $\vee$). Without loss of generality, we restrict our attention to formulas in which every variable is bound at most once. We say
<figure><img src="image_4.png" /><figcaption>**Fig. 3.** A closed formula $\Phi$ is tail-recursive if $\emptyset \vdash \text{tail}(\Phi, \emptyset)$ is derivable.</figcaption></figure>

that a formula $\mu X.\Phi$ is a tail-recursive definition if no subformula of $\Phi$ is of the form either $\Phi' \Psi$, or $\neg\Psi$, or $\Psi \wedge \Phi'$, with $X$ occuring free in $\Psi$ (see Figure 3 for an inductive definition). Observe that we therefore do not treat both sides of a conjunction symmetrically. A formula is tail recursive if every recursive definition is tail-recursive. We write PHFL($i, \text{tail}$) for the set of tail-recursive formulas of PHFL($i$).

*Example 4.* The formula $(\mu F.\lambda X.(F \langle a \rangle_1 X) \vee (X \wedge \langle a \rangle_2(F X)))(\mu Y.Y)$ is tail-recursive. On the other hand, the formula $\mu X.[a]_1 X$ is not tail-recursive because $X$ occurs underneath $[a]_1$ (see Figure ??). The formula $\mu F.\lambda X.(F X) \wedge (F(FX))$ is not tail-recursive either, for two different reasons: on the one hand $F$ occurs on the left side of $\wedge$, and on the other hand $F$ occurs in the argument $FX$ of $F$.

**Theorem 4.** Let $r > 0$ and $\Phi \in \text{PHFL}(1, \text{tail})$. Then $Q_{\Phi}^r$ is in PSPACE.

*Proof.* The proof of this result is slightly more complicated than for Theorem 2. To achieve EXPTIME, a global model-checking algorithm that closely follows the semantics of PHFL(1) is enough. However, such an algorithm needs to represent functions denoted by predicate transformer in extension, which requires exponential space. If we want a model-checking algorithm running in PSPACE, we need to avoid representing functions in extension.

For a PHFL(1, tail) formula $\Phi$, let the recursion depth $\text{rd}(\Phi)$ of $\Phi$ be inductively defined as follows: $\text{rd}(p_i) = \text{rd}(X) = 0$, $\text{rd}(\Phi_1 \vee \Phi_2) = \max(\text{rd}(\Phi_1), \text{rd}(\Phi_2))$, $\text{rd}(\Phi_1 \wedge \Phi_2) = \max(\text{rd}(\Phi_2), 1 + \text{rd}(\Phi_1))$, $\text{rd}(\Phi_1 \wedge \Phi_2) = \max(\text{rd}(\Phi_1, 1 + \text{rd}(\Phi_2)))$, $\text{rd}(\langle a \rangle_i \Phi) = \text{rd}(\lambda X.\Phi) = \text{rd}(\mu X.\Phi) = \text{rd}(\Phi)$, and $\text{rd}(\neg\Phi) = 1 + \text{rd}(\Phi)$.

If $\pi$ is a list $\mathcal{X}_1, \dots, \mathcal{X}_n$ of elements of $\mathcal{P}(Q^d)$, we write $\text{hd}(\pi)$ for $\mathcal{X}_1$ and $\text{tl}(\pi)$ for $\mathcal{X}_2, \dots, \mathcal{X}_n$, and $\mathcal{X} :: \pi$ for the list $\pi'$ with $\text{hd}(\pi') = \mathcal{X}$ and $\text{tl}(\pi') = \pi$. For simplicity, we assume without loss of generality that we work with formulas such that every variable is bound at most once. We call a variable *recursive* if it is
bound by a $\mu$. For a function $c : \mathbf{Var} \to \mathbb{N}$ we write $c[X++]$ for the function defined by $c[X++](X) = 1 + c(X)$ and $c[X++](Y) = c(Y)$ for all $Y \neq X$.

For a tuple $\mathbf{q} \in Q^d$, a PHFL(1, tail) formula $\Phi$, a list $\pi \in \mathcal{P}(Q^d)^*$, a function $\rho : \mathbf{Var} \to \mathcal{P}(Q^d)$ and a function $c : \mathbf{Var} \to \mathbb{N}$, let **check**($\mathbf{q}, \Phi, \pi, \rho, c$) be the non-deterministic recursive procedure defined as follows:

- if $\Phi$ is an atomic formula, return **true** if $\mathbf{q} \in [\Phi](\rho)$, **false** otherwise;

- if $\Phi = \{i \leftarrow j\}\Psi$, return **check**($\{i \leftarrow j\}(\mathbf{q}), \Psi, \pi, \rho, c$);

- if $\Phi = X$ and $X$ is not a recursive variable, return **true** if $\mathbf{q} \in \rho(X)$, **false** otherwise;

- if $\Phi = X$ for a recursive variable $X$ with $\mathrm{fp}_X = \mu X^\tau . \Psi$, let $N := |Q|^d$ if $X$ is order 0, otherwise $X$ is a $l$-ary predicate transformer for some $l > 0$, and we set $N := |Q|^{ld} \cdot 2^{|Q|^d}$; if $c(X) = N$, return **false**, otherwise return **check**($\mathbf{q}, \Psi, \pi, \rho, c[X++]$);

- if $\Phi = \neg \Psi$, return $\neg \mathbf{check}(\mathbf{q}, \Psi, \pi, \rho, c)$;

- if $\Phi = \Phi_1 \lor \Phi_2$, guess $i \in \{1, 2\}$ and return **check**($\mathbf{q}, \Phi_i, \mathcal{X}, \pi, \rho, c$);

- if $\Phi = \langle a \rangle_i \Psi$, guess $s$ such that $\mathbf{q} \xrightarrow{a,i} s$ and return **check**($s, \Psi, \pi, \rho, c$);

- if $\Phi = \Psi_1 \Psi_2$, compute first the set of tuples $\mathcal{X} := \{r \mid \mathbf{check}(r, \Psi_2, \pi, \rho, c) = \text{true}\}$, then return **check**($\Psi_1, \mathcal{X} :: \pi, \rho, c$);

- if $\Phi = \Phi_1 \land \Phi_2$, return **false** if $\mathbf{check}(\mathbf{q}, \Phi_1, \pi, \rho, c) = \mathbf{false}$, otherwise return **check**($\mathbf{q}, \Phi_2, \pi, \rho, c$);

- if $\Phi = \lambda X . \Psi$, return **check**($\Psi, \mathrm{tl}(\pi), \rho[X \mapsto \mathrm{hd}(\pi)], c$);

- if $\Phi = \mu X^\tau . \Phi'$, return **check**($\mathbf{q}, \Phi', \pi, \rho, c[X \mapsto 0]$).

Consider a fixed $d$-adic formula $\Phi$ with $l$ variables and recursion depth $rd(\Phi) = k$, and an LTS $\mathfrak{M}$ with $n$ states. Encoding sets as bit vectors and integers in binary, $\rho$, $\pi$ and $c$ require $\mathcal{O}(n^{dl})$ space, whereas encoding $\mathbf{q}$ requires $\mathcal{O}(d \cdot \log n)$. Moreover, if we avoid to stack the calling context at every tail recursive call (recursive calls of the form **return check(...)**), then the height of the stack of calling contexts is bounded by the recursion depth $k$ of the formula. So **check**($\mathbf{q}, \Phi, \pi, \rho, c$) requires overall space $\mathcal{O}(k \cdot n^{dl})$. As a consequence, for a fixed parameter formula $\Phi$, the procedure works in NPSPACE, and by Savitch's theorem we get that $Q_{\Phi}^r$ is in PSPACE. $\square$

We are now interested in the proof of the converse of Theorem 4. In order to establish that PHFL(1, tail) captures PSPACE/~, we again pick a logic that captures PSPACE over graphs, transfer this result to transition systems, and encode this logic in PHFL(1, tail). The logic we consider is first-order logic with partial fixpoints (FO[PFP]) introduced by Abiteboul and Vianu [7]. The partial fixpoint PFP($f$) of a predicate transformer $f : \mathcal{P}(Q^d) \to \mathcal{P}(Q^d)$ is the predicate defined as follows: if there is some $i \ge 0$ for which $f^i(\emptyset) = f^{i+1}(\emptyset)$, then PFP($f$) := $f^i(\emptyset)$; otherwise PFP($f$) := $\emptyset$. We only detail the encoding of this partial fixpoint combinator in PHFL(1, tail), since the rest of the proof does not significantly differ from the proofs of Lemmas 1 and 4 (see [18] for details).

Let $\forall_i \Phi$ denote the formula $\neg \exists_i \neg \Phi$, where $\exists_i \Phi$ is the formula we introduced for encoding first-order quantifiers. For a PHFL(1, tail) formula $\Phi$ with a free variable $X$, let $\Psi := (\mu F . \lambda X . (X \land \forall_1 \dots \forall_d (X \leftrightarrow \Phi))) \lor F \Phi) \perp$. It can be checked
that $\Psi$ is tail-recursive and order 1, and that it defines the partial fixpoint of $\lambda X.\Phi$.

**Theorem 5.** PHFL(1, tail) captures PSPACE/$\sim$ over labeled transition systems.

Next we consider tail-recursive formulas of order 0. The same algorithm that we used in the proof of Theorem 4 has a better space complexity for formulas of PHFL(0).

**Theorem 6.** For all $r \ge 0$, for every formula $\Phi$ of PHFL(0, tail), $Q_{\Phi}^r$ is in NLOGSPACE.

*Proof.* Consider again the procedure **check**(q, $\Phi$, $\pi$, $\rho$, c) for local model-checking introduced in the proof of Theorem 4. When $\Phi$ is in PHFL(0, tail), all variables are recursive, so the parameters $\rho$ and $\pi$ are useless, and for every recursive variable $X$, the counter $c(X)$ remains smaller than $|Q|^d$, so $c$ can be represented in logarithmic space. Since $q$ can also be represented in logarithmic space, and the height of the stack of recursive calls is bounded by the constant $rd(\Phi)$, **check** is a non-deterministic logarithmic space procedure. $\square$

In order to capture NLOGSPACE/$\sim$, we consider the logic FO[TC] whose syntax is defined as follows

$$ \Phi ::= p(x_i) \mid a(x_i, x_j) \mid x_i < x_j \mid \Phi \lor \Psi \mid \neg \Phi \mid \exists x_i. \Phi \mid X(\bar{x}) \mid [\text{TC } \Phi](\boldsymbol{x}, \boldsymbol{y}). $$

A formula $\Phi$ of FO[TC] is d-adic if for every first-order variable $x_i$ occurring in $\Phi$ the index $i$ is smaller than $2d$. The semantics of a d-adic formula is then a binary relation $R \subseteq Q^{2d}$, with $[[\text{TC } \Phi]]$ being the reflexive transitive closure of $[[\Phi]]$. As before, let FO[TC]/$\sim$ be the syntactically same logic which is interpreted over reduced LTS only. Bisimulation is still definable in FO[TC] because of the preorder $<$. Since bisimulation $\sim$ is P-complete [21], FO[TC]/$\sim$ is very unlikely to capture NLOGSPACE/$\sim$ over all transition systems. The way to go around this problem is to assume that the preorder $<$ is given as part of the model.

We call totally ordered LTS a tuple $\mathfrak{M} = (Q, <, \Sigma, P, \Delta, v)$ where $<$ is a preorder over $Q$ such that $< \cup > = \prec$. Observe that for a totally ordered LTS $\mathfrak{M}$, $(\mathfrak{M}, q)$ is reduced if and only if $<$ is a total order, and all states are reachable from one of the $q$ root states, so the query containing all reduced $(\mathfrak{M}, q)$ is in NLOGSPACE over totally ordered LTS. Now, using the same arguments as in Lemma 1, we get that FO[TC]/$\sim$ captures NLOGSPACE/$\sim$ over totally ordered LTS.

We call PHFL(0, <, tail) the set of formulas $\Phi[\Phi_{<}/X]$ such that $\Phi$ is in PHFL(0, tail). It follows from Theorem 6 that all queries over totally ordered LTS that are definable in PHFL(0, <, tail) are in NLOGSPACE/$\sim$.

**Theorem 7.** PHFL(0, <, tail) captures NLOGSPACE/$\sim$ over totally ordered LTS.

*Proof.* We need to show that for every $r > 0$ and every formula $\Phi$ of FO[TC], there is a PHFL(0, <, tail) formula $\Psi$ such that $Q_{\Phi}^r = Q_{\Psi}^r$ over totally ordered
<figure><img src="image_5.png" /><figcaption>Fig. 4. Capturing bisimulation-invariant complexity classes, compared to their non-bisimulation-invariant counterparts. Below dotted lines, structures are assumed to be equipped with a total order (resp. a bisimulation-invariant preorder).</figcaption></figure>

LTS. For any FO formula $\Phi$ and its already defined translation $\mathrm{tr}(\Phi)$ into a $\mathrm{PHFL}(0, <, \mathrm{tail})$ formula, consider the formulas

$$ \begin{aligned} \Psi_0 &:= \bigwedge_{i=1}^{d} \{(1, 2) \leftarrow (i, i+d)\} \neg \Phi_{<} \wedge \{(2, 1) \leftarrow (i, i+d)\} \Phi_{<} \\ \Psi &:= \{s\} (\mu X. \Psi_0 \lor \exists_{2d+1} \exists_{3d} ((\{s_1\} \mathrm{tr}(\Phi)) \wedge \{s_2\} X)) \end{aligned} $$

where $s := \{1, \dots, 2d \leftarrow i_1, \dots, i_d, j_1, \dots, j_d\}$, $\{s_1\} := \{1, \dots, d \leftarrow 2d+1, 3d\}$ and $\{s_2\} := \{d+1, \dots, 2d \leftarrow 2d+1, 3d\}$. Then $\Psi$ is equivalent to $[\mathrm{TC} \ \Phi](x, y)$ with $x = x_{i_1}, \dots, x_{i_d}$ and $y = x_{j_1}, \dots, x_{j_d}$. Moreover, as $\mathrm{tr}(\Phi)$ is closed and tail-recursive, so is $\Psi$. So any formula of $\mathrm{FO[TC]}$ with a single application of the transitive closure has an equivalent in $\mathrm{PHFL}(0, <, \mathrm{tail})$; since $\mathrm{FO[TC]}$ formulas have a normal form with a single application of the transitive closure [10], this proves the result. □

# 6 Conclusion and Further Work

The results obtained here are presented in Fig. 4 and compared to those results in the descriptive complexity of the non-bisimulation-invariant world which are being used to obtain the results of this paper.

Besides the obvious question of characterisations for $NP/\sim$ and $coNP/\sim$, bisimulation-invariant complexity classes beyond $EXPTIME$ also remain to be captured. We believe that $k$-$EXPTIME/\sim$ is captured by $\mathrm{PHFL}(k)$ for $k > 1$ and $k$-$EXPSPACE/\sim$ is captured by $\mathrm{PHFL}(k-1, \mathrm{tail})$ for $k > 2$. In order to establish such results, we may want to look for other logical characterisations of these complexity classes and encode them in $\mathrm{PHFL}(\omega)$ as we did here. Although we can think about natural candidates for such logical characterisations we could not find suitable references in the literature and the generalisation of our results to higher orders and higher complexity classes is therefore deferred to future work.
References

1. Viswanathan, M., Viswanathan, R.: A higher order modal fixed point logic. In: CONCUR. Volume 3170 of LNCS., Springer (2004) 512–528

2. Kozen, D.: Results on the propositional $\mu$-calculus. TCS **27** (1983) 333–354

3. Axelsson, R., Lange, M., Somla, R.: The complexity of model checking higher-order fixpoint logic. Logical Methods in Computer Science **3** (2007) 1–33

4. Fagin, R.: Generalized first-order spectra and polynomial-time recognizable sets. Complexity and Computation **7** (1974) 43–73

5. Stockmeyer, L.J.: The polynomial-time hierarchy. TCS **3**(1) (1976) 1–22

6. Immerman, N.: Languages that capture complexity classes. SIAM Journal of Computing **16**(4) (1987) 760–778

7. Abiteboul, S., Vianu, V.: Computing with first-order logic. Journal of Computer and System Sciences **50**(2) (1995) 309–335

8. Vardi, M.Y.: The complexity of relational query languages (extended abstract). In: STOC, ACM (1982) 137–146

9. Immerman, N.: Relational queries computable in polynomial time. Information and Control **68**(1–3) (1986) 86–104

10. Immerman, N.: Descriptive Complexity. Springer, New York (1999)

11. Grädel, E., Kolaitis, P.G., Libkin, L., Marx, M., Spencer, J., Vardi, M.Y., Venema, Y., Weinstein, S.: Finite Model Theory and its Applications. Springer (2007)

12. Otto, M.: Bisimulation-invariant PTIME and higher-dimensional $\mu$-calculus. Theor. Comput. Sci. **224**(1-2) (1999) 237–265

13. Andersen, H.R.: A polyadic modal $\mu$-calculus. Technical Report 145, IT Universitetet i København (1994)

14. Milner, R.: Communication and Concurrency. International Series in Computer Science. Prentice Hall (1989)

15. Stirling, C.: Modal and Temporal Properties of Processes. Texts in Computer Science. Springer (2001)

16. Grädel, E.: Capturing complexity classes by fragments of second-order logic. Theor. Comput. Sci. **101**(1) (1992) 35–57

17. Kobayashi, N., Inaba, K., Tsukada, T.: Unsafe order-2 tree languages are context-sensitive. In: FoSSaCS. Volume 8412 of Lecture Notes in Computer Science., Springer (2014) 149–163

18. Lange, M., Lozes, E.: Capturing bisimulation invariant complexity classes with higher-order modal fixpoint logic. available at http://carrick.fmv.informatik.uni-kassel.de/lozes/tcs14-long.pdf

19. Meyer, A.R., Stockmeyer, L.J.: Word problems requiring exponential time. In: STOC, ACM (1973) 1–9

20. Tarski, A.: A lattice-theoretical fixpoint theorem and its application. Pacific Journal of Mathematics **5** (1955) 285–309

21. Àlvarez, C., Balcázar, J.L., Gabarró, J., Santha, M.: Parallel complexity in the design and analysis on concurrent systems. In: Parallel Architectures and Languages Europe, PARLE’91. Volume 505 of LNCS., Springer (1991) 288–303