# Capturing Bisimulation-Invariant Exponential-Time Complexity Classes

Florian Bruse University of Kassel
Kassel, Germany<EMAIL_ADDRESS>University of Kassel
Kassel, GermanyUniversity of Kassel
Kassel, Germany David Kronenberger University of Kassel
Kassel, GermanyUniversity of Kassel
Kassel, Germany Martin Lange University of Kassel
Kassel, Germany<EMAIL_ADDRESS>
###### Abstract

Otto’s Theorem characterises the bisimulation-invariant PTIME queries over
graphs as exactly those that can be formulated in the polyadic $\mu$-calculus,
hinging on the Immerman-Vardi Theorem which characterises PTIME (over ordered
structures) by First-Order Logic with least fixpoints. This connection has
been extended to characterise bisimulation-invariant EXPTIME by an extension
of the polyadic $\mu$-calculus with functions on predicates, making use of
Immerman’s characterisation of EXPTIME by Second-Order Logic with least
fixpoints.

In this paper we show that the bisimulation-invariant versions of all classes
in the exponential time hierarchy have logical counterparts which arise as
extensions of the polyadic $\mu$-calculus by higher-order functions. This
makes use of the characterisation of $k$-EXPTIME by Higher-Order Logic (of
order $k+1$) with least fixpoints, due to Freire and Martins.

##  1 Introduction

Descriptive complexity theory aims at characterising complexity classes –
usually defined via computational resources like time or space consumption –
by means of _logical_ resources. Its central notion is that of a complexity
class $\mathcal{C}$ being _captured_ by a logic $\mathcal{L}$ in the sense
that the properties which can be checked in complexity $\mathcal{C}$ are
exactly those that can be defined in $\mathcal{L}$. This provides a
characterisation of computational complexity that is independent of a machine
model. Instead, computational difficulty is characterised by the need for
particular logical resources like $k$-order quantifiers or fixpoints of a
particular type. It is widely believed that this provides a more promising
line of attack for notoriously difficult problems of separating complexity
classes; at least it makes machinery that is traditionally used for measuring
the expressive power of logics available for such tasks.

Here we adopt terminology from database theory as this is traditionally close
to descriptive complexity, and speak of _queries_ being _answered_ instead of
problems being solved or languages being decided, different names for the same
thing.

Ever since Fagin’s seminal work showing that the complexity class NP is
captured by Existential Second-Order Logic [6], descriptive complexity has
provided logical characterisations of many standard complexity classes. The
Abiteboul-Vianu Theorem for instance states that PSPACE is captured by First-
Order Logic with Partial Fixpoint Operators [2]. The proofs of these results
rely on the existence of a total order on the structure at hand. This is not a
restriction for characterisations of complexity classes including and above NP
as the resources available there are sufficient to construct such an order.

There is no known way to define or construct such a total order in
deterministic polynomial time which is a major obstacle for capturing the
complexity class P. There is some belief that such a logic should exist,
possibly in the form of first-order logic with additional operators like
fixpoints, counting and others, cf. [8]. This is grounded in the
characterisation of the complexity class of _Ordered Polynomial Time_ – i.e.
those queries that can be answered in polynomial time on structures that are
equipped with a total order – by First-Order Logic with Least Fixpoints [21,
9].

An interesting result was then found by Otto who considered another
restriction of the class P, namely that of _bisimulation-invariant_ queries
(on graphs, naturally). He showed that this class, denoted P
$\\!\\!{/}\\!_{\sim}$ is captured by the polyadic $\mu$-calculus
$\mathcal{L}_{\mu}^{\omega}$ [18], a generalisation of the well-known modal
$\mu$-calculus to interpretations of formulas not in states but in tuples of
states of fixed arity [3]. This is particularly interesting as it shifts the
borderline at which the availability of an order becomes critical, from
between P and NP to between P $\\!\\!{/}\\!_{\sim}$ and NLOGSPACE
$\\!\\!{/}\\!_{\sim}$.

This opens up the question of further capturing results of bisimulation-
invariant complexity classes by (modal) logics. Indeed, characterisations have
been found for EXPTIME $\\!\\!{/}\\!_{\sim}$ and PSPACE $\\!\\!{/}\\!_{\sim}$
in terms an extension of $\mathcal{L}_{\mu}^{\omega}$ by first-order functions
from predicates to predicates [16]. The logic capturing EXPTIME
$\\!\\!{/}\\!_{\sim}$ is coined $\text{PHFL}^{1}$ – Polyadic Higher-Order
Fixpoint Logic of order 1. The higher-order extension is borrowed from HFL
which extends the modal $\mu$-calculus with a simply typed $\lambda$-calculus
[22]. A syntactical restriction called _tail-recursiveness_ [5] has been
identified that captures PSPACE $\\!\\!{/}\\!_{\sim}$ [16], and when applying
this restriction to $\mathcal{L}_{\mu}^{\omega}$ or, likewise,
$\text{PHFL}^{0}$, one captures NLOGSPACE $\\!\\!{/}\\!_{\sim}$ (with the help
of a particular partial order only, though) [16].

Considering bisimulation-invariant complexity classes above NP
$\\!\\!{/}\\!_{\sim}$ does not serve the same purpose as it does for smaller
ones as one of the key motivations for moving to the bisimulation-invariant
world is to avoid the need for a total order. On the other hand, for two
complexity classes $\mathcal{C},\mathcal{C}^{\prime}$ that have complete and
bisimulation-invariant problems we have $\mathcal{C}\neq\mathcal{C}^{\prime}$
iff
$\mathcal{C}\\!\\!{/}\\!_{\sim}\neq\mathcal{C}^{\prime}\\!\\!{/}\\!_{\sim}$.
Most of the standard complexity classes posses such problems, for example
(1-letter) NFA universality for NP, resp. PSPACE, unbounded tree automaton
intersection for EXPTIME, etc. Moreover, separating bisimulation-invariant
classes may be easier due to their close connection to modal logics where
separating their expressiveness is routinely done (not for the relatively
complex higher-order modal fixpoint logics mentioned here, though).

In this paper we extend the characterisation of bisimulation-invariant time
complexity classes to all the levels of the exponential time hierarchy. We
show that $k$-EXPTIME $\\!\\!{/}\\!_{\sim}$ is captured by $\text{PHFL}^{k}$,
the polyadic version of the higher-order extension of the modal $\mu$-calculus
with functions up to type order $k$. We remark that a similar characterisation
of the space complexity classes $k$-EXPSPACE is also possible [14] but needs
to be omitted for lack of space and is therefore left for a future
publication.

The paper is organised as follows. In Sect. 2 we recall the necessary
preliminaries, mainly about the logics studied here. In Sect. 3 we provide the
easy half of the capturing result by putting together known results and
constructions which witness that any $\text{PHFL}^{k}$ query can be answered
in $k$-fold exponential time. In Sect. 4 we prepare for the more difficult and
other half of the capturing result. We rely on a logical characterisation of
$k$-EXPTIME in terms of Higher-Order Predicate Logic with Fixpoints [7], and a
key step in expressing such (bisimulation-invariant) queries in Higher-Order
Modal Fixpoint is the modelling of higher-order quantification using an
enumeration technique. In Sect. 5 we put this to use for showing that any
$k$-EXPTIME $\\!\\!{/}\\!_{\sim}$-query is definable in $\text{PHFL}^{k}$. In
Sect. 6 we conclude with remarks on further work etc.

##  2 Preliminaries

Let $\mathbf{P}$ and $\mathbf{A}$ be finite sets of _propositions_ , resp.
_actions_. A labelled transition system (LTS) is a tuple
${T}=({S},\\{\mathop{{\hbox{{$\mathrel{\mathop{\hbox
to10.70013pt{\rightarrowfill}}\limits^{a}}$}}}}\\}_{a\in\mathbf{A}},\ell)$
where ${S}$ is a nonempty set of _states_ ,
$\mathop{{\hbox{{$\mathrel{\mathop{\hbox
to10.70013pt{\rightarrowfill}}\limits^{a}}$}}}}\subseteq{S}\times{S}$ is a
_transition relation_ for each action $a\in\mathbf{A}$, and $\ell\colon{S}\to
2^{\mathbf{P}}$ labels the states with those propositions that are true in
them. We write $s\mathop{{\hbox{{$\mathrel{\mathop{\hbox
to10.70013pt{\rightarrowfill}}\limits^{a}}$}}}}t$ instead of
$(s,t)\in\mathop{{\hbox{{$\mathrel{\mathop{\hbox
to10.70013pt{\rightarrowfill}}\limits^{a}}$}}}}$.

For $d\geq 1$, a $d$-_pointed LTS_ is a pair ${T},(s_{1},\dotsc,s_{d})$ of an
LTS and a $d$-tuple of states in it. It is also simply called _pointed_ when
$d$ is clear from the context. Note that in the case of $d=1$, this coincides
with the usual notion of a pointed LTS. Given some tuple
$\overline{s}=(s_{1},\dotsc,s_{d})$ and $i\leq d$, we write
$\overline{s}[t/i]$ to denote the tuple
$(s_{1},\dotsc,s_{i-1},t,s_{i+1},\dotsc,s_{d})$.

###  2.1 Polyadic Higher-Order Fixpoint Logic

We assume familiarity with the modal $\mu$-calculus $\mathcal{L}_{\mu}$ [13].
Polyadic Higher-Order Fixpoint Logic PHFL [16] extends $\mathcal{L}_{\mu}$ in
several ways: (i) HFL [22] adds to it a simply typed $\lambda$-calculus; (ii)
the polyadic $\mathcal{L}_{\mu}$, $\mathcal{L}_{\mu}^{\omega}$ [3, 18] is
obtained by lifting the interpretation of formulas in states to tuples of
states of fixed arity. Now PHFL merges both extensions. Its introduction
requires a few technicalities.

#### Types.

Types are used to govern the syntax of PHFL, especially those parts that
denote functions. They are derived from the grammar

$\tau\Coloneqq\bullet\mid\tau^{v}\to\tau$

where $\bullet$ is a ground type for propositions, $v\in\\{+,-,0\\}$ are
_variances_ denoting whether a function is monotonically increasing,
monotonically decreasing, or constant in its argument. Variances are only
needed to check well-typedness; we often do not display them for the sake of
readability.

The _order_ $\mathit{ord}$ of a type is defined via $\mathit{ord}(\bullet)=0$
and
$\mathit{ord}(\tau_{1}\to\tau_{2})=\max(\mathit{ord}(\tau_{1})+1,\mathit{ord}(\tau_{2}))$.
Types associate to the right whence every type is of the form
$\tau_{1}\to\dotsb\to\tau_{n}\to\bullet$.

Given some LTS ${T}=({S},\\{\mathop{{\hbox{{$\mathrel{\mathop{\hbox
to10.70013pt{\rightarrowfill}}\limits^{a}}$}}}}\\}_{a\in\mathbf{A}},\ell)$ and
some $0<d\in\mathbb{N}$, the semantics $\llbracket\tau\rrbracket^{{T}}$ of a
type $\tau$ is a complete lattice, defined inductively as follows:

$\displaystyle\llbracket\bullet\rrbracket^{{T}}$
$\displaystyle=(2^{{S}^{d}},\subseteq)$
$\displaystyle\llbracket\tau_{2}^{v}\to\tau_{1}\rrbracket^{{T}}$
$\displaystyle=(\llbracket\tau_{2}\rrbracket^{{T}}\to\llbracket\tau_{1}\rrbracket^{{T}},\sqsubseteq_{\tau_{2}^{v}\to\tau_{1}})$

where we tacitly identify a lattice with its domain and where the order
$\sqsubseteq_{\tau_{2}^{v}\to\tau_{1}}$ is given by

$f\sqsubseteq_{\tau_{2}^{v}\to\tau_{1}}g\quad\Leftrightarrow\quad\text{for all
}x\in\llbracket\tau_{2}\rrbracket^{{T}}\text{ we have }\left\\{\begin{aligned}
f(x)\sqsubseteq_{\tau_{1}}g(x)&,\text{ if }v=+\\\
g(x)\sqsubseteq_{\tau_{1}}f(x)&,\text{ if }v=-\\\ f(x)=g(x)&,\text{ if
}v=0.\end{aligned}\right.$

Hence, the semantics of $\bullet$ is the powerset lattice over ${S}^{d}$ and
$\tau_{2}^{v}\to\tau_{1}$ is the lattice of all monotonically increasing,
monotonically decreasing or constant functions from
$\llbracket\tau_{2}\rrbracket^{{T}}$ to $\llbracket\tau_{1}\rrbracket^{{T}}$,
depending on $v$. Such a set together with the above point-wise order forms a
complete lattice if $\llbracket\tau_{1}\rrbracket^{{T}}$ is one. Hence,
monotone functions in such a lattice always have a least and greatest fixpoint
due to the Knaster-Tarski-Theorem. We write
$\bigsqcup_{\tau_{2}^{v}\to\tau_{1}}$ to denote the join operator in this
lattice.

Note that, technically, $\llbracket\tau_{1}\rrbracket^{{T}}$ is also
parameterised in $d$. However, since $d$ is usually clear from context, we do
not display it to avoid clutter.

#### Syntax.

Let $\mathbf{P}$ and $\mathbf{A}$ be as above and let $\mathbf{F}$ and
$\mathbf{L}$ be finite sets of _fixpoint variables_ , resp.  _lambda
variables_. We use upper case letters $X,Y,\dots$ for the former and lower
case letters $x,y,f,g$ for the latter.

Let $d\geq 1$. By $[d]$ we denote the set $1,\ldots,d$. The set of –
potentially non-well-formed – formulas of the $d$-adic fragment of PHFL,
called $\text{PHFL}_{d}$, is derived via

$\varphi\Coloneqq p_{i}\mid\varphi\vee\varphi\mid\neg\varphi\mid\langle
a_{i}\rangle\varphi\mid\\{\sigma\\}\varphi\mid\lambda(x\colon\tau).\
\varphi\mid x\mid(\varphi\,\varphi)\mid\mu(X\colon\tau).\,\varphi\mid X$

where $x\in\mathbf{L}$, $X\in\mathbf{F}$, $p\in\mathbf{P}$, $a\in\mathbf{A}$,
$1\leq i\leq d$ and $\sigma\colon[d]\to[d]$ is a mapping on so-called
_indices_. We assume that standard connectives such as $\mathtt{f\\!f}$,
$\wedge,[a]$ and $\nu(X\colon\tau)$ are available via the obvious dualities if
needed. We will also allow ourselves to use more convenient notation for the
definition of (more complex) functions and their applications. For instance,
$(\ldots((\varphi\,\psi_{1})\,\psi_{2})\ldots)\,\psi_{n}$ is simply written as
$\varphi(\psi_{1},\ldots,\psi_{n})$, and
$\lambda(x_{1}\colon\tau_{1}).\lambda(x_{2}\colon\tau_{2}).\ldots\lambda(x_{n}\colon\tau_{n}).\psi$
is written as $\lambda(x_{1}\colon\tau_{1},\ldots,x_{n}\colon\tau_{n}).\psi$,
or even $\lambda(x_{1},\dotsc,x_{n}\colon\tau).\psi$ if $\tau=\tau_{i}$ for
all $1\leq i\leq n$.

The notions of free and bound variables in a formula are as usual, with
$\lambda(x\colon\tau).\varphi$ binding $x$ and with $\mu(X\colon\tau).\
\varphi$ binding $X$.

Over an LTS ${T}$, a $\text{PHFL}_{d}$ formula intuitively defines a set of
$d$-tuples in ${T}$, or a function that transforms such a set into such a set,
or into a function etc., depending on the formula’s type which will be
explained shortly. Before that we briefly introduce the intuitive meaning of
the operators in the syntax. The first five listed in the grammar above all
define a subset of ${S}^{d}$. For example, $p_{i}$ denotes all tuples such
that $p$ holds at their $i$th state. The operator $\\{\sigma\\}\varphi$
rearranges the positions in tuples in such a subset. The modality $\langle
a_{i}\rangle\varphi$ expresses that $\varphi$ holds on a tuple after replacing
the $i$th state in it by some $a$-successor. A formula of the form
$\lambda(x\colon\tau^{v}).\,\varphi$ defines a function that consumes an
argument of type $\tau$ and is monotonically increasing, monotonically
decreasing, or constant in this argument, depending on $v$. A formula of the
form $(\varphi\,\psi)$ denotes the application of the semantics of $\varphi$
to the object defined by $\psi$. Finally, fixpoints can now also define
higher-order functions.

Obviously, not all formulas that can be derived from the above grammar can be
given a semantics in a meaningful way; consider e.g. $(p_{1}\,p_{2})$,
Moreover, as is typical in a situation involving least and greatest fixpoints,
the use of negation has to be restricted, cf. the example
$\mu(X\colon\bullet).\ \neg X$. Hence, PHFL has a type system to filter out
formulas that cannot be endowed with a proper semantics.

$\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
16.32744pt\vbox{\vbox{}\hbox{\hskip-16.32744pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
p_{i}\colon\bullet$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
45.03604pt\vbox{\hbox{\hskip-45.03604pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\varphi_{1}\colon\bullet$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\varphi_{2}\colon\bullet$}}}}\vbox{}}}\over\hbox{\hskip
26.63329pt\vbox{\vbox{}\hbox{\hskip-26.63327pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\varphi_{1}\vee\varphi_{2}\colon\bullet$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
15.49301pt\vbox{\hbox{\hskip-15.49301pt\hbox{\hbox{$\displaystyle\displaystyle{}\overline{\Gamma}\vdash\varphi\colon\bullet$}}}\vbox{}}}\over\hbox{\hskip
23.06242pt\vbox{\vbox{}\hbox{\hskip-23.06241pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\neg\varphi\colon:\bullet$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
17.50687pt\vbox{\hbox{\hskip-17.50687pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\varphi:\bullet$}}}\vbox{}}}\over\hbox{\hskip
23.6145pt\vbox{\vbox{}\hbox{\hskip-23.61449pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\langle
a_{i}\rangle\varphi\colon\bullet$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
17.50687pt\vbox{\hbox{\hskip-17.50687pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\varphi:\bullet$}}}\vbox{}}}\over\hbox{\hskip
23.9751pt\vbox{\vbox{}\hbox{\hskip-23.97508pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\\{\sigma\\}\varphi\colon\bullet$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
30.93813pt\vbox{\hbox{\hskip-30.93811pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,x^{v}\colon\tau_{1}\vdash\varphi\colon\tau_{2}$}}}\vbox{}}}\over\hbox{\hskip
49.66275pt\vbox{\vbox{}\hbox{\hskip-49.66273pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\lambda(x^{v}:\tau_{1}).\
\varphi\colon\tau_{1}^{v}\to\tau_{2}$}}}}}}$
$\displaystyle\displaystyle{\hbox{\hskip
20.93634pt\vbox{\hbox{\hskip-20.93633pt\hbox{\hbox{$\displaystyle\displaystyle
v\in\\{+,0\\}$}}}\vbox{}}}\over\hbox{\hskip
32.44704pt\vbox{\vbox{}\hbox{\hskip-32.44704pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\;,\;x^{v}\colon\tau\vdash
x\colon\tau$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
31.92415pt\vbox{\hbox{\hskip-31.92413pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma,X^{+}\colon\tau\vdash\varphi\colon\tau$}}}\vbox{}}}\over\hbox{\hskip
41.09242pt\vbox{\vbox{}\hbox{\hskip-41.0924pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\mu(X\colon\tau).\
\varphi\colon\tau$}}}}}}$ $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
36.52129pt\vbox{\vbox{}\hbox{\hskip-36.52129pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\;,\;X^{+}\colon\tau\vdash
X\colon\tau$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
57.45992pt\vbox{\hbox{\hskip-57.4599pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\varphi_{1}:\tau_{2}^{+}\to\tau_{1}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\varphi_{2}:\tau_{2}$}}}}\vbox{}}}\over\hbox{\hskip
32.44122pt\vbox{\vbox{}\hbox{\hskip-32.44122pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash(\varphi_{1}\
\varphi_{2})\colon\tau_{1}$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
55.44606pt\vbox{\hbox{\hskip-55.44604pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\varphi_{1}:\tau_{2}^{-}\to\tau_{1}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\overline{\Gamma}\vdash\varphi_{2}:\tau_{2}$}}}}\vbox{}}}\over\hbox{\hskip
32.44122pt\vbox{\vbox{}\hbox{\hskip-32.44122pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash(\varphi_{1}\
\varphi_{2})\colon\tau_{1}$}}}}}}$ $\displaystyle\displaystyle{\hbox{\hskip
85.4387pt\vbox{\hbox{\hskip-85.43869pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\varphi_{1}:\tau_{2}^{0}\to\tau_{1}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\varphi_{2}\colon\tau_{2}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\overline{\Gamma}\vdash\varphi_{2}\colon\tau_{2}$}}}}}\vbox{}}}\over\hbox{\hskip
27.16347pt\vbox{\vbox{}\hbox{\hskip-27.16347pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\varphi_{1}\
\varphi_{2}\colon\tau_{1}$}}}}}}$ Figure 1: The PHFL typing system.

A finite sequence $\Gamma$ of _hypotheses_ of the form $X^{v}\colon\tau$ or
$x^{v}\colon\tau$ in which each variable occurs at most once is called a
_context_. The dual context $\overline{\Gamma}$ is obtained from $\Gamma$ by
replacing all the hypotheses of the form $X^{+}\colon\tau$ by
$X^{-}\colon\tau$ and vice versa, and doing the same for lambda variables. We
say that $\varphi$ has type $\tau$ in the context $\Gamma$ if the statement
$\Gamma\vdash\varphi\colon\tau$ can be derived from the rules in Fig. 1. A
formula without free variables is _well-typed_ if the statement
$\emptyset\vdash\varphi\colon\bullet$ can be derived from these rules. We
tacitly assume that each fixpoint variable and each lambda variable is bound
at most once in a well-typed formula, and that no variable occurs both freely
and bound in a formula. Hence, each variable has a unique type in the context
of a given, well-formed formula. If the type information is clear from context
or not important, we drop it from binders, simply writing $\lambda
x.\,\varphi$ and $\mu X.\,\varphi$ for better readability.

A formula is said to be of order $k$ if the maximal order of the type of any
subformula in $\varphi$ is $k$. By $\text{PHFL}^{k}_{d}$ we denote the set of
well-typed formulas in $\text{PHFL}_{d}$ that are of order $k$. Note that PHFL
does indeed constitute an extension of other known formalisms, namely

  * •

$\text{PHFL}^{k}_{1}$ is the same as $\text{HFL}^{k}$ for any $k\geq 0$ and,
thus $\text{PHFL}_{1}=\text{HFL}$, and in particular

  * •

$\text{PHFL}^{0}_{1}$ is just the modal $\mu$-calculus $\mathcal{L}_{\mu}$
while

  * •

$\text{PHFL}^{0}_{d}$ is the $d$-dimensional polyadic $\mu$-calculus.

#### Semantics.

Let ${T}=({S},\\{\mathop{{\hbox{{$\mathrel{\mathop{\hbox
to10.70013pt{\rightarrowfill}}\limits^{a}}$}}}}\\}_{a\in\mathbf{A}},\ell)$ be
an LTS and let $\varphi$ be a well-typed formula. An _environment_ is a
function $\eta$ that assigns to each fixpoint variable and each lambda
variable of type $\tau$ an element of $\llbracket\tau\rrbracket^{{T}}$.

Let $d\geq 1$. The semantics
$\llbracket\varphi\colon\tau\rrbracket^{{T}}_{\eta}$ of a $\text{PHFL}_{d}$
formula $\varphi$ of type $\tau$, relative to an LTS ${T}$ and an environment
$\eta$, is an object of $\llbracket\tau\rrbracket^{{T}}$, defined recursively
as follows.

$\displaystyle\llbracket\Gamma\vdash
p_{i}\colon\bullet\rrbracket^{{T}}_{\eta}$
$\displaystyle=\\{(s_{1},\dotsc,s_{d}\in{S}^{d}\mid p\in\ell(s_{i})\\}$
$\displaystyle\llbracket\Gamma\vdash\varphi_{1}\vee\varphi_{2}\colon\bullet\rrbracket^{{T}}_{\eta}$
$\displaystyle=\llbracket\Gamma\vdash\varphi_{1}\colon\bullet\rrbracket^{{T}}_{\eta}\cup\llbracket\Gamma\vdash\varphi_{2}\colon\bullet\rrbracket^{{T}}_{\eta}$
$\displaystyle\llbracket\Gamma\vdash\neg\varphi\colon\bullet\rrbracket^{{T}}_{\eta}$
$\displaystyle={S}^{d}\setminus\llbracket\overline{\Gamma}\vdash\varphi\colon\bullet\rrbracket^{{T}}_{\eta}$
$\displaystyle\begin{split}\llbracket\Gamma\vdash\langle
a_{i}\rangle\varphi\colon\bullet\rrbracket^{{T}}_{\eta}&=\\{(s_{1},\dotsc,s_{d})\in{S}^{d}\mid\text{
ex. }t\text{ s.t. }\\\
&\qquad\qquad\qquad(s_{1},\dotsc,s_{i_{1}},t,s_{i+1},\dotsc,s_{d})\in\llbracket\Gamma\vdash\varphi\colon\bullet\rrbracket^{{T}}_{\eta}\text{
and }s_{i}\mathop{{\hbox{{$\mathrel{\mathop{\hbox
to10.70013pt{\rightarrowfill}}\limits^{a}}$}}}}t\\}\end{split}$
$\displaystyle\llbracket\Gamma\vdash\\{\sigma\\}\varphi\colon\bullet\rrbracket^{{T}}_{\eta}$
$\displaystyle=\\{(s_{1},\dotsc,s_{d})\in{S}^{d}\mid(s_{\sigma(1)},\dotsc,s_{\sigma(d)})\in\llbracket\Gamma\vdash\varphi\colon\bullet\rrbracket^{{T}}_{\eta}\\}$
$\displaystyle\llbracket\Gamma\vdash\lambda(x^{v}\colon\tau_{2}).\
\varphi\colon\tau_{2}^{v}\to\tau_{1}\rrbracket^{{T}}_{\eta}$
$\displaystyle=f\in\llbracket\tau_{2}^{v}\to\tau_{1}\rrbracket^{{T}}\text{
s.t.~{}f.a. }y\in\llbracket\tau_{2}\rrbracket^{{T}}.\
f(y)=\llbracket\Gamma,x^{v}\colon\tau_{2}\vdash\varphi\colon\tau_{1}\rrbracket^{{T}}_{\eta[x\mapsto
y]}$ $\displaystyle\llbracket\Gamma\vdash x\colon\tau\rrbracket^{{T}}_{\eta}$
$\displaystyle=\eta(x)$
$\displaystyle\llbracket\Gamma\vdash(\varphi_{1}\,\varphi_{2})\colon\tau_{1}\rrbracket^{{T}}_{\eta}$
$\displaystyle=\llbracket\Gamma\vdash\varphi_{1}\colon\tau_{2}^{v}\to\tau_{1}\rrbracket^{{T}}_{\eta}\,(\llbracket\Gamma\vdash\varphi_{2}\colon\tau_{2}\rrbracket^{{T}}_{\eta})$
$\displaystyle\llbracket\Gamma\vdash\mu(X\colon\tau).\varphi\colon\tau\rrbracket^{{T}}_{\eta}$
$\displaystyle=\bigsqcap_{\tau\to\tau}\\{d\in\llbracket\tau\rrbracket^{{T}}_{\eta}\mid\llbracket\Gamma,X\colon\tau^{+}\vdash\varphi\colon\tau\rrbracket^{{T}}_{\eta[X\mapsto
d]}\sqsubseteq_{\tau}d\\}$ $\displaystyle\llbracket\Gamma\vdash
X\colon\tau\rrbracket^{{T}}_{\eta}$ $\displaystyle=\eta(X)$

If the type is clear from context, or not important, we simply write
$\llbracket\varphi\rrbracket^{{T}}_{\eta}$. We write
${T},(s_{1},\dotsc,s_{d})\models_{\eta}\varphi$ if $\varphi\colon\bullet$ and
$(s_{1},\dotsc,s_{d})\in\llbracket\varphi\rrbracket^{{T}}_{\eta}$. We say that
two formulas $\varphi$ and $\psi$ are _equivalent_ , written
$\varphi\equiv\psi$, if for all ${T}$ and all $\eta$ we have
$\llbracket\varphi\rrbracket^{{T}}_{\eta}=\llbracket\psi\rrbracket^{{T}}_{\eta}$.

It is well-known that the semantics of HFL and, hence, PHFL is invariant under
$\beta$-reduction and admits the fixpoint unfolding principle, i.e. $\mu
X.\,\varphi\equiv\varphi[\mu X.\,\varphi/X]$ where substitution is defined as
usual.

#### Bisimilarity.

A _bisimulation_ $R$ on an LTS
${T}=({S},\\{\mathop{{\hbox{{$\mathrel{\mathop{\hbox
to10.70013pt{\rightarrowfill}}\limits^{a}}$}}}}\\}_{a\in\mathbf{A}},\ell)$ is
a symmetric relation $R\subseteq{S}\times{S}$ satisfying the following for all
$(s,t)\in R$.

  * •

$\ell(s)=\ell(t)$,

  * •

if there is $a\in\mathbf{A}$ and $s^{\prime}\in{S}$ s.t.
$s\mathop{{\hbox{{$\mathrel{\mathop{\hbox
to10.70013pt{\rightarrowfill}}\limits^{a}}$}}}}s^{\prime}$ then there is
$t^{\prime}\in{S}$ with $t\mathop{{\hbox{{$\mathrel{\mathop{\hbox
to10.70013pt{\rightarrowfill}}\limits^{a}}$}}}}t^{\prime}$ and
$(s^{\prime},t^{\prime})\in R$,

  * •

if there is $a\in\mathbf{A}$ and $t^{\prime}\in{S}$ s.t.
$t\mathop{{\hbox{{$\mathrel{\mathop{\hbox
to10.70013pt{\rightarrowfill}}\limits^{a}}$}}}}t^{\prime}$ then there is
$s^{\prime}\in{S}$ with $s\mathop{{\hbox{{$\mathrel{\mathop{\hbox
to10.70013pt{\rightarrowfill}}\limits^{a}}$}}}}s^{\prime}$ and
$(s^{\prime},t^{\prime})\in R$.

Two states $s,t$ are bisimilar, written $s\sim t$, if there is a bisimulation
$R$ with $(s,t)\in R$.

Let $d\geq 1$. A set $T\subseteq{S}$ is called _bisimulation-invariant_ if for
all $\bar{s}=(s_{1},\ldots,s_{d}),\bar{t}=(t_{1},\ldots,t_{d})\in{S}^{d}$ such
that $s_{i}\sim t_{i}$ for all $i\in[d]$, we have $\bar{s}\in T$ iff
$\bar{t}\in T$. The notion of bisimulation-invariance can straight-forwardly
be lifted to objects of type $\llbracket\tau\rrbracket^{{T}}$ for types
$\tau\neq\bullet$, cf. [22].

It is well-known that modal logics cannot distinguish bisimilar models, and it
is not surprising that the extensions beyond pure modal logic that are
available in PHFL do not break this property.

######  Proposition 1 ([22, 16]).

Let $d\geq 1$, ${T}$ be an LTS with state set ${S}$ and $\varphi$ be a closed
$\text{PHFL}_{d}$ formula of type $\bullet$. Then
$\llbracket\varphi\rrbracket^{{T}}\subseteq{S}^{d}$ is bisimulation-invariant.

######  Example 2 ([18]).

A standard example shows that bisimilarity itself is definable in
$\text{PHFL}^{0}_{2}$, provided that $\mathbf{P}$ and $\mathbf{A}$ are finite.
The $\text{PHFL}^{0}_{2}$ formula

$\varphi_{\sim}:=\nu(X:\bullet).(\bigwedge\limits_{p\in\mathbf{P}}p_{1}\leftrightarrow
p_{2})\wedge(\bigwedge\limits_{a\in\mathbf{A}}[a_{1}]\langle a_{2}\rangle
X)\wedge\\{1\mapsto 2,2\mapsto 1\\}X$

is satisfied by a pair $(s,t)$ of some ${T}$ iff $s\sim t$. The formula
essentially states that $(s,t)$ needs to belong to the largest set $X$ of
states $(s^{\prime},t^{\prime})$ that agree on all propositions (first
conjunct) and for which $t^{\prime}$ can match any $a$-transition out of
$s^{\prime}$, for any $a\in\mathbf{A}$, to a pair
$(s^{\prime\prime},t^{\prime\prime})\in X$ (second conjunct). Moreover, $X$
needs to be a symmetric relation (third conjunct).

To exemplify the use of higher-orderness (here: first-order functions) we can
use the definability of finite-trace equivalence in $\text{PHFL}^{1}_{2}$.

######  Example 3.

Two states $s,t$ are finite-trace equivalent if whenever there is a sequence
$s\mathop{{\hbox{{$\mathrel{\mathop{\hbox
to12.70013pt{\rightarrowfill}}\limits^{a_{1}}}$}}}}s_{1}\mathop{{\hbox{{$\mathrel{\mathop{\hbox
to12.70013pt{\rightarrowfill}}\limits^{a_{2}}}$}}}}s_{2}\mathop{{\hbox{{$\mathrel{\mathop{\hbox
to12.70013pt{\rightarrowfill}}\limits^{a_{3}}}$}}}}$
$\ldots\mathop{{\hbox{{$\mathrel{\mathop{\hbox
to13.10107pt{\rightarrowfill}}\limits^{a_{n}}}$}}}}s_{n}$ then there are
$t_{1},\ldots,t_{n}$ s.t. $t\mathop{{\hbox{{$\mathrel{\mathop{\hbox
to12.70013pt{\rightarrowfill}}\limits^{a_{1}}}$}}}}t_{1}\mathop{{\hbox{{$\mathrel{\mathop{\hbox
to12.70013pt{\rightarrowfill}}\limits^{a_{2}}}$}}}}t_{2}\mathop{{\hbox{{$\mathrel{\mathop{\hbox
to12.70013pt{\rightarrowfill}}\limits^{a_{3}}}$}}}}\ldots\mathop{{\hbox{{$\mathrel{\mathop{\hbox
to13.10107pt{\rightarrowfill}}\limits^{a_{n}}}$}}}}t_{n}$ and vice-versa.

$\varphi_{\mathsf{fte}}:=\big{(}\nu F(x,y).(x\leftrightarrow
y)\wedge\bigwedge\limits_{a\in\mathbf{A}}F(\langle a_{1}\rangle x,\langle
a_{2}\rangle y))(\mathtt{t\\!t},\mathtt{t\\!t})$

is then satisfied by a pair $(s,t)$ iff $s$ and $t$ are finite-trace
equivalent in the sense above. The greatest fixpoint in the formula expresses
an infinite conjunction over all finite paths, these can be thought of to be
built step-wise via fixpoint unfolding; the $n$th unfolding expresses that all
finite traces of length $n$ are available in the first component of the tuple
(and built via $\langle a_{1}\rangle$) iff they are available in the second
component (built via $\langle a_{2}\rangle$. For better readability we have
omitted the types in the formula. The types of $x,y$ are $\bullet$ and that of
$F$ is, consequently, $\bullet^{0}\to\bullet^{0}\to\bullet$.

We remark that it is easily possible to extend the formula to also check for
matching atomic propositions along the traces emerging from $s$ and $t$. Cf.
[17] for further examples of how various other process equivalences and
preorders can be expressed in $\text{PHFL}^{1}$.

###  2.2 Higher-Order Logic with Least Fixpoints

We introduce Higher-Order Logic with Least Fixpoints (HO(LFP)) to make use of
the characterisation of $k$-EXPTIME over the class of ordered structures as
the queries definable in order-$(k+1)$ HO(LFP), due to Immerman and Vardi [9,
21, 10], resp. Freire and Martins [7].

#### Types.

Types for Higher-Order Logic with Least Fixpoints are constructed, similar to
those for PHFL, from a single base type and one constructor:
$\tau^{\prime}\Coloneqq\odot\mid(\tau^{\prime},\dotsc,\tau^{\prime})$. Here,
however, $\odot$ is the type of _individuals_ (like states rather than sets of
states), and the tuple type is used to denote (higher-order) relations. We
define the order111Note the discrepancy in the traditional ways to assign
numerals to orders in the two logics considered here: order $1$ in HO(LFP)
refers to, like in “First-Order Logic”, individual elements and order $2$ is
for relations like sets thereof. In PHFL, order $1$ refers to the order of a
function, i.e. one that takes sets of arguments. This explains why
$\text{PHFL}^{k}$ corresponds to the fragment of HO(LFP) of order $k+1$, see
also the right column in Fig. 2. of a type via $\mathit{ord}(\odot)=1$ and
$\mathit{ord}(\tau^{\prime}_{1},\dots,\tau^{\prime}_{n})=1+\max\\{\mathit{ord}(\tau^{\prime}_{1}),\dotsc,\mathit{ord}(\tau^{\prime}_{n})\\}$.

Let ${T}=({S},\\{\mathop{{\hbox{{$\mathrel{\mathop{\hbox
to10.70013pt{\rightarrowfill}}\limits^{a}}$}}}}\\}_{a\in\mathbf{A}},\ell)$ be
an LTS. This induces a set-theoretic interpretation of types via
$\llbracket\odot\rrbracket^{{T}}={S}$ and
$\llbracket(\tau^{\prime}_{1},\dots,\tau^{\prime}_{n})\rrbracket^{{T}}=2^{\llbracket\tau^{\prime}_{1}\rrbracket^{{T}}\times\dotsb\times\llbracket\tau^{\prime}_{n}\rrbracket^{{T}}}$.

#### Syntax.

Let $\mathbf{V}=\\{X,\dotsc\\}$ be a countable set of _higher-order variables_
, each implicitly equipped with a type. Let $\mathbf{P},\mathbf{A}$ be sets of
propositions, resp. actions. The syntax of HO(LFP) formulas is derived from
the following grammar:

$\varphi\Coloneqq p(X)\mid a(X,Y)\mid
X(Y_{1},\dotsc,Y_{N})\mid\neg\varphi\mid\varphi\vee\varphi\mid\exists(X\colon\tau^{\prime}).\
\varphi\mid\big{(}\mathit{lfp}(X,Y_{1},\dotsc,Y_{N}).\
\varphi\big{)}(Z_{1},\dotsc,Z_{n})$

where $p\in\mathbf{P}$, $a\in\mathbf{A}$ and
$X,Y_{1},\dotsc,Y_{n},Z_{1},\dotsc,Z_{n}\in\mathbf{V}$. Again, dual operators
such as $\wedge$ and $\mathit{gfp}$ (for greatest fixpoints) are available via
the obvious dualities. The variable $X$ is bound in
$\exists(X\colon\tau^{\prime}).\ \varphi$ and $X,Y_{1},\dotsc,Y_{N}$ are bound
in $\big{(}\mathit{lfp}(X,Y_{1},\dotsc,Y_{N}).\
\varphi\big{)}(Z_{1},\dotsc,Z_{n})$. A formula is _well-formed_ if each
variable is bound at most once, and, moreover, variables occur only in a way
that matches their type. For example, only a variable of type $\odot$ can
occur in a subformula of the form $p(X)$, and if a subformula of the form
$X(Y_{1},\dotsc,Y_{n})$ occurs, then $X$ has type
$(\tau^{\prime}_{1},\dotsc,\tau^{\prime}_{n})$ for some
$\tau^{\prime}_{1},\dotsc,\tau^{\prime}_{n}$ and $Y_{i}$ has type
$\tau^{\prime}_{i}$ for all $1\leq i\leq n$. Moreover, in a subformula of the
form $\big{(}\mathit{lfp}(X,Y_{1},\dotsc,Y_{N}).\
\varphi\big{)}(Z_{1},\dotsc,Z_{n})$, the variable $X$ occurs only under an
even number of negations in $\varphi$. For a more detailed introduction into
Higher-Order Logic including formal ways to define well-formedness of
formulas, cf. [20]. In a well-formed formula each variable has a unique type.
An HO(LFP) formula $\varphi$ has order $k$ if the order of the highest type of
a variable in $\varphi$ is at most $k$. We write
$\textsf{HO}^{k}\textsf{(LFP)}$ for the set of HO(LFP) formulas of order at
most $k$.

#### Semantics.

Let ${T}=({S},\\{\mathop{{\hbox{{$\mathrel{\mathop{\hbox
to10.70013pt{\rightarrowfill}}\limits^{a}}$}}}}\\}_{a\in\mathbf{A}},\ell)$ be
an LTS. A variable assignment $\alpha$ is a function that maps each variable
in $\mathbf{V}$ of type $\tau^{\prime}$ into
$\llbracket\tau^{\prime}\rrbracket^{{T}}$.

Let $\varphi$ be an HO(LFP) formula with free variables in
$X,Y_{1},\dotsc,Y_{n}$ such that $X$ occurs only under an even number of
negations in $\varphi$ and let
$\tau^{\prime}=(\tau^{\prime}_{1},\dotsc,\tau^{\prime}_{n})$ be the type of
$X$ in $\varphi$ while $\tau^{\prime}_{i}$ is the type of $Y_{i}$ in $\varphi$
for $1\leq i\leq n$. Then, given some variable assignment $\alpha$, the
formula $\varphi$ defines a monotone function
$f\colon\llbracket\tau^{\prime}\rrbracket^{{T}}\to\llbracket\tau^{\prime}\rrbracket^{{T}}$
via

$f(M)\mapsto\\{(m_{1},\dotsc,m_{n})\in\llbracket\varphi\rrbracket^{{T}}_{\alpha[Y_{1}\mapsto
m^{\prime}_{1},\dotsc,Y_{n}\mapsto
m^{\prime}_{n}]}\mid(m^{\prime}_{1},\dotsc,m^{\prime}_{n})\in M\\}.$

By the Knaster-Tarski-Theorem [12, 19] this function has a least fixpoint
denoted by $\mathit{LFP}(X,Y_{1},\dotsc,Y_{n})\varphi$. Note that we suppress
${T}$ and $\alpha$ here since they will always be clear from context.

The satisfaction relation between an LTS ${T}$, a variable assignment $\alpha$
and an HO(LFP) formula $\varphi$ is defined inductively as follows.

$\displaystyle{T},\alpha\models p(X)$ $\displaystyle\text{ iff
}p\in\ell(\alpha(X))$ $\displaystyle{T},\alpha\models a(X,Y)$
$\displaystyle\text{ iff }\alpha(X)\mathop{{\hbox{{$\mathrel{\mathop{\hbox
to10.70013pt{\rightarrowfill}}\limits^{a}}$}}}}\alpha(Y)$
$\displaystyle{T},\alpha\models X(Y_{1},\dotsc,Y_{n})$ $\displaystyle\text{
iff }(\alpha(Y_{1}),\dotsc,\alpha(Y_{n}))\in\alpha(X)$
$\displaystyle{T},\alpha\models\neg\varphi$ $\displaystyle\text{ iff
}{T},\alpha\not\models\varphi$
$\displaystyle{T},\alpha\models\varphi_{1}\vee\varphi_{2}$
$\displaystyle\text{ iff }{T},\alpha\models\varphi_{1}\text{ or
}{T},\alpha\models\varphi_{2}$
$\displaystyle{T},\alpha\models\exists(X\colon\tau^{\prime})$
$\displaystyle\text{ iff ex.\
}d\in\llbracket\tau^{\prime}\rrbracket^{{T}}\text{ s.t.\ }{T},\alpha[X\mapsto
d]\models\varphi$
$\displaystyle{T},\alpha\models\big{(}\mathit{lfp}(X,Y_{1},\dotsc,Y_{N}).\
\varphi\big{)}(Z_{1},\dotsc,Z_{n})$ $\displaystyle\text{ iff
}(\alpha(Z_{1}),\dotsc,\alpha(Z_{n}))\in\mathit{LFP}(X,Y_{1},\dotsc,Y_{n})\varphi.$

###  2.3 Descriptive Complexity

A _query_ (of dimension $d$) is a set $Q$ of pairs
$({T},(s_{1},\ldots,s_{d}))$ s.t. each ${T}$ is finite. It is expressed by the
HO(LFP) formula $\varphi$ with free variables $X_{1},\dotsc,X_{d}$, if
$Q=\\{({T},(s_{1},\dotsc,s_{d}))\mid{T},[X_{1}\mapsto
s_{1},\dotsc,X_{d}\mapsto s_{d}]\models\varphi\\}$. Let $k\geq 0$. The
complexity class $k$-EXPTIME is defined as
$\mathit{DTIME}(2^{n^{\mathcal{O}(1)}}_{k})$ where $2^{m}_{0}:=m$ and
$2^{m}_{k+1}:=2^{2^{m}_{k}}$. Note that $0$-EXPTIME equals P.

For a complexity class $\mathcal{C}$, a $\mathcal{C}$-query is one that can be
decided within the resource bounds given by $\mathcal{C}$. We write
$\mathcal{C}\\!\\!{/}\\!_{\sim}$ for the complexity class of
$\mathcal{C}$-queries that are bisimulation-invariant.

We say that a logic $\mathcal{L}$ _captures_ a complexity class $\mathcal{C}$
if the model checking problem for $\mathcal{L}$ is in $\mathcal{C}$ and each
$\mathcal{C}$-query can be expressed in $\mathcal{L}$.

The Immerman-Vardi Theorem characterises the P-queries _over ordered
structures_ as those expressible in $\textsf{HO}^{1}\textsf{(LFP)}$, resp.
first-order logic with least fixpoints. It’s generalisation is the following:

######  Proposition 4 ([9, 21, 10, 7]).

For each $k\geq 0$, $\textsf{HO}^{k+1}\textsf{(LFP)}$ captures $k$-EXPTIME
over the class of ordered structures.

The ordering is only important for the case of $k=0$ as such an ordering can
be defined in second-order logic, i.e. as soon as $k\geq 1$. It is an open
problem whether a logic exists that captures P over the class of all
structures (cf. e.g. [8]).

The first capturing result for a bisimulation-invariant class is given by
Otto’s Theorem.

######  Proposition 5 ([18]).

The polyadic modal $\mu$-calculus $\mathcal{L}_{\mu}^{\omega}$, or,
equivalently $\text{PHFL}^{0}$, captures $\textsf{P}\\!\\!{/}\\!_{\sim}$, or
equivalently, 0$-\textsf{EXPTIME}\\!\\!{/}\\!_{\sim}$.

We give a quick sketch of its proof in order to prepare for the technical
developments in Sects. 4 and 5. The model checking problem for
$\text{PHFL}^{0}$ is readily seen to be in P (see also [15]). The interesting
part is to show that every bisimulation-invarariant P query can be expressed
in $\text{PHFL}^{0}$. In principle, this could be done by encoding runs of
polynomially time-bounded Turing machines, but it is not immediately clear how
bisimulation-invariance of the query in question can be used. Instead, the
proof for this rests on a key observation: non-bisimilarity of two states can
be expressed in $\text{PHFL}^{0}_{2}$ by a least-fixpoint formula, since
bisimilarity can be defined via the greatest fixpoint formula in Ex. 2. Hence,
non-bisimilarity of two states, as a least fixpoint, has a well-founded
reason, i.e. one that can be found in finitely many fixpoint unfoldings.
Ordering the atomic types in an arbitrary way entails a total order on the
bisimulation-equivalence classes, and this order can be defined in
$\text{PHFL}^{0}_{2}$. Hence, the LTS in question is ordered, and the
Immerman-Vardi Theorem is available, whence the problem reduces to showing
that every query defined by a bisimulation-invariant
$\textsf{HO}^{1}\textsf{(LFP)}$-query can be expressed equivalently in
$\text{PHFL}^{0}$.

This latter reduction now follows from a rather straightforward translation
from $\textsf{HO}^{1}\textsf{(LFP)}$ formulas to $\text{PHFL}^{0}$ formulas.
Variables of type $\odot$ are emulated through polyadicity and variables of
type $(\odot,\dotsc,\odot)$ are represented as order-$0$
$\text{PHFL}^{0}$-variables. Since, in the bisimulation-invariant setting, one
can always assume that the LTS in question already is its own bisimulation
quotient, bisimilarity and equality coincide. Hence, a subformula of the form
$a(X_{i},X_{j})$ can be replaced by the statement that the $i$th component of
the relation defined has an $a$-successor that is bisimilar and, hence equal
to the $j$th component. Moreover, since all states in such a bisimulation
quotient of a pointed LTS are reachable from a distinguished state,
existential quantification can be replaced by reachability of a suitable
state. It remains to translate least fixpoints in
$\textsf{HO}^{1}\textsf{(LFP)}$ into order-$0$ fixpoints of $\text{PHFL}^{0}$.

Using reasoning along similar lines, Otto’s Theorem has also been generalised
by one order.

######  Proposition 6 ([16]).

$\text{PHFL}^{1}$ captures $\textsf{EXPTIME}\\!\\!{/}\\!_{\sim}$.

##  3 Upper Bounds

Capturing a complexity class $\mathcal{C}$, defined by some restricted
resource consumption, by a logic $\mathcal{L}$ contains two parts: what is
commonly seen as the lower bound consists of showing that every query which
can be evaluated in complexity $\mathcal{C}$ can also be defined in the logic
$\mathcal{L}$. The upper bound is established by showing the contrary. This is
relatively easy as it suffices to show that queries definable in $\mathcal{L}$
can be evaluated in complexity $\mathcal{C}$, in other words that the model
checking problem for $\mathcal{L}$ belongs to class $\mathcal{C}$.

Here we do this for the fragments of PHFL of arbitrary but fixed arity $d$ and
arbitrary order $k$, w.r.t. the classes $k$-EXPTIME of the exponential time
hierarchy. We do so by extending the reduction of the model checking problem
for a polyadic logic to that of its monadic fragment [15]. Note that
$\text{PHFL}^{k}_{1}$ equals $\text{HFL}^{k}$ – the fragment of (non-polyadic)
Higher-Order Fixpoint Logic of formulas of type order at most $k$. The
complexity of model checking such fragments is known:

######  Proposition 7 ([4]).

Let $k\geq 1$. The model checking problem for $\text{HFL}^{k}$ is $k$-EXPTIME-
complete.

The corresponding result for $\text{PHFL}^{k}_{d}$, first stated without proof
in [16], follows via a reduction:

######  Theorem 8.

Let $k,d\geq 1$. The model checking problem for $\text{PHFL}^{k}_{d}$ is in
$k$-EXPTIME.

###### Proof.

By a polynomial reduction to the model checking problem for HFL. Let $k,d\geq
1$ and an LTS ${T}=({S},\\{\mathop{{\hbox{{$\mathrel{\mathop{\hbox
to10.70013pt{\rightarrowfill}}\limits^{a}}$}}}}\\}_{a\in\mathbf{A}},\ell)$
over $\mathbf{A}$ and $\mathbf{P}$ be given. We construct its $d$-product
${T}^{d}$ over the action set $\mathbf{A}^{d}:=\\{a_{i}\mid
a\in\mathbf{A},i\in[d]\\}\cup\\{\sigma\mid\sigma:[d]\to[d]\\}$ and atomic
propositions $\mathbf{P}^{d}:=\\{q_{i}\mid q\in\mathbf{P},i\in[d]\\}$ as
$({S}^{d},\\{\mathop{{\hbox{{$\mathrel{\mathop{\hbox
to11.0007pt{\rightarrowfill}}\limits^{x}}$}}}}\\}_{x\in\mathbf{A}^{\prime}_{d}},\ell^{\prime})$
where, for all $q\in\mathbf{P}$, $i\in[d]$, $a\in\mathbf{A}$,
$s_{1},\ldots,s_{d},t_{1},\ldots,t_{d}\in{S}$ we have

  * •

$q_{i}\in\ell^{\prime}(s_{1},\ldots,s_{d})$ iff $q\in\ell(s_{i})$,

  * •

$(s_{1},\ldots,s_{d})\mathop{{\hbox{{$\mathrel{\mathop{\hbox
to12.07819pt{\rightarrowfill}}\limits^{a_{i}}}$}}}}(t_{1},\ldots,t_{d})$ iff
$s_{i}\mathop{{\hbox{{$\mathrel{\mathop{\hbox
to10.70013pt{\rightarrowfill}}\limits^{a}}$}}}}t_{i}$ and $t_{j}=s_{j}$ for
all $j\neq i$,

  * •

$(s_{1},\ldots,s_{d})\mathop{{\hbox{{$\mathrel{\mathop{\hbox
to10.99991pt{\rightarrowfill}}\limits^{\sigma}}$}}}}(t_{1},\ldots,t_{d})$ iff
$t_{j}=\sigma(s_{j})$ for all $j\in[d]$.

Next, we translate a $\text{PHFL}^{k}_{d}$ formula $\varphi$ inductively into
a $\text{PHFL}_{1}$ formula $\widehat{\varphi}$ as follows. The operation
$\widehat{\cdot}$ acts homomorphically on all operators apart from the
following three cases.

$\widehat{\\{\sigma\\}\psi}:=\langle\sigma\rangle\widehat{\psi}\enspace,\quad\widehat{\langle
a_{i}\rangle\psi}:=\langle
a_{i}\rangle\widehat{\psi}\enspace,\quad\widehat{p_{i}}:=p_{i}\ .$

The latter two cases may be confusing as $\widehat{\cdot}$ seems to not change
those operators either. However, in e.g. the second case, $\langle
a_{i}\rangle$ on the left side is a polyadic modality combining the action
$a\in\mathbf{A}$ with the index $i\in[d]$. On the right side, $\langle
a_{i}\rangle$ is a monadic modality over the action $a_{i}\in\mathbf{A}^{d}$.
Likewise in the third case.

This equality in syntax for two technically different modal operators, resp.
atomic formulas is intended because of the following connection: the $d$-tuple
$(s_{1},\ldots,s_{d})$ of states in ${T}$ satisfies the $\text{PHFL}_{d}$
formula $\langle a_{i}\rangle\psi$ iff the state $(s_{1},\ldots,s_{d})$ of
${T}^{d}$ satisfies the $\text{PHFL}_{1}$ formula $\langle
a_{i}\rangle\widehat{\psi}$. A similar statement can be made for atomic
propositions and these can easily be generalised to show by induction on the
syntax of PHFL that for all $\text{PHFL}_{d}$ formulas $\varphi$, all
$s_{1},\ldots,s_{d}\in{S}$ and all environments $\eta$ we have:
$(s_{1},\ldots,s_{d})\in\llbracket\varphi\rrbracket^{{T}}_{\eta}$ iff
$(s_{1},\ldots,s_{d})\in\llbracket\widehat{\varphi}\rrbracket^{{T}^{d}}_{\eta}$.

This establishes correctness of the reduction. Note that $\widehat{\varphi}$
is a $\text{PHFL}^{k}_{1}$-, i.e. $\text{HFL}^{k}$ formula whenever
$\varphi\in\text{PHFL}^{k}_{d}$. Moreover, both ${T}^{d}$ and
$\widehat{\varphi}$ are easily seen to be constructible in polynomial time
(for fixed $d$). Thus, by Prop. 7 model checking $\text{PHFL}^{k}_{d}$ is also
in $k$-EXPTIME. ∎

##  4 Higher-Order Quantification

To show that every bisimulation-invariant $k$-EXPTIME query can be expressed
in $\text{PHFL}^{k}$ it suffices, due to Prop. 4, to show that every
$\textsf{HO}^{k+1}\textsf{(LFP)}$-query can be translated into a
$\text{PHFL}^{k}$ formula. The main challenge here is to deal with existential
quantification, which has no obvious equivalent in PHFL. In [18], first-order
existential quantification is replaced by reachability of a suitable state,
which is sufficient in the bisimulation-invariant setting. Higher-order
quantification does not have such an obvious correspondent - there is no
notion of a set, or a set of sets, etc. being reachable. Moreover, PHFL does
only have a type for sets of tuples of states, not for sets of sets etc. We
solve this problem by replacing higher-order types by a variant of their
characteristic function, something that fits quite naturally into the PHFL
world. We then lift the order on the states inherited from [18] to sets of
tuples of states and then to said characteristic functions by ordering them
lexicographically. We can enumerate sets, functions and so on alongside this
order, and hence, we can mimic existential quantification over some HO(LFP)
type by an enumeration of corresponding characteristic functions.

The increased complexity of this approach compared to simple reachability
requires two adaptations: first, since we use the order of sets, functions
etc. present in the bisimulation-invariant setting, we often have to compare
two such objects w.r.t. this order. Comparing e.g. two sets of $d$-ary tuples,
however, requires a formula containing types of width $2d$. Also,
HO(LFP)-formulas can define a query of some width, yet contain types, resp.
quantification over objects of much higher width. Hence, in order to keep the
presentation simple, the formulas we develop subsequently will be of some
unspecified, yet generally quite high arity, i.e. they will be in
$\text{PHFL}^{k}_{d}$ for some $d$ that is large compared with the width of
the original query. The exact value of $d$ will be given towards the end of
the translation.

Since we have already agreed to blow up the width used in our translated
formulas, we can also make things easier by reserving certain positions in the
tuples we work with for special tasks. We generally use the last two positions
in our tuples (those with indices $d$ and $d-1$) to compare individual states
w.r.t. the order from [18], and we will use the next $r$ positions from the
right, i.e. those with indices $d-r-1,\dotsc,d-2$ for some $r$, to keep copies
of states such that the whole LTS is reachable from at least one of these
states, in order to keep the pattern for first-order quantification valid.
This will be made formal after we revisit the pattern for existential
quantification just below. We then subsequently expand quantification towards
sets and characteristic functions. The final translation is then given in Sec.
5.

#### Reachable States.

In [18], existential quantification of first-order logic was replaced by
reachability of a suitable state in the LTS in question, using the pattern
given subsequently. First, we recall the role of the substitution operator:
Let $\sigma^{i\leftarrow j}$ be defined by $\sigma^{i\leftarrow j}(i)=j$ and
$\sigma^{i\leftarrow j}(i^{\prime})=i^{\prime}$ if $i^{\prime}\not=i$. Then
$(\overline{s}\in\llbracket\\{\sigma^{i\leftarrow
j}\\}\varphi\rrbracket^{{T}}_{\eta}$ iff
$\overline{s}[s_{j}/i]=(s_{1},\dotsc,s_{i-1},s_{j},s_{i+1},\dotsc,s_{d})\in\llbracket\varphi\rrbracket^{{T}}_{\eta}$
for all ${T}$ and $\eta$.

Now let $\mathbf{A}$ be a set of actions, let $d>2$, $r\leq d-2$ and $i\leq
d-r-2$. Recall that, for the time being, we assume that every tuple we work
with is such that all states in an LTS are reachable from one of the states at
indices $d-r-1,\dotsc,d-2$ of the tuple and that we reserve the last two
positions for comparisons (see below). Consider the formula

$\exists_{i}\varphi\coloneqq\bigvee_{j=d-r-1}^{d-2}\\{\sigma^{i\leftarrow
j}\\}\big{(}\mu(X\colon\bullet).\ \varphi\vee\bigvee_{a\in\mathbf{A}}\langle
a_{i}\rangle X\big{)}.$

for some $\varphi\in\text{PHFL}_{d}$. We have the following:

######  Observation 9.

Let ${T}$ be an LTS over $\mathbf{A}$ and let $s=(s_{1},\dotsc,s_{d})$ such
that all states in ${T}$ are reachable from at least one state in
$s_{d-r-1},\dotsc,s_{d-2}$. Then ${T},\overline{s}\models\exists_{i}\varphi$
iff there is a state $t$ in ${T}$ such that
${T},\overline{s}[t/i]\models\varphi$.

As said before, quantification over higher-order types is more complicated,
but we can replace reachability by enumeration in lexicographical order for
higher-order types. Towards this, note that for all $d\geq 2$ there is some
$\text{PHFL}^{0}_{2}$-formula $\varphi_{<}$ defining a transitive and
irreflexive relation $<$ such that, for all LTS ${T}$ and $d$-tuples
$\overline{s}=(s_{1},\dotsc,s_{d})$ we have that
${T},\overline{s}\models\varphi_{<}$ iff $s_{d-1}<s_{d}$. This formula is
defined in [18] using a variant of the negation of the formula from Ex. 2. The
actual position of the tuple elements that are compared is not important, we
choose to fix it here for consistency.

A crucial ingredient for the correctness of the quantification pattern above
is that every state in the LTS is reachable from the states in positions
$d-r-1,\dotsc,d-2$. For the first-order case, this can be guaranteed by never
manipulating the components with the respective indices. In the higher-order
setting, this does not suffice as one deals with arbitrary sets, functions,
etc. Hence, for the remainder of the section all formulas are assumed to have
a free lambda variable $e$ of type $\bullet$ that is as follows:

######  Definition 10.

Let ${T}$ be an LTS and let $r$ be fixed. Then an interpretation $\eta$ is
_good_ if $\eta(e)$ is a set of the form
$M\times\\{s_{d-r-1}\\}\times\dotsb\times\\{s_{d-2}\\}\times{S}^{2}$ such that
$\emptyset\not=M\subseteq{S}^{d-2-r}$ and each state of ${T}$ is reachable
from one of the $s_{d-r-1},\dotsc,s_{d-2}$.

We do not make this free variable explicit, since it is always assumed to be
there. We will see in Sect. 5 how this intended interpretation can be
enforced. This stipulation formalises the informal idea given above. Note that
in [18], it was assumed that all states of the LTS in question are reachable
from a singular state, but this is not a necessary requirement for the
argument to work.

Finally, let $w$ and $d$ be such that $2w+r+2\leq d$. The intuition here is
that, in order to translate from HO(LFP), we will have to deal with sets and
higher-order sets of arity at most $w$.

#### Quantification for Sets.

We now define a similar pattern to that for the first-order case which allows
us to iterate over all sets of $w$-tuples in an LTS. This is not the same as
enumerating $\llbracket\bullet\rrbracket^{{T}}$ since $w<d$.

Let $\sigma_{i}$ be defined via $\sigma_{i}(d-1)=i$, $\sigma_{i}(d)=i+w$ and
$\sigma_{i}(j)=j$ if $j<d-1$. Then
$\overline{s}\in\llbracket\\{\sigma_{i}\\}\varphi\rrbracket^{{T}}_{\eta}$ iff
$\overline{s}[s_{i}/d-1,s_{i+w}/d]\in\llbracket\varphi\rrbracket^{{T}}_{\eta}$.
The intended use for this substitution is to compare the elements at indices
$i$ and $i+w$ w.r.t. to the order induced by $\varphi_{<}$. Remember that this
formula always compares the last two elements of the tuple. Moreover, let
$\sigma_{\rightarrow w}$ be defined by $\sigma_{\rightarrow w}(i)=w+i$ for
$i\leq w$ and $\sigma_{\rightarrow w}(j)=j$ for $j>w$. Then
$(s_{1},\dotsc,s_{d})\in\llbracket\\{\sigma_{\rightarrow
w}\\}\varphi\rrbracket^{{T}}_{\eta}$ iff
$(s_{1},\dotsc,s_{w},s_{1},\dotsc,s_{w},s_{2w+1},\dotsc,s_{d})\in\llbracket\varphi\rrbracket^{{T}}_{\eta}$.
The intended use here is to shift the first $w$ elements of a formula to the
right to make room for another tuple at the first $w$ positions such that the
two tuples can be compared lexicographically.

Consider the formula
$\exists^{(w)}x.\varphi\coloneqq\big{(}\mu(F\colon\bullet\to\bullet).\,\lambda(x\colon\bullet).\,\varphi\vee
F(\mathit{next}^{(w)}(x))\big{)}\mathtt{f\\!f}$ where

$\displaystyle\varphi_{<}^{w}$
$\displaystyle\coloneqq\bigvee_{i=1}^{w}\\{\sigma_{i}\\}\varphi_{<}\wedge\bigwedge_{j=1}^{i-1}\\{\sigma_{j}\\}\neg\varphi_{<}$
$\displaystyle\varphi_{<}^{(w)}(x,y)$
$\displaystyle\coloneqq\exists_{1}\dotsc\exists_{w}.\ y\wedge\neg
x\wedge\\{\sigma_{\rightarrow
w}\\}\big{(}\forall_{1}\dotsc\forall_{w}.\varphi_{<}^{w}\rightarrow
x\rightarrow y\big{)}.$ $\displaystyle\mathit{next}^{(w)}(x)$
$\displaystyle\coloneqq\lambda(x\colon\bullet).\ e\wedge\neg
x\wedge\\{\sigma_{\rightarrow w}\\}\big{(}\forall_{1}\dotsc\forall_{w}.\
\varphi_{<}^{w}\rightarrow x\big{)}$ $\displaystyle\qquad\qquad\;\;\;\;\vee
e\wedge x\wedge\\{\sigma_{\rightarrow
w}\\}\big{(}\exists_{1}\dotsc\exists_{w}.\ \varphi_{<}^{w}\wedge\neg x\big{)}$

The first formula $\varphi_{<}^{w}$ implements lexicographical comparison of
the first $w$ elements in a tuple to the second $w$ elements. The second
formula $\varphi_{<}^{(w)}$ lifts the order from tuples to sets of tuples via
the lexicographical order induced by the order on the tuples. Finally, the
formula $\mathit{next}^{(w)}$ is a predicate transformer that consumes a set
of tuples. It returns a set of tuples that is the lexicographical successor of
the input in the order induced by the order on the first $w$ elements of the
individual tuples: the output contains a tuple iff either the input does
contain it, but not all lexicographically smaller tuples, or if the input does
not contain it, but all lexicographically smaller tuples. Also note the role
of $e$ that filters out all tuples that do not adhere to our stipulation that
the whole LTS be reachable from one of the states at indices
$d-r-1,\dotsc,d-2$.

######  Lemma 11.

Let ${T}$ be an LTS with state set ${S}$ and let $\eta$ be good. Then
${T},\overline{s}\models_{\eta}\exists^{(w)}x.\,\varphi$ iff there is
$M\subseteq{S}^{w}$ such that ${T},\overline{s}\models_{\eta[x\mapsto
M\times{S}^{d-w}\cap\eta(e)]}\varphi$.

The proof consists of verifying the informal intuition above. We write
$\forall^{(w)}x.\ \varphi$ to denote $\neg\exists^{(w)}x.\ \neg\varphi$. We
write $\exists^{(w)}x_{1},\dotsc,x_{n}.\ \varphi$ for
$\exists^{(w)}x_{1}\dotsb\exists^{(w)}x_{n}.\ \varphi$, and similarly for
$\forall^{(w)}x.\ \varphi$.

#### Generalised Higher-Order Quantification.

We have just seen how existential quantification can be emulated for
individual states in an LTS and, with some restrictions, for sets of
$w$-tuples of an LTS. For other types that commonly appear in HO(LFP), i.e.
relations of higher order, there is no immediate PHFL equivalent, since all
types beyond $\bullet$ are function types. However, we can use these function
types to emulate the HO(LFP) types to a sufficient degree. For the sake of
simplicity, we only consider types of a special form; we argue in Sect. 5 why
this is not a restriction.

Let $\tau_{w,k}$ be inductively defined via $\tau_{w,0}=\bullet$ and
$\tau_{w,i+1}=\tau_{w,i}\to\dotsb\to\tau_{w,i}\to\bullet$ where $\tau_{w,i}$
is repeated $w$ many times. Given ${T}$, let
$\llbracket\tau^{\circ}_{w,i}\rrbracket^{{T}}=\llbracket\tau_{w,i}\rrbracket^{{T}}$
for $i\leq 1$ and let

$\llbracket\tau^{\circ}_{w,k}\rrbracket^{{T}}=\\{f\in\llbracket\tau_{w,k}\rrbracket^{{T}}\mid
f(f_{1},\dotsc,f_{w})={S}\text{ or }f(f_{1},\dotsc,f_{w})=\emptyset\text{
f.a.\ }f_{1},\dotsc,f_{w}\in\llbracket\tau^{\circ}_{w,k-1}\rrbracket^{{T}}\\}$

for $k\geq 2$. The important distinction here is that
$\llbracket\tau^{\circ}_{w,k}\rrbracket^{{T}}$ is the restriction of
$\llbracket\tau_{w,k}\rrbracket^{{T}}$ to those functions that always return
either the full set of states or the empty set, at least on inputs from
$\llbracket\tau^{\circ}_{w,k-1}\rrbracket^{{T}}$. This is desirable since we
want to use functions in $\llbracket\tau^{\circ}_{w,k}\rrbracket^{{T}}$ to
emulate higher-order variables of a special form. Given $x,x_{1},\dotsc,x_{w}$
of the appropriate type, the question whether $\overline{s}\in\llbracket
x(x_{1},\dotsc,x_{w})\rrbracket^{{T}}_{\eta}$ does not depend on
$\overline{s}$ (as in modal logics), but is uniform over the while LTS.
However, since $\llbracket\tau_{w,k}\rrbracket^{{T}}$ also contains functions
that are not uniform starting from PHFL-order $2$, we restrict ourselves to
functions that are uniform on the necessary inputs (i.e. those that are
themselves sufficiently uniform).

Consider the following formulas for $k\geq 1$, where
$\overline{x}=x_{1},\dotsc,x_{w}$ and $\overline{y}=y_{1},\dotsc,y_{w}$:

$\displaystyle\varphi_{<}^{w,k-1}(x_{1},\dotsc,x_{w},y_{1},\dotsc,y_{w})$
$\displaystyle\coloneqq\bigvee_{i=1}^{w}\varphi_{<}^{(w),k-1}(x_{i},y_{i})\wedge\bigwedge_{j=1}^{i-1}\neg\varphi_{<}^{(w),k-1}(x_{j},y_{j})$
$\displaystyle\varphi_{<}^{(w),k}(x,y)$
$\displaystyle\coloneqq\exists^{w,k-1}\overline{x}.\ y(\overline{x})\wedge\neg
x(\overline{x})$ $\displaystyle\;\wedge\forall^{w,k-1}\overline{y}.\
\varphi_{<}^{w,l}(\overline{y},\overline{x})\rightarrow
x(\overline{y})\rightarrow y(\overline{y})$
$\displaystyle\mathtt{f\\!f}_{(w),k}$
$\displaystyle\coloneqq\lambda(\overline{x}\colon\tau_{w,k-1}).\,\mathtt{f\\!f}$
$\displaystyle\mathit{next}^{w,k}(x)$
$\displaystyle\coloneqq\lambda(x\colon\tau_{w,k}).\
\lambda(\overline{x}\colon\tau_{w,k-1}).\ $ $\displaystyle\big{(}\neg
x(\overline{x})\wedge\forall^{w,k}\overline{y}.\
\varphi_{<}^{w,k}(\overline{y},\overline{x})\rightarrow
x(\overline{y})\big{)}$
$\displaystyle\vee\big{(}x(\overline{x})\wedge\exists^{w,k}\overline{y}.\
\varphi_{<}^{w,k}(\overline{y},\overline{x})\wedge\neg x(\overline{y})\big{)}$
$\displaystyle\exists^{w,k}(x).\ \varphi$
$\displaystyle\coloneqq\big{(}\mu(F\colon\tau_{w,k}\to\tau_{w,k}).\
\lambda(x\colon\tau_{w,k}).\,\varphi\vee
F(\mathit{next}^{w,k}x)\big{)}\,\mathtt{f\\!f}_{(w),k}$

where $\varphi_{<}^{(w),k-1}=\varphi_{<}^{(w)}$ in case $k=1$ and
$\exists^{w,k-1}x.\varphi=\exists^{(w)}x.\varphi$ if $k=1$.

Similarly as in the definitions given before Lemma 11, these formulas lift
quantification up by one level on the type hierarchy. The formula
$\varphi_{<}^{w,k-1}$ compares width-$w$-tuples of functions of type
$\tau^{\circ}_{w,k-1}$ lexicographically using the previously defined formula
$\varphi_{<}^{(w),k-1}$ that compares individual such functions. The formula
$\varphi_{<}^{(w),k}$ then lifts this to individual functions of the next
type, using existential and universal quantification. The formula
$\mathit{next}^{w,k}$ again consumes a function of type $\tau^{\circ}_{w,k}$
and returns the lexicographically next one using the standard definition of
binary incrementation, while $\exists^{w,k}$ implements existential
quantification for $\tau^{\circ}_{w,k}$ by iterating through all possible
candidates using $\mathit{next}^{w,k}$.

######  Lemma 12.

Let ${T}$ be an LTS and let $\eta$ be good. Then
${T},\overline{s}\models_{\eta}\exists^{w,k}x.\,\varphi$ iff there is
$f\in\llbracket\tau^{\circ}_{w,k}\rrbracket^{{T}}$ such that
${T},\overline{s}\models_{\eta[x\mapsto f]}\varphi$.

The proof follows the same pattern as that of Lemma 11 by verifying that the
individual formulas do what is claimed above.

Lemmas 11 and 12 justify the use of HO(LFP)-style quantification symbols for
individual states, sets of type $M\times{S}^{d-w}\cap\eta(e)$ for
$M\subseteq{S}^{s}$ and for $\tau^{\circ}_{w,k}$ for all $k\geq 2$. Note that
the latter do neither coincide with HO(LFP) types nor with the respective
$\tau_{w,k}$.

##  5 Lower Bounds

#### Homogeneous Types.

In order to simplify the translation from HO(LFP) to PHFL, we restrict the set
of types that can be used in HO(LFP) formulas. Let $w\geq 2$ be fixed but
arbitrary. Define $\tau^{\prime}_{w,k}$ as $\tau^{\prime}_{w,1}=\odot$,
$\tau^{\prime}_{w,i+1}=(\tau^{\prime}_{w,i},\dotsc,\tau^{\prime}_{w,i})$ with
$w$ many repetitions of $\tau^{\prime}_{w,i}$.

######  Lemma 13.

If $\varphi\in\textsf{HO}^{k}\textsf{(LFP)}$ defines a query $Q$, then there
is $\varphi^{\prime}\in\textsf{HO}^{k}\textsf{(LFP)}$ that defines the same
query, but the only types used in $\varphi^{\prime}$ are
$\tau^{\prime}_{w,0},\dotsc,\tau^{\prime}_{w,k}$ for some $w$.

###### Proof.

There are two principles that are used here: If $\varphi$ contains a type of
the form $\tau^{\prime\prime}=(\tau^{\prime},\dotsc,\tau^{\prime})$ with
$w^{\prime}\leq w$ many repetitions of $w$, we can replace
$\tau^{\prime\prime}$ by $(\tau^{\prime},\dotsc,\tau^{\prime})$ with exactly
$w$ many repetitions of $\tau^{\prime}$ by changing the respective type
everywhere in the formula and requiring at quantifiers that, e.g., the last
$w-w^{\prime}$ components are equal to the $w-w^{\prime}-1$st in every tuple
contained in a set. Hence, every type can be assumed to have width exactly
$w$.

It remains to deal with inhomogeneous types, e.g. those of the form
$(\tau^{\prime},\tau^{\prime\prime},\dotsc)$ such that
$\mathit{ord}(\tau^{\prime})\not=\mathit{ord}(\tau^{\prime\prime})$. This can
be remedied by increasing the type of the lower order by one order, and
requiring at quantification steps that the only tuple in the set be a
singleton of the form $(M,\dotsc,M)$ of width $w$. This procedure needs to be
chained if the orders of constituent types diverge by more than one. ∎

#### Type Correspondence.

Now that we can assume w.l.o.g. that all
$\textsf{HO}^{k}\textsf{(LFP)}$-definable queries are defined by an
$\textsf{HO}^{k}\textsf{(LFP)}$ formula which uses only the types
$\tau^{\prime}_{w,i}$ for $i\leq k$ we can observe that these types are quite
similar to the types $\tau_{w,k}$ defined in the previous section. In fact, we
want to emulate the type $\tau^{\prime}_{w,k}$ with $k>1$ by
$\tau^{\circ}_{w,k-2}$. The type $\tau^{\prime}_{s,1}$ will be handled by
polyadicity as in [18].222It would also be possible to completely eliminate
this type from $\textsf{HO}^{k}\textsf{(LFP)}$ for $k\geq 2$; cf. similar
constructions in the context of MSO and automata theory.

Let ${T}$ be an LTS with state set ${S}$ and let $d\geq w\geq 2$. For each
$k\geq 2$, we define a translation
$\mathit{tptr}_{k}^{{T}}\colon\llbracket\tau^{\prime}_{w,k}\rrbracket^{{T}}\to\llbracket\tau^{\circ}_{w,k-2}\rrbracket^{{T}}$
via $\mathit{tptr}^{{T}}_{2}(M)=M\times{S}^{d-w}$ and
$\mathit{tptr}^{{T}}_{i+1}(M)=f\in\llbracket\tau_{w,k-2}\rrbracket^{{T}}$ s.t.

$\displaystyle f(f_{1},\dotsc,f_{n})=\left\\{\begin{aligned} {S},&\text{ if
}f_{j}=\mathit{tptr}^{{T}}_{i}(x_{i})\text{ f.a. }0\leq j\leq w\text{ and
}(x_{1},\dotsc,x_{w})\in M\\\ \emptyset,&\text{
otherwise.}\end{aligned}\right.$

Hence, a variable assignment $\alpha$ such that all variables are of types
$\tau^{\prime}_{w,2},\dotsc,\tau^{\prime}_{w,k}$ induces an environment
$\eta_{\alpha}$ with definitions for all those variables of order $\geq 2$ via
$\eta_{\alpha}(X)=\mathit{tptr}^{{T}}_{i}(X)$ where $i$ is the order of $X$.

#### The Translation.

We are now ready to extend the translation given in [18] to
$\textsf{HO}^{k}\textsf{(LFP)}$ with $k\geq 2$. Towards this, we present a
syntactical translation $\mathit{trans}$ from $\textsf{HO}^{k}\textsf{(LFP)}$
with $k\geq 2$ into $\text{PHFL}^{d}_{k-1}$ for some $d\geq 2$.

######  Lemma 14.

Let $\varphi\in\textsf{HO}^{k}\textsf{(LFP)}$ be bisimulation invariant and
have free first-order variables $X_{1},\dotsc,X_{r}$ and, hence define a query
of width $r$. Moreover, let $\tau^{\prime}_{w,0},\dotsc,\tau^{\prime}_{w,k}$
be the only types in $\varphi$. W.l.o.g. let $2w\geq r$. Let $d=2w+r+2$. Then
there is $\varphi^{\prime}\in\text{PHFL}^{d}_{k-1}$ such that, for all LTS
${T}$ that are a bisimulation quotient, we have ${T},\alpha\models\varphi$ iff
${T},(\alpha(X_{1}),\dotsc,\alpha(X_{r}))\models_{\eta_{\alpha}[e\mapsto
M]}\varphi^{\prime}$ where $\emptyset\not=M^{\prime}\subseteq{S}^{r}$ and
$M=M^{\prime}\times{S}^{d-2r-2}\times\\{\alpha(X_{1})\\}\times\dotsb\times\\{\alpha(X_{r})\\}\times{S}^{2}$.

###### Proof.

Let $\mathit{trans}$ be given via

$\displaystyle\mathit{trans}(p(X_{i}))$ $\displaystyle\coloneqq p_{i}$
$\displaystyle\mathit{trans}(a(X_{i},X_{j}))$ $\displaystyle\coloneqq\langle
a_{i}\rangle\\{\sigma_{i,j}\\}\varphi_{\sim}$
$\displaystyle\mathit{trans}(\varphi_{1}\vee\varphi_{2})$
$\displaystyle\coloneqq\mathit{trans}(\varphi_{1})\vee\mathit{trans}(\varphi_{2})$
$\displaystyle\mathit{trans}(\neg\varphi)$
$\displaystyle\coloneqq\neg\mathit{trans}(\varphi)$
$\displaystyle\mathit{trans}(\exists(X_{i}\colon\odot).\ \varphi)$
$\displaystyle\coloneqq\exists_{i}.\ \mathit{trans}(\varphi)$
$\displaystyle\mathit{trans}(\exists(X\colon\tau^{\prime}_{w,1}).\,\varphi)$
$\displaystyle\coloneqq\exists^{(w)}(x).\ \mathit{trans}(\varphi)$
$\displaystyle\mathit{trans}(\exists(X\colon\tau^{\prime}_{w,k}).\ \varphi)$
$\displaystyle\coloneqq\exists^{w,k}(x).\ \mathit{trans}(\varphi)\text{ if
}k\geq 2$ $\displaystyle\mathit{trans}(X(X_{i_{1}},\dotsc,X_{i_{w}}))$
$\displaystyle\coloneqq\\{\sigma\\}x\text{ if }(X\colon\tau^{\prime}_{w,1})$
$\displaystyle\mathit{trans}(X(X_{1},\dotsc,X_{w}))$ $\displaystyle\coloneqq
x(x_{1},\dotsc,x_{w})\text{ if }(X\colon\tau^{\prime}_{w,k})\text{ and }k\geq
2$ $\displaystyle\mathit{trans}(\big{(}\mathit{lfp}(X,Y_{1},\dotsc,Y_{w}).\
\varphi\big{)}(Z_{i_{1}},\dotsc,Z_{i_{w}}))$
$\displaystyle\coloneqq\\{\sigma\\}\mu(F\colon\bullet\to\bullet).\
\mathit{trans}(\varphi)\text{ if }(X\colon\tau_{w,2})$
$\displaystyle\mathit{trans}(\big{(}\mathit{lfp}(X,Y_{1},\dotsc,Y_{w}).\
\varphi\big{)}(Z_{1},\dotsc,Z_{w}))$
$\displaystyle\coloneqq\big{(}\mu(F\colon\tau_{w,k-2}\to\tau_{w,k-2}).\
\lambda(y_{1},\dotsc,y_{w}\colon\tau_{w,k-3}).\ $
$\displaystyle\qquad\qquad\qquad\quad\mathit{trans}(\varphi)\big{)}(Z_{1},\dotsc,Z_{w})\text{
if }(X\colon\tau_{w,k})\text{ and }k\geq 3$

where $\sigma_{i,j}$ is defined via $\sigma_{i,j}(d-1)=i,\sigma_{i,j}(d)=j$
and $\sigma_{i,j}(k)=k$ for $k<d-1$, and $\varphi_{\sim}$ is the formula from
Ex. 2, resp. [18] that holds iff the states in positions $d-1$ and $d$ are
bisimilar, and, finally $\sigma$ is defined via $\sigma(j)=i_{j}$ for $0\leq
j\leq w$ and $\sigma(k)=k$ for $k\geq w$. The substitions $\sigma_{i,j}$,
resp. $\sigma$ serve to swap the elements $i$ and $j$ to positions $d-1$ and
$d$, resp. to reorder the elemtents according to the variable order used on
the left side of the translation.¸

The claim now follows by induction over the syntax tree of $\varphi$. The
first five cases are as in [18]. The next four cases are by Lemmas 11 and 12,
resp. the definition of $\eta_{\alpha}$. The fixpoint cases are by an
induction over the individual stages of the fixpoint iteration; note that the
Knaster-Tarski-based semantics of the fixpoints in HO(LFP) and PHFL can be
equivalently replaced by semantics based on the Kleene Fixpoint Theorem [11].
This mirrors the proof of the fixpoint case in [18]. ∎

######  Theorem 15.

$\text{PHFL}^{k}$ captures k-EXPTIME $\\!\\!{/}\\!_{\sim}$ for all $k\geq 0$.

###### Proof.

The cases of $k=0$ and $k=1$ are of course already known [18, 16]. For $k\geq
2$, the upper bound is shown in Thm. 8. For the lower bound, it suffices, due
to Prop. 4, to show that for any bisimulation-invariant query defined by an
$\textsf{HO}^{k+1}\textsf{(LFP)}$ formula there is an equivalent formula in
$\text{PHFL}^{k}$. Let $\varphi$ be a formula defining such a query $Q$ of
width $r\geq 1$, and w.l.o.g. $\varphi$ contains only the types
$\tau_{w,0},\dotsc,\tau_{w,k}$.

Let $\varphi^{\prime}$ be the formula obtained from the translation in Lemma
14 and let $\sigma$ be defined via $\sigma(d-r-2+i)=i$ for $1\leq i\leq r$,
and $\sigma(j)=j$ for $j\leq d-r-2$ or $j\geq d-1$. Note that $\sigma$ simply
copies the first $r$ many states in a tuple to the positions
$d-r-1,\dotsc,d-2$ where they serve to retain goodness (cf. Def. 10). Then
$\psi=(\lambda(e\colon\bullet)\varphi)\\{\sigma\\}\mathtt{t\\!t}$ defines the
query $\\{({T},(s_{1},\dotsc,s_{d}))\mid({T},(s_{1},\dotsc,s_{r}))\in Q\\}$.
Towards this, note that
$\llbracket\\{\sigma\\}\mathtt{t\\!t}\rrbracket^{{T}}=\\{(s_{1},\dotsc,s_{d})\mid
s_{i}=s_{d-r-2+i}\text{ for }1\leq i\leq r\\}=M$. Hence,
$\llbracket\psi\rrbracket^{{T}}=\llbracket\varphi^{\prime}\rrbracket^{{T}}_{\eta}$
where $\eta=\emptyset[e\mapsto M]$. Since $\eta$ is good, Lemma 14 is
applicable.

What remains is to argue that a query that, on each LTS ${T}$, returns all
tuples in $M\times{S}^{d-r}$ where $M\subseteq{S}^{r}$, is in fact a query
that defines tuples of width $r$. This can either be done formally by
expanding the semantics of the substitution operator $\\{\sigma\\}$ to return
tuples in the width of its co-domain, or by simply considering queries of the
above form to be of width $r$, cf. [18]. ∎

##  6 Conclusion

We have extended the descriptive complexity of bisimulation-invariant queries,
as started by Otto [18] with the capturing of the class P
$\\!\\!{/}\\!_{\sim}$ with the logic $\mathcal{L}_{\mu}^{\omega}$, to further
time complexity classes, namely the classes $k$-EXPTIME $\\!\\!{/}\\!_{\sim}$
of bisimulation-invariant queries that can be answered in $k$-fold exponential
time. These turn out to be exactly those that can be defined in PHFL, the
polyadic extension of the higher-order modal fixpoint logic HFL. This is
genuinely an extension as $\mathcal{L}_{\mu}^{\omega}$ coincides with
$\text{PHFL}^{0}$, the fragment with no higher-order constructs. Moreover, the
level in the exponential-time hierarchy corresponds to the type order used in
formulas: $k$-EXPTIME $\\!\\!{/}\\!_{\sim}$ = $\text{PHFL}^{k}$.

PP $\\!\\!{/}\\!_{\sim}$EXPTIMEEXPTIME
$\\!\\!{/}\\!_{\sim}$$2$-EXPTIME$2$-EXPTIME
$\\!\\!{/}\\!_{\sim}$$3$-EXPTIME$3$-EXPTIME
$\\!\\!{/}\\!_{\sim}$$\vdots$$\vdots$$\text{PHFL}^{0}=\mathcal{L}_{\mu}^{\omega}$$\textsf{HO}^{2}\textsf{(LFP)}$$\text{PHFL}^{1}$$\textsf{HO}^{3}\textsf{(LFP)}$$\text{PHFL}^{2}$$\textsf{HO}^{4}\textsf{(LFP)}$$\text{PHFL}^{3}$$\vdots$$\vdots$[18][16]Thm.
15Thm. 15[10][7][7]Computational ComplexityDescriptive Complexity Figure 2:
Capturing results for time complexity classes - an overview.

The resulting picture of descriptive time complexity is shown in Fig. 2. A
natural way to extend this is of course to integrate results about the space
complexity classes $k$-EXPSPACE $\\!\\!{/}\\!_{\sim}$ sitting in between
$k$-EXPTIME $\\!\\!{/}\\!_{\sim}$ and $(k+1)$-EXPTIME $\\!\\!{/}\\!_{\sim}$.
Here we can only state that it is possible to capture these in terms of
natural fragments of PHFL as well but the proof requires a few more
ingredients than the time-complexity case. Here we could use the already known
characterisation of $k$-EXPTIME by Higher-Order Predicate Logics with Least
Fixpoints [7]. For the space complexity classes, we need to first develop such
characterisations that extend the Abiteboul-Vianu Theorem. This can be done
[14], but due to space restrictions here its detailed presentation is left for
a future publication.

A noteworthy observation for the capturing of $k$-EXPTIME
$\\!\\!{/}\\!_{\sim}$ with $k\geq 1$ is that, unlike in the case of $k=0$, the
requirement of structures being ordered is not necessary for the invocation of
the (generalised) Immerman-Vardi Theorem. However, starting from $k\geq 1$ the
order being provided in the bisimulation-invariant setting plays a crucial
role to emulate existential quantification from the HO(LFP) side: the LTS in
question coming with a $\text{PHFL}^{0}_{2}$-definable order allows us to
enumerate sufficiently many sets, functions, etc. to emulate existential
quantification. It remains to see in further detail whether this is an
artifact of the proof strategy or a genuine and inherent part of the
correspondence between complexity classes and logics in the bisimulation-
invariant framework.

## References

  * [1]
  * [2] S. Abiteboul & V. Vianu (1987): _A Transaction Language Complete for Database Update and Specification_.  In: Proc. ACM SIGACT-SIGMOD Symp. on Principles of Database Systems, San Diego, CA, pp. 260–268, 10.1145/28659.28688.
  * [3] H. R. Andersen (1994): _A Polyadic Modal $\mu$-Calculus_.  Technical Report ID-TR: 1994-195, Dept. of Computer Science, Technical University of Denmark, Copenhagen, 10.1.1.42.1859.
  * [4] R. Axelsson, M. Lange & R. Somla (2007): _The Complexity of Model Checking Higher-Order Fixpoint Logic_.  Logical Methods in Computer Science 3, pp. 1–33, 10.2168/LMCS-3(2:7)2007.
  * [5] F. Bruse, M. Lange & É. Lozes (2017): _Space-Efficient Fragments of Higher-Order Fixpoint Logic_.  In: Proc. 11th Int. Workshop on Reachability Problems, RP’17, LNCS 10506, pp. 26–41, 10.1007/978-3-319-67089-8_3.
  * [6] R. Fagin (1974): _Generalized First-Order Spectra and Polynomial-Time Recognizable Sets_.  Complexity and Computation 7, pp. 43–73.
  * [7] C. M. Freire & A. T. Martins (2011): _The Descriptive Complexity of the Deterministic Exponential Time Hierarchy_.  In: Proc. 5th Workshop on Logical and Semantic Frameworks with Applications, LSFA’10, 269, pp. 71–82, 10.1016/j.entcs.2011.03.006.
  * [8] M. Grohe (2008): _The Quest for a Logic Capturing PTIME_.  In: Proc. 23rd Annual IEEE Symp. on Logic in Computer Science, LICS’08, IEEE Computer Society, pp. 267–271, 10.1109/LICS.2008.11.
  * [9] N. Immerman (1986): _Relational Queries Computable in Polynomial Time_.  Information and Control 68(1-3), pp. 86–104, 10.1016/S0019-9958(86)80029-8.
  * [10] N. Immerman (1987): _Languages That Capture Complexity Classes_.  SIAM Journal of Computing 16(4), pp. 760–778, 10.1137/0216051.
  * [11] S. C. Kleene (1938): _On Notation for Ordinal Numbers_.  Journal of Symbolic Logic 3(4), pp. 150–155, 10.2307/2267778.
  * [12] B. Knaster (1928): _Un théorèm sur les fonctions d’ensembles_.  Annals Soc. Pol. Math 6, pp. 133–134.
  * [13] D. Kozen (1983): _Results on the Propositional $\mu$-calculus_.  Theor. Comp. Sci. 27, pp. 333–354, 10.1016/0304-3975(82)90125-6.
  * [14] D. Kronenberger (2018): _Capturing Bisimulation-Invariant Complexity Classes by Polyadic Higher-Order Fixpoint Logic_.  Master’s thesis, University of Kassel.
  * [15] M. Lange & É. Lozes (2012): _Model Checking the Higher-Dimensional Modal $\mu$-Calculus_.  In: Proc. 8th Workshop on Fixpoints in Computer Science, FICS’12, Electr. Proc. in Theor. Comp. Sc. 77, pp. 39–46, 10.4204/EPTCS.77.
  * [16] M. Lange & É. Lozes (2014): _Capturing Bisimulation-Invariant Complexity Classes with Higher-Order Modal Fixpoint Logic_.  In: Proc. 8th Int. IFIP Conf. on Theoretical Computer Science, TCS’14, LNCS 8705, Springer, pp. 90–103, 10.1007/978-3-662-44602-7.
  * [17] M. Lange, É. Lozes & M. Vargas Guzmán (2014): _Model-Checking Process Equivalences_.  Theor. Comp. Sci. 560, pp. 326–347, 10.1016/j.tcs.2014.08.020.
  * [18] M. Otto (1999): _Bisimulation-invariant PTIME and higher-dimensional $\mathrm{\mu}$-calculus_.  Theor. Comput. Sci. 224(1-2), pp. 237–265, 10.1016/S0304-3975(98)00314-4.
  * [19] A. Tarski (1955): _A Lattice-theoretical Fixpoint Theorem and its Application_.  Pacific Journal of Mathematics 5, pp. 285–309, 10.2140/pjm.1955.5.285.
  * [20] J. van Benthem & K. Doets (1983): _Higher-Order Logic_.  In D. Gabbay & F. Guenther, editors: Handbook of Philosophical Logic, Volume I: Elements of Classical Logic, D. Reidel Publishing Co., pp. 275–329, 10.1007/978-94-009-7066-3_4.
  * [21] M. Y. Vardi (1982): _The Complexity of Relational Query Languages (Extended Abstract)_.  In: Proc. 14th Symp. on Theory of Computing, STOC’82, ACM, San Francisco, CA, USA, pp. 137–146, 10.1145/800070.
  * [22] M. Viswanathan & R. Viswanathan (2004): _A Higher Order Modal Fixed Point Logic_.  In: Proc. 15th Int. Conf. on Concurrency Theory, CONCUR’04, LNCS 3170, Springer, pp. 512–528, 10.1007/978-3-540-28644-8_33.