The Complexity of Bisimilarity and Model Checking in Finitary Diagrams

Bläser, Markus; Dutta, Sagnik; Okyay, Samuel

doi:10.4230/LIPIcs.ICALP.2026.166

The Complexity of Bisimilarity and Model Checking in Finitary Diagrams

Markus Bläser

Saarland University, Saarland Informatics Campus, Saarbrücken, Germany Sagnik Dutta

Max Planck Institut für Informatik, Saarland Informatics Campus, Saarbrücken, Germany Samuel Okyay Saarland University, Saarland Informatics Campus, Saarbrücken, Germany

Abstract

Inspired by the work of Dubut, Goubault, and Goubault-Larrecq (ICALP 2015) on natural homology, Dubut (RAMiCS 2020) introduces finitary diagrams and studies bisimilarity and diagrammatic path logics for them. To this aim, he defines a fragment of the existential theory of the reals, called the existential theory of invertible matrices (ETIM). Using a PSPACE upper bound for this fragment, he proves that for finitary diagrams, bisimilarity can be decided in EXPSPACE and model checking for diagrammatic path logic in PSPACE.

We significantly improve both these bounds and settle the complexity of model checking for finitary diagrams. As our first main result, we show that there is an efficient randomized algorithm for ETIM. Combining this with the previous work by Dubut, we obtain an NEXP upper bound for bisimilarity of finitary diagrams and an NP upper bound for diagrammatic path logic. We also provide a matching NP-hardness proof for the latter. The hardness proof introduces constrained layered poset problems, which may be of independent interest, and connects them to finitary diagrams using Gabriel’s theorem for representations of path quivers. For bisimilarity over finite fields, we further improve the upper bound to PSPACE. In ETIM, we quantify over invertible matrices. We finally ask what happens if we instead quantify over matrices from the special linear group, that is, of determinant one. We show that in this case, the resulting fragment is equivalent to the existential theory of the reals, under a mild generalization of the allowed linear constraints.

Keywords and phrases:

Bisimilarity, Finitary diagrams, Model checking, Existential Theory of the Reals

Category:

Track B: Automata, Logic, Semantics, and Theory of Programming

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Logic

Editors:

Sayan Bhattacharya, Danupon Nanongkai, Michael Benedikt, and Gabriele Puppis

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

The study of behavioral equivalence in complex systems has been a central theme in concurrency theory and coalgebraic semantics. Among the most prominent notions of equivalence is bisimilarity, which provides a way to compare systems based on their observable behavior rather than their internal structure. In classical models, such as transition systems, bisimilarity relates states in such a way that every move of one system can be matched by a move of the other. Dubut, Goubault, and Goubault-Larrecq [5] proposed a categorical version of this idea in the setting of directed algebraic topology, where systems are represented not merely by states and transitions, but by diagrams with values in algebraic categories. This approach enables the comparison of systems with rich algebraic structure, including linear dynamical systems and weighted automata.

Dubut [4] introduced finitary diagrams as a finite, algebraic setting in which this categorical notion of bisimilarity can be studied algorithmically. A finitary diagram is a functor from a finite poset to a category of finite-dimensional vector spaces. While deciding the bisimilarity of two diagrams, there are two problems: first, finding out how to relate the executions and second, constructing the bisimulation, in particular, the isomorphisms. The first part is difficult in general, because this relation is necessarily infinite when there are loops. Restricting the input category to a finite poset removes this difficulty and allows us to focus on the algebraic problem of finding suitable isomorphisms between vector spaces. This makes finitary diagrams a natural setting for understanding the complexity of bisimilarity.

Dubut, Goubault, and Goubault-Larrecq [5] proposed a homology theory based on natural systems of abelian groups, meant to reflect directed structure, unlike classical homology which ignores direction. A diagram is a functor $F:C\to A$ , where $C$ is a small category and $A$ is a category of observations. Inspired by the theory in [7] of comparing transition systems, Dubut, Goubault, and Goubault-Larrecq [5] defined two diagrams $F:C\to A$ and $G:D\to A$ to be bisimilar if there is a span of open morphisms between them, i.e., a diagram $H:E\to A$ and two open morphisms from $H$ to $F$ and $H$ to $G$ , respectively. Dubut [4] studies equivalent notions of bisimilarity. He first defines the notion of bisimulation between two diagrams $F:C\to A$ and $G:D\to A$ : A bisimulation should identify pairs of elements $c\in C$ and $d\in D$ such that for any morphism $i:c\to c^{\prime}$ of $C$ , there must be a morphism $j:d\to d^{\prime}$ of $D$ and an isomorphism $g:F(c^{\prime})\to G(d^{\prime})$ satisfying the following commutativity relation (see also Figure 1)

g\circ F(i)=G(j)\circ f,

(1)

where $F(i)$ and $G(j)$ are the induced morphisms of $A$ . He shows that $F$ and $G$ are bisimilar if and only if there is a bisimulation between them. Then he goes on to show that bisimilarity can also be characterized in terms of path logics, in the spirit of [6, 7]. He defines a logic called diagrammatic path logic and proves that two diagrams are bisimilar if and only if they are logically equivalent, i.e., for every $c\in C$ , there is a $d\in D$ such that for every diagrammatic path formula $S$ , either $F, c$ and $G, d$ are both a model for $S$ or both are not.

1.1 Previous results

Finding bisimulations for finitary diagrams typically has a “combinatorial” part and an “algebraic” part. In the combinatorial part, we have to find an alignment of the objects in $C$ and $D$ whereas in the algebraic part, we need to find the isomorphisms $f$ and $g$ .

As a first tool for computing these isomorphisms, [4] introduced the existential theory of invertible matrices ( $\mathrm{ETIM}_{\mathbb{R}})$ . It contains sentences of the form

\exists_{n_{1}}X_{1}\exists_{n_{2}}X_{2}\dots\exists_{n_{k}}X_{k}:\bigwedge_{i% =1}^{m}P_{i}(X_{1},\dots,X_{k}).

Here $n_{\kappa}\geq 0$ are natural numbers, $1\leq\kappa\leq k$ , and $X_{\kappa}$ are variables that quantify over invertible matrices in $\mathbb{R}^{n_{\kappa}\times n_{\kappa}}$ . $P_{j}$ is a predicate of the form

AX_{\kappa}=X_{\mu}B\quad\text{for $1\leq\kappa,\mu\leq k$}

(2)

for some matrices $A$ and $B$ of matching sizes and with rational entries. Such systems of equations can be used to model the commutativity relations in Equation 1. It is easy to see that $\mathrm{ETIM}_{\mathbb{R}}$ is a fragment of the existential theory of the reals ( $\mathrm{ETR}$ ). Since $\mathrm{ETR}\in\mathsf{PSPACE}$ [2, 9], this implies that $\mathrm{ETIM}_{\mathbb{R}}\in\mathsf{PSPACE}$ too. The survey [10, L-Open2] asks the natural question whether $\mathrm{ETIM}_{\mathbb{R}}$ is $\exists\mathbb{R}$ -complete.

Utilizing the $\mathsf{PSPACE}$ upper bound for $\mathrm{ETIM}_{\mathbb{R}}$ , Dubut [4] shows that bisimilarity of finitary diagrams can be decided in $\mathsf{EXPSPACE}$ . For this, he guesses the tuples of a bisimulation relation with placeholders for the isomorphisms, implicitly using that if there is bisimulation, then there is one of at most exponential size. Then to check whether isomorphisms in the guessed relation can be instantiated such that they fulfill the commutativity relations in (1), he sets up a system of equations and uses the $\mathsf{PSPACE}$ algorithm for $\mathrm{ETIM}$ on an exponentially large instance to check its feasibility.

In a similar fashion, Dubut [4] solves the model checking problem for positive diagrammatic path logic in $\mathsf{PSPACE}$ . He first guesses the “combinatorial” part of the model checking problem, then sets up a system of equations of the form (1), and then invokes the $\mathsf{PSPACE}$ algorithm for $\mathrm{ETIM}_{\mathbb{R}}$ .

1.2 Our contributions

We begin by showing that the aforementioned algebraic part of finding bisimulations is often easy. In particular, we demonstrate that the existential theory of invertible matrices $\mathrm{ETIM}$ allows for an efficient randomized algorithm over the reals, i.e., $\mathrm{ETIM}_{\mathbb{R}}\in\mathsf{RP}$ , greatly improving on the upper bound of $\mathsf{PSPACE}$ by [4]. This is still true when we allow arbitrary linear constraints in the entries of the matrices and not only constraints of the form (2). We call this generalization $\mathrm{genETIM}_{\mathbb{R}}$ . We obtain our efficient algorithm by reducing the problem to the well-known polynomial identity testing problem (PIT). [10, L-Open2] asks whether $\mathrm{ETIM}_{\mathbb{R}}$ is $\exists\mathbb{R}$ -complete. Our results answer this question in the negative (assuming $\mathsf{RP}\not=\exists\mathbb{R}$ ). We also show that derandomizing the algorithm will be difficult, at least for $\mathrm{genETIM}_{\mathbb{R}}$ , since this would be equivalent to derandomizing symbolic determinant identity testing ( $\mathrm{SDIT}_{\mathbb{R}}$ ), which is a major open problem in complexity theory [8].

$\mathrm{ETIM}_{\mathbb{R}}\in\mathsf{RP}$ implies that $\mathrm{ETIM}_{\mathbb{R}}\in\mathsf{NP}$ . In fact, we are able to show that $\mathrm{ETIM}_{\mathbb{F}}\in\mathsf{NP}$ for all fields $\mathbb{F}$ . Using this new upper bound for $\mathrm{ETIM}$ readily gives improved upper bounds for testing bisimilarity of finitary diagrams as well as model checking for (negation-free) diagrammatic path logic of finitary diagrams. We call these problems $\mathrm{BisimFD}_{\mathbb{F}}$ and $\mathrm{posFF}_{\mathbb{F}}$ respectively. We get that $\mathrm{posFF}_{\mathbb{F}}\in\mathsf{NP}$ and $\mathrm{BisimFD}_{\mathbb{F}}\in\mathsf{NEXP}$ for all fields $\mathbb{F}$ .

For $\mathrm{posFF}_{\mathbb{F}}$ , we prove a matching lower bound – we show that the problem is $\mathsf{NP}$ -hard too. In the reduction, we define constrained layered poset problems, which might be of independent interest for showing hardness proofs in the context of finitary diagrams. To relate constrained layered posets to finitary diagrams, we make use of Gabriel’s theorem for the representation of path quivers. For $\mathrm{BisimFD}_{\mathbb{F}}$ , we go further and present a $\mathsf{PSPACE}$ upper bound when $\mathbb{F}$ is a finite field.

Finally, we study the theory of special linear matrices. Instead of quantifying over invertible matrices, here we quantify over matrices with determinant $1$ . This corresponds to isomorphisms that are volume preserving. While we show that the generalized theory of real invertible matrices is in $\mathsf{RP}$ , we prove that the generalized theory of special linear matrices is $\exists\mathbb{R}$ -complete. We leave it as an open question whether this is also true if we only allow for linear constraints of the form $(\ref{eq:etim})$ .

2 Preliminaries

2.1 Finitary diagrams

Definition 1 ([4]).

A finitary diagram $F$ over a field $\mathbb{F}$ consists of the following data:

1.

a finite partially ordered set (for short poset) $(C,\leq)$ which describes the domain,
2.

for every $c\in C$ , a natural number $F(c)$ (which stands for the vector space $\mathbb{F}^{F(c)}$ ),
3.
for every pair $c\leq c^{\prime}$ of $C$ , a matrix $F(c\leq c^{\prime})$ of size $F(c^{\prime})\times F(c)$ , with coefficients from $\mathbb{F}$ , such that:
- $\blacksquare$
  
  $F(c\leq c)$ is the identity matrix for all $c\in C$ ,
- $\blacksquare$
  
  for every triple $c\leq c^{\prime}\leq c^{\prime\prime}$ , $F(c\leq c^{\prime\prime})=F(c^{\prime}\leq c^{\prime\prime})\cdot F(c\leq c^{% \prime})$ , where “ $\cdot$ ” denotes matrix multiplication.

2.2 Bisimilarity

We first give the general definition of bisimulations in the setting of [5] and [4] and then specialize it to finitary diagrams.

Definition 2.

A bisimulation $R$ between two diagrams $F:C\rightarrow A$ and $G:D\rightarrow A$ is a set of triples $(c,f,d)$ where $c$ is an object of $C$ , $d$ is an object of $D$ and $f:F(c)\rightarrow G(d)$ is an isomorphism of A such that:

1.

For every $(c,f,d)\in R$ and $i:c\rightarrow c^{\prime}\in C$ , there exists $j:d\rightarrow d^{\prime}\in D$ and $g:F(c^{\prime})\rightarrow G(d^{\prime})\in A$ such that $g\circ F(i)=G(j)\circ f$ and $(c^{\prime},g,d^{\prime})\in R$ , see Figure 1.
2.

Symmetrically, for every $(c,f,d)\in R$ and $j:d\rightarrow d^{\prime}\in D$ , there exists $i:c\rightarrow c^{\prime}\in C$ and $g:F(c^{\prime})\rightarrow G(d^{\prime})\in A$ such that $g\circ F(i)=G(j)\circ f$ and $(c^{\prime},g,d^{\prime})\in R$ .
3.

$\forall c\in C:\exists d,f:(c,f,d)\in R$ .
4.

$\forall d\in D:\exists c,f:(c,f,d)\in R$ .

Figure 1: If

f

identifies

c

with

d

and

i

is a morphism

c\to c^{\prime}

, then there must be an object

d^{\prime}

and an isomorphism

g

such that the diagram commutes.

Definition 3.

Two diagrams are called bisimilar if there is a bisimulation between them.

We will denote the problem of bisimilarity testing in finitary diagrams by $\mathrm{BisimFD}_{\mathbb{F}}$ , where $\mathbb{F}$ is the underlying field of the vector spaces in the diagram. The main result of [4] on the bisimilarity of finitary diagrams is the following.

Proposition 4.

$\mathrm{BisimFD}_{\mathbb{R}}\in\mathsf{EXPSPACE}$ .

2.3 Diagrammatic path logic and finitary formulae

[4] introduces the so-called diagrammatic path logic, which is similar to the logic introduced by [6] for transition systems or to path logics developed by [7]. Finitary formulae are an instance of diagrammatic path logic for finitary diagrams. The syntax is as follows.

Object formulae:: $S::=[n]P$ with $n\in\mathbb{N}$
Morphism formulae:: $P::=\langle M\rangle P\ |\ ?S\ |\ \neg P\ |\ P_{1}\wedge P_{2}\ |\ \top$ ,

where $M$ is a matrix over some field $\mathbb{F}$ . Here, $[n]P$ asserts that the current object represents the vector space $\mathbb{F}^{n}$ , $\langle M\rangle P$ “fires” a transition via the matrix $M$ , “?” transitions back to object-level evaluation, $\neg$ and $\wedge$ are standard Boolean connectives, and $\top$ is the tautology.

The semantics are as follows: For a diagram $F:\mathcal{C}\to\mathcal{A}$ , an object $c\in\mathcal{C}$ , and an isomorphism $f$ of $\cal A$ of the form $f:\mathbb{F}^{F(d)}\to\mathbb{F}^{F(d)}$ for some $d$ , we define $F,c\models S$ for an object formula $S$ , and $F,f,d\models P$ for a morphism formula $P$ by induction on the structure:

1.

$F,c\models[n]P$ iff $F(c)=n$ and $F,f,c\models P$ for some isomorphism $f:\mathbb{F}^{F(c)}\to\mathbb{F}^{F(c)}$ .
2.

$F,f,c\models\langle M\rangle P$ iff there is a $c\leq c^{\prime}$ in $\cal C$ and an isomorphism $f^{\prime}$ of $\mathbb{F}^{F(c^{\prime})}$ such that $Mf=f^{\prime}F(c\leq c^{\prime})$ .
3.

? switches back to object formulae, $F,f,c\models?S$ iff $F,c\models S$ .
4.

Conjunction has the usual semantics, i.e., $F,f,c\models P_{1}\wedge P_{2}$ iff $F,f,c\models P_{1}$ and $F,f,c\models P_{2}$ .
5.

The same is true for negation, $F,f,c\models\neg P$ iff $F,f,c\not\models P$ .
6.

Finally, $\top$ is always satisfied, i.e., $F,f,c\models\top$ always holds.

This setup closely mirrors labeled transition or path logics, but here the “labels” are matrices over a field.

Let $\mathrm{FF}$ denote all triples $(F,c,S)$ , where $S$ is a finitary object formula, such that $F,c\models S$ . A finitary formula is called positive if it does not contain any negations. Let $\mathrm{posFF}_{\mathbb{F}}$ denote the subset of $\mathrm{FF}$ corresponding to positive finitary formulas, with $\mathbb{F}$ being the underlying field. [4, Thm. 9] shows the following:

Proposition 5.

$\mathrm{posFF}_{\mathbb{R}}\in\mathsf{PSPACE}$ .

2.4 Existential theory of the reals

The existential theory of the reals ( $\mathrm{ETR}$ ) is the decision problem of determining the truth of formulas of the form

\exists x_{1},\ldots,x_{n}\;:\;\Big(p_{1}(x_{1},\ldots,x_{n})\ \bowtie_{1}\ 0% \Big)\;\land\;\cdots\;\land\;\Big(p_{m}(x_{1},\ldots,x_{n})\ \bowtie_{m}\ 0% \Big),

(3)

where each $p_{i}$ is a multivariate polynomial with integer (or rational) coefficients, and

\bowtie_{i}\;\in\;\{=,\ <,\ \leq,\ >,\ \geq\}.

The complexity class $\exists\mathbb{R}$ is the set of all languages polynomial-time many-one reducible to the $\mathrm{ETR}$ problem. It satisfies $\mathsf{NP}\subseteq\exists\mathbb{R}\subseteq\mathsf{PSPACE}$ . By now, there is an abundance of complete problems for $\exists\mathbb{R}$ known, see the recent compendium [10].

2.5 Existential theory of invertible matrices

Dubut [4] defines the existential theory of invertible matrices as an intermediate problem. It contains sentences of the form

\exists_{n_{1}}X_{1}\exists_{n_{2}}X_{2}\dots\exists_{n_{k}}X_{k}:\bigwedge_{i% =1}^{m}P_{i}(X_{1},\dots,X_{k}).

Here $n_{\kappa}\geq 0$ are natural numbers, $1\leq\kappa\leq k$ and $X_{\kappa}$ are variables that quantify over invertible matrices in $\mathbb{F}^{n_{\kappa}\times n_{\kappa}}$ , for some field $\mathbb{F}$ . $P_{j}$ is a predicate of the form $AX_{\kappa}=X_{\mu}B$ for $1\leq\kappa,\mu\leq k$ for some matrices $A$ and $B$ of matching sizes and with entries from $\mathbb{F}$ . $\mathrm{ETIM}_{\mathbb{F}}$ is the set of all true sentences of the above form.

The predicates were chosen to be of the above form because they naturally appear in the case of finitary diagrams. We can also consider a more general problem where each $P_{i}$ is an arbitrary affine linear equation in the entries of the matrices $X_{1},\dots,X_{k}$ . We call this problem $\mathrm{genETIM}_{\mathbb{F}}$ , as it is a generalization of $\mathrm{ETIM}_{\mathbb{F}}$ .

2.6 Nondeterministic reductions

As a tool to prove the containment of problems in $\mathsf{NP}$ or $\mathsf{NEXP}$ , we will use nondeterministic reductions, which already implicitly appear in [4].

Definition 6.

A language $A$ is nondeterministically polynomial time many-one reducible to $B$ if there is a deterministically polynomial time computable function $f$ with two inputs such that for all $x$ : $x\in A$ iff there is a $y$ with $|y|\leq\operatorname{poly}(|x|)$ such that $f(x,y)\in B$ . We write $A\leq_{\mathrm{NP}}B$ .

Proposition 7.

If $A\leq_{\mathrm{NP}}B$ and $B\in\mathsf{NP}$ , then $A\in\mathsf{NP}$ .

We will also need nondeterministic exponential-time reductions. Exponential here means $2^{\operatorname{poly}(n)}$ .

Definition 8.

A language $A$ is nondeterministically exponential-time many-one reducible to $B$ , if there is an exponential time computable function $f$ with two inputs such that for all $x$ : $x\in A$ iff there is a $y$ with $|y|\leq 2^{\operatorname{poly}(|x|)}$ such that $f(x,y)\in B$ . We write $A\leq_{\mathrm{NEXP}}B$ .

Proposition 9.

If $A\leq_{\mathrm{NEXP}}B$ and $B\in\mathsf{NP}$ , then $A\in\mathsf{NEXP}$ .

2.7 A tool from quiver theory and persistent homology

A finitary diagram is a functor from a poset category to the category of finite-dimensional vector spaces and linear maps. This is closely related to the notion of representations of a quiver and when the poset is totally ordered, it is exactly the same as single-parameter persistent modules. Therefore, tools from quiver theory and persistent homology can prove useful for problems on finitary diagrams. We use one particular tool which follows from the well-known Gabriel’s theorem on quivers and also appears in persistent homology as the rank invariant criterion [3, Theorem 12].

Theorem 10.

We are given the matrices $A_{1},\cdots,A_{k}$ and $B_{1},\cdots,B_{k}$ over some field $\mathbb{F}$ , where for each $i\in[k]$ , the matrices $A_{i}$ and $B_{i}$ have dimension $d_{i+1}\times d_{i}$ for some integers $d_{1},\cdots,d_{k+1}$ . For $1\leq i\leq i^{\prime}\leq k$ , let $A_{[i,i^{\prime}]}$ denote the product $A_{i^{\prime}}A_{i^{\prime}-1}\cdots A_{i}$ and $B_{[i,i^{\prime}]}$ denote the product $B_{i^{\prime}}B_{i^{\prime}-1}\cdots B_{i}$ . Then,

	$\displaystyle\exists\text{ invertible matrices }X_{1},\cdots,X_{k+1}\ :\ % \forall i\geq 2,\ X_{i}\cdot A_{i-1}=B_{i-1}\cdot X_{i-1}$
	$\displaystyle\iff\text{ for all }1\leq i\leq i^{\prime}\leq k,\ \operatorname{% rk}A_{[i,i^{\prime}]}=\operatorname{rk}B_{[i,i^{\prime}]}\ .$

This criterion follows from the classification of representations of the Dynkin quiver $A_{n}$ (a special case of Gabriel’s theorem). For more background on the criterion and its connection to Gabriel’s theorem, refer to the full version.

3 Overview of results and techniques

We give a comprehensive overview of our results and explain the main techniques used in our proofs.

3.1 Existential theory of invertible matrices

Dubut introduces the existential theory of invertible matrices ( $\mathrm{ETIM}$ ) to get upper bounds for deciding bisimilarity of finitary diagrams and model checking of finitary formulae. An instance of $\mathrm{ETIM}_{\mathbb{F}}$ is of the form $\exists_{n_{1}}X_{1}\exists_{n_{2}}X_{2}\dots\exists_{n_{k}}X_{k}:\bigwedge_{i% =1}^{m}P_{i}(X_{1},\dots,X_{k})$ , where each constraint is of the form $AX_{i}=X_{j}B$ for matrices $A$ and $B$ over $\mathbb{F}$ . If we consider the case of the real field, an instance of $\mathrm{ETIM}$ can be easily translated into an equivalent instance of the existential theory of the reals. This leads [10, L-Open2] to ask the natural question whether $\mathrm{ETIM}_{\mathbb{R}}$ is $\exists\mathbb{R}$ -complete. We answer this question in the negative (assuming $\mathsf{RP}\not=\exists\mathbb{R}$ ) by giving an efficient randomized algorithm.

Dubut uses $\mathrm{ETIM}_{\mathbb{F}}$ to verify the commutativity relations of the form $(\ref{eq:etim})$ , which explains the structure of the constraints $P_{i}$ . It turns out that our algorithm can also handle the case of arbitrary affine linear equations in the entries of the matrices, which we call $\mathrm{genETIM}_{\mathbb{F}}$ .

Theorem I (Theorem 12).

$\mathrm{genETIM}_{\mathbb{F}}\in\mathsf{RP}$ for infinite fields $\mathbb{F}$ .

Proof overview.

In a $\mathrm{genETIM}$ instance, we have linear equations from the constraints $P_{1},\dots,P_{m}$ , and polynomial inequalities involving the determinants, expressing that the matrices $X_{1},\dots,X_{k}$ are invertible. First, we parametrize the solution space of the linear system using free variables and substitute this parametrization into the matrix variables. The instance is satisfiable if and only if after the substitution, all of the determinants are nonzero polynomials. This can be tested with the famous Schwartz-Zippel lemma. We need the infiniteness of the field to sample enough points from it for the use of the lemma. $\hfill\blacktriangleleft$

One can ask the question whether our algorithm can be derandomized. This turns out to be a hard problem, since it is equivalent to the complement of the symbolic determinant identity problem, whose derandomization over the rationals/reals in particular implies strong circuit lower bounds (see [8]).

Theorem II (Theorem 15).

$\mathrm{genETIM}_{\mathbb{F}}$ is deterministically polynomial time equivalent to the complement of the symbolic determinant identity testing problem $\mathrm{SDIT}_{\mathbb{F}}$ for all fields $\mathbb{F}$ .

Proof overview.

The reduction from $\mathrm{genETIM}_{\mathbb{F}}$ to the complement of $\mathrm{SDIT}_{\mathbb{F}}$ is already implicit in the proof strategy of the above theorem. For the other direction, we essentially use the linear constraints of $\mathrm{genETIM}_{\mathbb{F}}$ to specify the affine linear entries of the $\mathrm{SDIT}_{\mathbb{F}}$ instance. $\hfill\blacktriangleleft$

3.2 First results through our algorithm for ETIM

Dubut essentially constructs nondeterministic reductions from $\mathrm{BisimFD}$ and $\mathrm{posFF}$ to $\mathrm{ETIM}$ . The first one is an exponential time reduction, the second one is polynomial-time. In both reductions, he nondeterministically guesses the assignments between states and for each such guess, he creates an equation of the form (2) to check the existence of a matching isomorphism. All these checks can be pushed to the end, making the algorithms by Dubut essentially nondeterministic reductions. Since $\mathrm{ETIM}_{\mathbb{F}}\in\mathsf{NP}$ (using Theorem 12 for infinite fields and trivially for finite fields) and $\mathsf{NP}$ is closed under nondeterministic polynomial time reductions and the closure of $\mathsf{NP}$ under nondeterministic exponential time reductions is $\mathsf{NEXP}$ , we get the following results

Theorem III (Corollary 18).

$\mathrm{BisimFD}_{\mathbb{F}}\in\mathsf{NEXP}$ for all fields $\mathbb{F}$ .

Theorem IV (Corollary 23).

$\mathrm{posFF}_{\mathbb{F}}\in\mathsf{NP}$ for all fields $\mathbb{F}$ .

The upper bound for $\mathrm{posFF}$ is optimal, the one for $\mathrm{BisimFD}$ can be further improved for finite fields.

3.3 Complexity of bisimilarity checking for finitary diagrams

Theorem V (Theorem 21).

$\mathrm{BisimFD}_{\mathbb{F}}\in\mathsf{PSPACE}$ when $\mathbb{F}$ is a finite field.

Proof overview.

The above reduction approach to $\mathrm{ETIM}$ produces a system of equations of exponential size, therefore, we have to use a different approach. We set up a quantified formula that is true iff the given diagrams are bisimilar. This formula quantifies over Boolean variables and matrices over $\mathbb{F}$ . Therefore, we can brute-force over all possibilities in $\mathsf{PSPACE}$ . $\hfill\blacktriangleleft$

3.4 Complexity of model checking for finitary formulae

We already showed that $\mathrm{posFF}$ is in $\mathsf{NP}$ . Now we establish its $\mathsf{NP}$ -completeness.

Theorem VI (Theorem 28).

$\mathrm{posFF}_{\mathbb{F}}$ is $\mathsf{NP}$ -hard for all fields $\mathbb{F}$ .

Proof overview.

We reduce the classic CLIQUE problem to $\mathrm{posFF}$ . Given an undirected graph $G$ and a parameter $k$ , we have to construct a finitary diagram and a finitary formula over the diagram such that the formula is satisfiable if and only if $G$ has a clique of size $k$ . A finitary diagram $F$ is a functor from a poset to the category of finite-dimensional $\mathbb{F}$ -vector spaces and linear maps. Posets can be viewed as transitive and reflexive directed acyclic graphs, which is already a very restricted class of graphs. Further, whenever there is a chain $a\leq b\leq c$ in the poset, the diagram must satisfy $F(b\leq c)\cdot F(a\leq b)=F(a\leq c)$ . All these restrictions make the reduction extremely tricky. Therefore, we construct intricate gadgets called constrained layered posets, which help us build the necessary finitary diagram. Then we construct a finitary object formula of the form $[q]\langle M_{1}\rangle\langle M_{2}\rangle\cdots\langle M_{k}\rangle$ . The advantage of this special form is that we can use the rank invariant criterion in Theorem 10 to characterize the satisfiability of such formulas. Finally, we can ensure that the rank-invariance conditions are satisfied if and only if $G$ has a $k$ -clique. $\hfill\blacktriangleleft$

3.5 Existential theory of special linear matrices

Instead of taking arbitrary isomorphisms for identifying the elements of the diagram, we could also consider special linear maps, that is, matrices of determinant one. This would put stronger geometric conditions on the similarity, for instance, volumes being preserved. It is natural to explore the complexity of the corresponding problems. We prove that the existential theory of special linear matrices is $\exists\mathbb{R}$ -complete, in contrast to $\mathrm{genETIM}_{\mathbb{R}}$ .

Theorem VII (Corollary 33).

$\mathrm{genETSLM}_{\mathbb{R}}$ is $\exists\mathbb{R}$ -complete.

Proof overview.

The reduction is gadget-based. We start from a special case of $\mathrm{ETR}$ , called $\mathrm{ETR}_{\mathrm{inv}}$ , where we are only allowed to use equations of the form $x=1$ , $x+y=z$ , and $xy=1$ , cf. [1]. For every variable, we set up a $2\times 2$ -matrix and use linear equations such that the matrices have the form $\left(\begin{smallmatrix}x&0\\ 0&x^{\prime}\end{smallmatrix}\right)$ . Together with the fact that we quantify over special linear matrices, this enforces $xx^{\prime}=1$ , that is, $x^{\prime}=x^{-1}$ . This automatically also implements equations of the form $xy=1$ . The tricky part is to implement the additions. This requires a series of cleverly chosen linear equations. In each step, we have to ensure that we do not constrain the matrices too much, since we always have to ensure that there is still a solution in which the determinant of the matrices in the equations is one. $\hfill\blacktriangleleft$

4 An efficient algorithm for the existential theory of invertible matrices

In this section, we present our first main result, an efficient algorithm for the generalized existential theory of invertible matrices. The main insight for designing our algorithm is that we can reduce the existential theory of invertible matrices to polynomial identity testing (PIT). Then we will use the famous Schwartz-Zippel Lemma, see e.g. [11], to get an efficient randomized algorithm.

Lemma 11 (Schwartz-Zippel).

Let $P\in R[x_{1},x_{2},\dots,x_{n}]$ be a non-zero polynomial of total degree $d>0$ over an integral domain $R$ . Let $S$ be a finite subset of $R$ and let $r_{1},r_{2},\dots,r_{n}$ be selected independently and uniformly at random from $S$ . Then:

\Pr[P(r_{1},r_{2},\dots,r_{n})=0]\leq\frac{d}{|S|}.

Let

\exists_{n_{1}}X_{1}\exists_{n_{2}}X_{2}\dots\exists_{n_{k}}X_{k}:\bigwedge_{i% =1}^{m}P_{i}(X_{1},\dots,X_{k}).

(4)

be the given $\mathrm{genETIM}$ -instance. Recall that we quantify over invertible matrices and that $P_{1},\dots,P_{m}$ are affine linear equations in the entries $x_{i,j}^{(h)}$ of the matrices $X_{h}$ , $1\leq i,j\leq n_{h}$ , $1\leq h\leq k$ . The following algorithm decides whether the instance is true:

Algorithm 1

\mathrm{genETIM}

by identity testing.

Input: A $\mathrm{genETIM}$ -instance like in Equation 4
Output: Whether the instance is satisfiable

Theorem 12.

$\mathrm{genETIM}_{\mathbb{F}}\in\mathsf{RP}$ for infinite fields $\mathbb{F}$ .

Proof.

We need to prove the correctness of Algorithm 1. If the algorithm returns 1, then by construction it has found an assignment to $X_{1},\dots,X_{k}$ such that the linear constraints are satisfied and each determinant is nonzero, that is, the matrix is invertible. If on the other hand the algorithm returns $0$ , then either the linear system has no solution, or one of the determinants is identically zero, or one of the identity tests erroneously failed. In the first case, there is indeed no solution, since already the linear system without any invertibility constraints is not satisfiable. In the second case, there is no solution, too, since we computed the solution space of the affine system of linear constraints and one of the determinants vanishes on this space. In the third case, by choosing the set $S$ in the Schwartz-Zippel lemma large enough, we can ensure that the error probability of one test failing is $\leq 1/(2k)$ . This means that by the union bound, the error probability in the yes-case is bounded by $1/2$ , thus we satisfy the acceptance condition of $\mathsf{RP}$ .

The algorithm can be implemented in randomized polynomial time, since we only solve systems of linear equations and evaluate determinants. This proves the theorem. $\hfill\blacktriangleleft$

Corollary 13.

$\mathrm{ETIM}_{\mathbb{F}}\in\mathsf{RP}$ for infinite fields $\mathbb{F}$ .

Since $\mathsf{RP}\subseteq\mathsf{NP}$ , we have $\mathrm{genETIM}_{\mathbb{F}}\in\mathsf{NP}$ for all infinite fields $\mathbb{F}$ . On the other hand, for finite fields $\mathbb{F}$ , we trivially have $\mathrm{genETIM}_{\mathbb{F}}\in\mathsf{NP}$ , since one can guess the solution to the $\mathrm{genETIM}$ -instance non-deterministically. The same is true for $\mathrm{ETIM}$ . Therefore, we have the following corollary.

Corollary 14.

$\mathrm{genETIM}_{\mathbb{F}}\in\mathsf{NP}$ and $\mathrm{ETIM}_{\mathbb{F}}\in\mathsf{NP}$ for all fields $\mathbb{F}$ .

Next, we show that our upper bound for $\mathrm{genETIM}$ is optimal in the sense that derandomizing it over rational/real fields would have dramatic consequences in complexity theory. The symbolic determinant identity problem ( $\mathrm{SDIT}_{\mathbb{F}}$ ) is the following problem: Given a square matrix $A(\mathbf{y})$ whose entries are affine linear polynomials from $\mathbb{F}[y_{1},\cdots,y_{m}]$ , decide whether $\det A=0$ .

Theorem 15.

$\mathrm{genETIM}_{\mathbb{F}}$ is deterministically polynomial time equivalent to the complement of $\mathrm{SDIT}_{\mathbb{F}}$ for all fields $\mathbb{F}$ .

Proof.

The reduction from $\mathrm{genETIM}_{\mathbb{F}}$ to the complement of $\mathrm{SDIT}_{\mathbb{F}}$ is exactly the construction in Algorithm 1. Since we stop just before invoking the Schwartz-Zippel lemma, this part of the construction holds over all fields $\mathbb{F}$ .

For the other direction, first we can use a standard reduction from $\mathrm{SDIT}$ for matrices with affine linear entries to $\mathrm{SDIT}$ for matrices with entries which are only variables or constants. Refer to the full version for this reduction. Now, given an $\mathrm{SDIT}$ -instance $A=(a_{i,j})$ of size $n\times n$ with entries that are variables or constants, we create a $\mathrm{genETIM}$ -instance as follows: We quantify over one matrix $X=(x_{i,j})$ of size $n\times n$ . If $a_{i,j}$ is a constant, then we add the equation $x_{i,j}=a_{i,j}$ to the instance. For each variable $y_{\ell}$ that appears in $A$ , we let $(i_{1},j_{1}),\dots,(i_{k},j_{k})$ be the entries of $A$ in which it occurs. Then we add the equations $x_{i_{s},j_{s}}=x_{i_{s+1},j_{s+1}}$ , $1\leq s<k$ , to the instance. By construction $\det A\not=0$ iff there is an invertible matrix that satisfies the constructed equations. $\hfill\blacktriangleleft$

Over finite fields, $\mathrm{SDIT}$ is $\mathsf{coNP}$ -complete. Over rational/real fields, derandomizing $\mathrm{SDIT}$ (as well as PIT in general) is a major open problem in computational complexity, in particular, it implies strong circuit lower bounds ([8]).

5 An improved algorithm for bisimilarity

In this section, we present an improved algorithm for bisimilarity testing of finitary diagrams. [4, Theorem 8] shows that this problem is in $\mathsf{EXPSPACE}$ . We get an improvement by using our new result for $\mathrm{genETIM}$ (Theorem 12). [4, Section 7] gives an algorithm, which implicitly constructs a nondeterministic reduction from testing bisimilarity of finitary diagrams to $\mathrm{ETIM}$ :

Proposition 16 (implicit in [4]).

$\mathrm{BisimFD}_{\mathbb{F}}\leq_{\mathrm{NEXP}}\mathrm{ETIM}_{\mathbb{F}}$ for all fields $\mathbb{F}$ .

In his reduction, Dubut essentially guesses a bisimulation, that is, triples of the form $(a,X,b)$ , implicitly using the fact that if there is a bisimulation, then there is always one of exponential size. The reduction works as follows: In the triple $(a,X,b)$ , $a$ is from the poset $C$ of the first diagram $F:C\to A$ and $b$ is from the poset $D$ of the second diagram $G:D\to A$ . $X$ is a “placeholder” for the isomorphism between $F(a)$ and $G(b)$ . We then list all the $\mathrm{ETIM}$ -equations that need to be satisfied according to Definition 3 and use an $\mathrm{ETIM}$ -solver to check whether the system is feasible.

This implicitly uses the following lemma. Let $S$ be a bisimulation between two finitary diagrams $F:C\to A$ and $G:D\to A$ . We define a partial order on the set of triples in $S$ as follows:

(a,f,b)\leq(a^{\prime},f^{\prime},b^{\prime})\iff\text{$a\leq a^{\prime}$ and % $b\leq b^{\prime}$ and $f^{\prime}\cdot F(a\leq a^{\prime})=G(b\leq b^{\prime}% )\cdot f$}.

Lemma 17.

Any bisimulation $S$ between two finitary diagrams $F:C\to A$ and $G:D\to A$ contains a subset $S^{\prime}\subset S$ such that $S^{\prime}$ is a bisimulation and $|S^{\prime}|=2^{\operatorname{poly}(n)}$ , where $|C|,|D|\leq n$ .

Proof.

Consider $S$ with the order $\leq$ defined above. Among all minimal elements in $S$ , choose at most one tuple of the form $(a,f,b)$ for each pair $a\in C$ and $b\in D$ . The number of tuples is bounded by $n^{2}$ . For every tuple $(a,f,b)$ that was chosen in the first round and every $a<a^{\prime}$ , we choose a tuple $(a^{\prime},f^{\prime},b^{\prime})\in S$ such that $b\leq b^{\prime}$ and $f^{\prime}\cdot F(a\leq a^{\prime})=G(b\leq b^{\prime})\cdot f$ . Such tuples exist by the definition of bisimulation. We do the same for every $b<b^{\prime}$ . In this way, we add $2n$ new tuples to $S^{\prime}$ for each tuple added in the first round, so we add $\leq n^{2}\cdot(2n)$ tuples in total in the second round. Now we go on inductively: For each tuple $(a,f,b)$ added in the previous round and each $a\leq a^{\prime}$ , we choose one tuple $(a^{\prime},f^{\prime},b^{\prime})\in S$ such that $f^{\prime}\cdot F(a\leq a^{\prime})=G(b\leq b^{\prime})\cdot f$ and add it to $S^{\prime}$ . We do the same for every $b\leq b^{\prime}$ . This process comes to an end after $2n$ rounds. Therefore, the total size of $S^{\prime}$ is bounded by $|S^{\prime}|\leq n^{2}\cdot\sum_{i=0}^{2n}(2n)^{i}=2^{\operatorname{poly}(n)}$ . By construction, $S^{\prime}$ satisfies the conditions in the definition of bisimulation. $\hfill\blacktriangleleft$

Together with our improved upper bound for $\mathrm{ETIM}$ (Corollary 14) and Proposition 9, we get an improved upper bound for testing bisimilarity of finitary diagrams.

Corollary 18.

$\mathrm{BisimFD}_{\mathbb{F}}\in\mathsf{NEXP}$ for all fields $\mathbb{F}$ .

6 A PSPACE upper bound for bisimilarity over finite fields

Next, we further improve the upper bound for $\mathrm{BisimFD}_{\mathbb{F}}$ to $\mathsf{PSPACE}$ , when $\mathbb{F}$ is a finite field. Since the system of equations that is generated in the above reduction is of exponential size, the reduction approach to $\mathrm{ETIM}$ will not work unless we could prove that there is a smaller system. Instead, we will (deterministically) polynomial-time reduce this problem to $\mathrm{TQBF}$ , the set of all true quantified Boolean formulas, which is a classical $\mathsf{PSPACE}$ -complete problem.

Let $F:C\to A$ and $G:D\to A$ be two finitary diagrams. We construct a quantified formula $\Phi$ , which is true iff $F$ and $G$ are bisimilar:
$\begin{array}[]{ll}\forall a_{1}\quad\exists b_{1}&\exists_{D(a_{1})}X_{1}:% \operatorname{match}(a_{1},b_{1})\,\wedge\\ \forall a_{2}:\ \operatorname{sabove}(a_{2},a_{1},b_{1})\implies\\ \exists b_{2}:\ \operatorname{above}(b_{2},a_{1},b_{1})\ \wedge\ \operatorname% {match}(a_{2},b_{2})\ \wedge&\exists_{D(a_{2})}X_{2}:\operatorname{comm}(a_{1}% ,b_{1},X_{1},a_{2},b_{2},X_{2})\\ \forall a_{3}:\ \operatorname{sabove}(a_{3},a_{2},b_{2})\implies\\ \exists b_{3}:\ \operatorname{above}(b_{3},a_{2},b_{2})\ \wedge\ \operatorname% {match}(a_{3},b_{3})\ \wedge&\exists_{D(a_{3})}X_{3}:\operatorname{comm}(a_{2}% ,b_{2},X_{2},a_{3},b_{3},X_{3})\\ \vdots\\ \forall a_{m}:\ \operatorname{sabove}(a_{m},a_{m-1},b_{m-1})\implies\\ \exists b_{m}:\ \operatorname{above}(b_{m},a_{m-1},b_{m-1})\ \wedge\ % \operatorname{match}(a_{m},b_{m})\ \wedge&\exists_{D(a_{m})}X_{m}:\\ &\enspace\operatorname{comm}(a_{m-1},b_{m-1},X_{m-1},a_{m},b_{m},X_{m})\end{array}$ (5)
In the formula:

1.

$a_{i}$ and $b_{i}$ quantify over $C\cup D$ .
2.

$\operatorname{match}(a_{i},b_{i})$ is true if $a_{i}$ and $b_{i}$ are in different posets and the dimensions of the associated vector spaces match.
3.

$\operatorname{sabove}(a_{i},a_{i-1},b_{i-1})$ is true iff $a_{i-1},b_{i-1}$ are from different posets and $a_{i}$ is strictly greater than the element $a_{i-1}$ or $b_{i-1}$ of the matching poset. (The “s” stands for “strictly”.)
4.

$\operatorname{above}(b_{i},a_{i-1},b_{i-1})$ is defined in the same way, but we only require that $b_{i}$ is greater than the element of the matching poset.
5.

$\operatorname{comm}(a_{i-1},b_{i-1},X_{i-1},a_{i},b_{i},X_{i})$ is true if $a_{i-1}$ and $b_{i-1}$ are in different posets as well as $a_{i}$ and $b_{i}$ . Furthermore, the matrices $X_{i-1}$ and $X_{i}$ have to be chosen such that the diagram induced by the four elements commutes. Here we assume that the matrices map from $F$ to $G$ .
6.

$D(a_{i})$ is the dimension of the associated vector space, which is either $F(a_{i})$ or $G(a_{i})$ .
7.

$\exists_{D}X$ quantifies over $\mathbb{F}$ -matrices of size $D\times D$ .
8.

$m=|C|+|D|$ .

A model of the formula $\Phi$ in (5) can be thought of as a tree. The root has a child for every $a_{1}\in C\cup D$ . The node corresponding to each $a_{1}$ is labeled with a triple $(a_{1},X_{1},b_{1})$ such that $b_{1}$ is from the other poset with a matching dimension and $X_{1}\in\mathbb{F}^{D(a_{1})\times D(a_{1})}$ is an invertible matrix. For each element $a_{2}$ that is strictly above the matching element $a_{1}$ or $b_{1}$ , we select an element $b_{2}$ that is above the matching element $a_{1}$ or $b_{1}$ such that $a_{2}$ and $b_{2}$ are in different posets and the dimensions of the associated vector spaces match. Finally, we select an invertible matrix $X_{2}$ such that the diagram induced by the poset elements $a_{1},a_{2},b_{1},b_{2}$ as well as the two isomorphisms $X_{1}$ to $X_{2}$ commutes. $(a_{2},X_{2},b_{2})$ becomes the label of the new nodes. We go on recursively like this until both poset elements of $(a_{i},X_{i},b_{i})$ are maximal. This happens at the latest when $i=m=|C|+|D|$ . Note that when we have reached maximal elements, the predicate $\operatorname{sabove}(\dots)$ is always false, therefore, the implication is always true in this case. Thus it does not matter when we reach a maximal pair of poset elements earlier than after $m$ steps.

Lemma 19.

When the formula $\Phi$ has a model, then the diagrams $F$ and $G$ are bisimilar.

Proof.

We claim that the set $S$ of labels of the tree $T$ constructed above forms a bisimulation. For every $c\in C$ there exists $d\in D$ with $F(c)=G(d)$ and an $M\in\mathbb{F}^{F(c)\times F(c)}$ such that $(c,M,d)$ is a label. This is already ensured by the first layer of nodes in $T$ . The same is true for the symmetric statement with the roles of $c$ and $d$ swapped. Finally, if there is a tuple $(c,M,d)\in S$ , then for any $c<c^{\prime}$ , there must be a $d^{\prime}\geq d$ such that $F(c^{\prime})=G(d^{\prime})$ and an invertible matrix $M^{\prime}\in\mathbb{F}^{F(c^{\prime})\times F(c^{\prime})}$ such that $M^{\prime}F(c\leq c^{\prime})=G(d\leq d^{\prime})M$ . This is ensured by the $\exists b_{i}\dots$ part of the formula. The same is true for the symmetric statement for any $d<d^{\prime}$ . Since $c<c^{\prime}$ or $d<d^{\prime}$ , we can stop at depth $m$ , since any ascending chain in $C\times D$ with the order $(c,d)\leq(c^{\prime},d^{\prime})$ iff $c\leq c^{\prime}\wedge d\leq d^{\prime}$ has length at most $|C|+|D|=m$ . $\hfill\blacktriangleleft$

We can also prove the converse.

Lemma 20.

If $F$ and $G$ are bisimilar, then $\Phi$ has a model.

Proof.

Let $S$ be a bisimulation. For each $c\in C$ , we choose a tuple $(c,M,d)\in S$ and label one child of the root with it. Such tuples exist by the definition of bisimulation. In the same way for every $d\in D$ , we choose a tuple $(c,M,d)$ and add a child to the root. For every child with label $(c,M,d)$ such that either $c$ or $d$ are not maximal, we add for each $c^{\prime}>c$ a child with tuple $(c^{\prime},M^{\prime},d^{\prime})$ for some $d^{\prime}\geq d$ and $M^{\prime}$ such that the diagram induced by $c,c^{\prime},d,d^{\prime}$ commutes. Such a triple exists by the definition of bisimulation. We do the same for each $d^{\prime}>d$ . This obviously creates a model of $\Phi$ . $\hfill\blacktriangleleft$

Now we immediately get the following theorem.

Theorem 21.

$\mathrm{BisimFD}_{\mathbb{F}}\in\mathsf{PSPACE}$ when $\mathbb{F}$ is a finite field.

Proof.

The last two lemmas show that $F$ and $G$ are bisimilar if and only if the formula $\Phi$ in Equation 5 has a model. Since $\Phi$ is a QBF, we can brute-force over all assignments to the quantified variables in polynomial space and therefore decide its satisfiability in $\mathsf{PSPACE}$ . $\hfill\blacktriangleleft$

7 Complexity of model checking for finitary diagrams

There is a nondeterministic polynomial time reduction from $\mathrm{posFF}$ to $\mathrm{ETIM}$ . Since $\mathrm{ETIM}\in\mathsf{NP}$ , this proves that $\mathrm{posFF}\in\mathsf{NP}$ , improving on the $\mathsf{PSPACE}$ upper bound by [4].

Theorem 22.

$\mathrm{posFF}_{\mathbb{F}}\leq_{\mathrm{NP}}\mathrm{ETIM}_{\mathbb{F}}$ for all fields $\mathbb{F}$ .

Proof.

In the model checking problem, there are two kinds of choices that need to be made: In a formula of the form $[n]P$ , we need to choose an isomorphism. This will be done by $\mathrm{ETIM}$ . The second kind of choice is in formulas of the form $\langle M\rangle P$ . Here we can choose the next element $c^{\prime}$ of the diagram. This choice will be modeled by the nondeterminism of the reduction. This reduction is implicit in the work of [4], when he proves the $\mathsf{PSPACE}$ upper bound.

Our nondeterministic reduction will add quantifiers of the form $\exists_{n}X$ one after another to the output formula $O$ as well as linear equations. In the beginning, our input is a diagram $F$ , and an object $c$ and an object formula $P$ . The reduction proceeds recursively along the structure of $P$ . When $P$ is a morphism formula, then besides $F$ and $c$ , we will also have a variable matrix $X$ as an input. Our reduction simulates the semantic rules of Section 2.3 as follows:

$\blacksquare$

if $P=[n]S$ , then if $n\not=F(c)$ , we reject. Otherwise, we add the quantifier $\exists_{n}X$ for some fresh variable $X$ to $O$ and we go on with $F, c, X, P$ .
$\blacksquare$

if $P=?S$ , then we go on with $F, c, S$ .
$\blacksquare$

if $P=\top$ , then we accept and output $O$ .
$\blacksquare$

if $P=P_{1}\wedge P_{2}$ , then we first go on with $F,c,X,P_{1}$ and then with $F,c,X,P_{2}$ .
$\blacksquare$

If $P=\langle M\rangle P^{\prime}$ with $M$ being an $n_{2}\times n_{1}$ -matrix, then we first check whether $n_{1}=F(c)$ . If not, then we reject. Otherwise, we guess a $c^{\prime}$ with $c\leq c^{\prime}$ such that $F(c^{\prime})=n_{2}$ . If no such $c^{\prime}$ exists, then we reject. Otherwise, we add $\exists_{n_{2}}Y$ to $O$ for some fresh variable $Y$ as well as the equations $M\cdot X=Y\cdot F(c\leq c^{\prime})$ . Go on with $F,c^{\prime},Y,P^{\prime}$ .

By construction $(F,c)\in\mathrm{posFF}$ iff there is an accepting path on which we output a satisfiable $\mathrm{ETIM}$ -instance. $\hfill\blacktriangleleft$

Now, using Corollary 14 immediately gives us the following corollary.

Corollary 23.

$\mathrm{posFF}_{\mathbb{F}}\in\mathsf{NP}$ for all fields $\mathbb{F}$ .

Our next goal will be to show $\mathsf{NP}$ -hardness for $\mathrm{posFF}$ . We will achieve this by reducing Clique to $\mathrm{posFF}$ . For this reduction, we invent a gadget called constrained layered poset, which we outline below.

Definition 24 (Constrained Layered Poset (CLP)).

A poset $C$ is said to be a constrained layered poset (CLP) if it satisfies the following properties:

$\blacksquare$

Layered structure. For some $k,n\in\mathbb{N}$ , we have $C=\{c_{i,j}\ |\ i\in[k],j\in[n]\}$ . The elements are ordered by $c_{i,j}\leq c_{i^{\prime},j^{\prime}}$ iff $i<i^{\prime}$ or $(i,j)=(i^{\prime},j^{\prime})$ . Thus, the poset has $k$ layers where the $i$ -th layer is an antichain $\{c_{i,1},\cdots,c_{i,n}\}$ , and every element in layer $i$ is smaller than every element in layer $i^{\prime}>i$ .
$\blacksquare$

Set-labels. Every pair $a\leq b$ in the poset is labeled by a set $L(a,b)\subseteq U$ for some universe $U$ . We will call $L:C\times C\rightarrow 2^{U}$ the label-function of the CLP.
$\blacksquare$

Triplet criterion. For any triplet $a\leq b\leq c$ in $C$ , we have $L(a,b)\cap L(b,c)=L(a,c)$ .

Notice that a finitary diagram $F:C\rightarrow A$ can be visualized as the poset $C$ having every pair $c\leq c^{\prime}$ labeled by a matrix $F(c\leq c^{\prime})$ . However, in CLPs defined above, the pairs $c\leq c^{\prime}$ are labeled by sets $L(c,c^{\prime})$ instead. The idea behind this is to only focus on finitary diagrams where each matrix $F(c\leq c^{\prime})$ is a diagonal matrix with $0-1$ diagonal entries and its support being the index-set $L(c,c^{\prime})$ . Then the triplet criterion basically captures the fact that $F(a\leq c)=F(b\leq c)\cdot F(a\leq b)$ whenever $a\leq b\leq c$ in $C$ .

In the following lemma, we take the first step in our reduction. We show that given a graph, we can construct a CLP in polynomial time satisfying certain properties capturing the edge-relations in the graph.

Lemma 25.

Given an undirected graph $G=([n],E)$ and two integers $k, m$ with $m\geq n$ , we can construct in polynomial time a CLP $C=\{c_{i,j}\ |\ i\in[k],j\in[n]\}$ with label-function $L$ such that for all $1\leq i<i^{\prime}\leq k$ and $j,j^{\prime}\in[n]$ ,

|L(c_{i,j},c_{i^{\prime},j^{\prime}})|=\begin{cases}f(i,i^{\prime},k,m)&\text{% if }(j,j^{\prime})\in E,\\ f(i,i^{\prime},k,m)-1&\text{otherwise},\end{cases}

for some appropriately chosen function $f:\mathbb{Z}^{4}\rightarrow\mathbb{Z}$ .

Proof.

We are given an undirected graph $G=([n],E)$ and two integers $k, m$ with $m\geq n$ . We have to construct a CLP satisfying the given properties.

The poset.

Following the definition of CLP, we can define the comparabilities in our poset $C=\{c_{i,j}\ |\ i\in[k],\ j\in[n]\}$ as follows:

c_{i,j}\leq c_{i^{\prime},j^{\prime}}\text{ iff }i<i^{\prime}\text{ or }(i,j)=% (i^{\prime},j^{\prime}).

The universe.

Let $X:=\{e_{u,v},\ \hbox{\vbox{\hrule height=0.7pt\kern 1.72218pt\hbox{\kern 0.500% 03pt$e$\kern 0.50003pt}}}_{u,v}\ |\ (u,v)\in[m]^{2}\}$ be a set of symbols and set the universe $U:=[k]^{2}\times X$ . We also define a map $\eta:[m]^{2}\rightarrow X$ given by

\eta(u,v)=\begin{cases}e_{u,v}&\text{if }(u,v)\in E,\\ \hbox{\vbox{\hrule height=0.7pt\kern 1.72218pt\hbox{\kern 0.50003pt$e$\kern 0.% 50003pt}}}_{u,v}&\text{if }(u,v)\notin E,\end{cases}

which we are going to use later while constructing the labels. Note that in particular, $\eta(u,v)=\hbox{\vbox{\hrule height=0.7pt\kern 1.72218pt\hbox{\kern 0.50003pt$% e$\kern 0.50003pt}}}_{u,v}$ for all $(u,v)\in[m]^{2}\setminus[n]^{2}$ since $E\subseteq[n]^{2}$ .

Labels.

We have to assign $L(c,c^{\prime})\subseteq U$ for all comparable $c\leq c^{\prime}$ in $C$ . First of all, we set $L(c,c):=U\text{ for all }c\in C$ . Now we handle the strictly comparable pairs. For $i<i^{\prime}$ and $j,j^{\prime}\in[n]$ , we define

L(c_{i,j},c_{i^{\prime},j^{\prime}}):=Q_{i,i^{\prime}}\ \sqcup\ R_{i,i^{\prime% },j}\ \sqcup\ S_{i,i^{\prime},j^{\prime}}\ \sqcup\ T_{i,i^{\prime},j,j^{\prime}}

where

	$\displaystyle Q_{i,i^{\prime}}$	$\displaystyle=\{(a,a^{\prime},x)\in[k]^{2}\times X\ \|\ a<i<i^{\prime}<a^{% \prime}\},$
	$\displaystyle R_{i,i^{\prime},j}$	$\displaystyle=\{(i,a^{\prime},e_{j,b})\in[k]^{2}\times X\ \|\ a^{\prime}>i^{% \prime},\ b\in[m]\},$
	$\displaystyle S_{i,i^{\prime},j^{\prime}}$	$\displaystyle=\{(a,i^{\prime},\eta(b,j^{\prime}))\in[k]^{2}\times X\ \|\ a<i,\ % b\in[m]\},$
	$\displaystyle T_{i,i^{\prime},j,j^{\prime}}$	$\displaystyle=\begin{cases}\{(i,i^{\prime},e_{j,j^{\prime}})\}&\text{if }(j,j^% {\prime})\in E,\\ \emptyset&\text{otherwise.}\end{cases}$

The four sets are pairwise disjoint because they have mutually exclusive constraints on the first two coordinates.

For every $i<i^{\prime}$ and every $j,j^{\prime}\in[n]$ , we have
$|Q_{i,i^{\prime}}|=(i-1)(k-i^{\prime})\cdot 2m^{2},\quad|R_{i,i^{\prime},j}|=(% k-i^{\prime})m,\quad|S_{i,i^{\prime},j^{\prime}}|=(i-1)m,\quad|T_{i,i^{\prime}% ,j,j^{\prime}}|=\mathbbm{1}_{(j,j^{\prime})\in E}\ .$

Hence,

|L(c_{i,j},c_{i^{\prime},j^{\prime}})|=2(i-1)(k-i^{\prime})m^{2}+(k-i^{\prime}% )m+(i-1)m+\mathbbm{1}_{(j,j^{\prime})\in E}\ .

Now define the function $f:\mathbb{Z}^{4}\rightarrow\mathbb{Z}$ as

f(i,i^{\prime},k,m)=2(i-1)(k-i^{\prime})m^{2}+(k-i^{\prime})m+(i-1)m+1\ .

Then for all $j,j^{\prime}$ ,

|L(c_{i,j},c_{i^{\prime},j^{\prime}})|=\begin{cases}f(i,i^{\prime},k,m)&\text{% if }(j,j^{\prime})\in E,\\ f(i,i^{\prime},k,m)-1&\text{otherwise.}\end{cases}

Satisfaction of the triplet criterion.

It remains to show that for all $a\leq b\leq c$ in $C$ ,

L(a,b)\cap L(b,c)=L(a,c).

Assume $a=c_{i,j}$ , $b=c_{i^{\prime},j^{\prime}}$ , $c=c_{i^{\prime\prime},j^{\prime\prime}}$ with $i<i^{\prime}<i^{\prime\prime}$ . The sets $L(c_{i,j},c_{i^{\prime},j^{\prime}})$ and $L(c_{i^{\prime},j^{\prime}},c_{i^{\prime\prime},j^{\prime\prime}})$ can be written as unions of their $Q, R, S, T$ parts and hence their intersection is the union of the cross-intersections between these parts. The only nonempty cross-intersections are:

	$\displaystyle Q_{i,i^{\prime}}\cap Q_{i^{\prime},i^{\prime\prime}}$	$\displaystyle=Q_{i,i^{\prime\prime}},$	$\displaystyle R_{i,i^{\prime},j}\cap Q_{i^{\prime},i^{\prime\prime}}=R_{i,i^{% \prime\prime},j},$
	$\displaystyle S_{i^{\prime},i^{\prime\prime},j^{\prime\prime}}\cap Q_{i,i^{% \prime}}$	$\displaystyle=S_{i,i^{\prime\prime},j^{\prime\prime}},$	$\displaystyle R_{i,i^{\prime},j}\cap S_{i^{\prime},i^{\prime\prime},j^{\prime% \prime}}=T_{i,i^{\prime\prime},j,j^{\prime\prime}}.$

The first three equalities are easy to see. For the last equality, observe that $R_{i,i^{\prime},j}$ contains tuples with first coordinate $i$ and third coordinate $e_{j,b}$ for $b\in[m]$ while $S_{i^{\prime},i^{\prime\prime},j^{\prime\prime}}$ contains tuples with second coordinate $i^{\prime\prime}$ and third coordinate $\eta(b,j^{\prime\prime})$ for $b\in[m]$ . Therefore, their intersection can contain at most one element $(i,i^{\prime\prime},e_{j,j^{\prime\prime}})$ and it contains this element only when $\eta(j,j^{\prime\prime})=e_{j,j^{\prime\prime}}$ , i.e., when $(j,j^{\prime\prime})\in E$ . It follows that the intersection equals to $T_{i,i^{\prime\prime},j,j^{\prime\prime}}$ . Therefore,

L(c_{i,j},c_{i^{\prime},j^{\prime}})\cap L(c_{i^{\prime},j^{\prime}},c_{i^{% \prime\prime},j^{\prime\prime}})=Q_{i,i^{\prime\prime}}\sqcup R_{i,i^{\prime% \prime},j}\sqcup S_{i,i^{\prime\prime},j^{\prime\prime}}\sqcup T_{i,i^{\prime% \prime},j,j^{\prime\prime}}=L(c_{i,j},c_{i^{\prime\prime},j^{\prime\prime}}).\

$\hfill\blacktriangleleft$

As we described earlier, the idea behind using the set-labels $L(c,c^{\prime})$ for partial orders $c\leq c^{\prime}$ in CLPs is to define a finitary diagram $F:C\rightarrow A$ , where each $F(c\leq c^{\prime})$ is a diagonal matrix with $0-1$ diagonal entries and its support being the index-set $L(c\leq c^{\prime})$ . In the following lemma, we make this idea explicit in order to lift the CLP-gadget of Lemma 25 to a finitary-diagram-gadget.

Lemma 26.

Given a field $\mathbb{F}$ , an undirected graph $G=([n],E)$ and two integers $k, m$ with $m\geq n$ , we can construct in polynomial time a finitary diagram $F$ from a CLP $C=\{c_{i,j}\ |\ i\in[k],j\in[n]\}$ to a category $A$ composed of a single $\mathbb{F}$ -vector space and linear maps, such that for all $1\leq i<i^{\prime}\leq k$ and $j,j^{\prime}\in[n]$ ,

\operatorname{rk}F(c_{i,j}\leq c_{i^{\prime},j^{\prime}})=\begin{cases}f(i,i^{% \prime},k,m)&\text{if }(j,j^{\prime})\in E,\\ f(i,i^{\prime},k,m)-1&\text{otherwise},\end{cases}

for some appropriately chosen function $f:\mathbb{Z}^{4}\rightarrow\mathbb{Z}$ .

Proof.

Given the undirected graph $G=([n],E)$ and the integers $k, m$ with $m\geq n$ , first use Lemma 25 to construct a CLP $C=\{c_{i,j}\ |\ i\in[k],j\in[n]\}$ with label-function $L$ such that for all $1\leq i<i^{\prime}\leq k$ and $j,j^{\prime}\in[n]$ ,

|L(c_{i,j},c_{i^{\prime},j^{\prime}})|=\begin{cases}f(i,i^{\prime},k,m)&\text{% if }(j,j^{\prime})\in E,\\ f(i,i^{\prime},k,m)-1&\text{otherwise},\end{cases}

for some function $f:\mathbb{Z}^{4}\rightarrow\mathbb{Z}$ . Now we will define the finitary diagram $F:C\rightarrow A$ .

Let $U$ be the universe used in the label-function $L$ , i.e., $U=\bigcup\limits_{\begin{subarray}{c}a,b\in C\\ a\leq b\end{subarray}}L(a,b),$ and let $q:=|U|$ . We will define the range of the diagram to be the single-object category $A:=\{q\}$ where the object $q$ represents the vector space $\mathbb{F}^{q}$ . Therefore, $F(c)=q$ and $F(c\leq c)=\mathbf{I}_{q}$ for all $c\in C$ .

Choose any bijection $\phi:[q]\rightarrow U$ . Now, given a subset $S\subseteq U$ , define $\mathbf{I}_{S}$ to be the diagonal $q\times q$ matrix whose $i$ -th diagonal entry is $1$ if $\phi(i)\in S$ and $0$ otherwise. We have

\operatorname{rk}\mathbf{I}_{S}=|S|\quad\text{ and }\quad\mathbf{I}_{S}\cdot% \mathbf{I}_{T}=\mathbf{I}_{S\cap T}

for all $S,T\subseteq U$ . Now for all $a\leq b$ in $C$ , define

F(a\leq b)=\mathbf{I}_{L(a,b)}.

Then for all $a\leq b\leq c$ in $C$ ,

F(b\leq c)\cdot F(a\leq b)=\mathbf{I}_{L(a,b)}\cdot\mathbf{I}_{L(b,c)}=\mathbf% {I}_{L(a,b)\cap L(b,c)}=\mathbf{I}_{L(a,c)}=F(a\leq c)\ ,

as desired in a diagram, and for all $1\leq i<i^{\prime}\leq k$ and $j,j^{\prime}\in[n]$ ,

\operatorname{rk}F(c_{i,j}\leq c_{i^{\prime},j^{\prime}})=|L(c_{i,j},c_{i^{% \prime},j^{\prime}})|=\begin{cases}f(i,i^{\prime},k,m)&\text{if }(j,j^{\prime}% )\in E,\\ f(i,i^{\prime},k,m)-1&\text{otherwise}.\end{cases}\

$\hfill\blacktriangleleft$

Having built the necessary gadget, we can proceed towards the main proof now. The following lemma gives a necessary and sufficient condition for a special kind of finitary formula being satisfiable. Focusing on these special kind of formulas will be sufficient for us to prove $\mathsf{NP}$ -hardness of the general problem.

Lemma 27.

Let $F$ be a finitary diagram from a poset $C$ to a category $A=\{q\}$ , where the object $q$ represents the vector-space $\mathbb{F}^{q}$ for some field $\mathbb{F}$ . Let $S=[q]\langle M_{1}\rangle\langle M_{2}\rangle\cdots\langle M_{k}\rangle$ be an object formula for singular matrices $M_{1},\cdots,M_{k}$ over $\mathbb{F}$ of dimension $q\times q$ . Then given $c_{1}\in C$ , we have $F,c_{1}\models S$ if and only if there exists a chain $c_{1}<c_{2}<\cdots<c_{k+1}$ in $C$ satisfying

\operatorname{rk}(M_{i}M_{i+1}\cdots M_{i^{\prime}-1})=\operatorname{rk}F(c_{i% }\leq c_{i^{\prime}})

for all $1\leq i<i^{\prime}\leq k+1$ .

Proof.

We have

$F,c_{1}\models[q]\langle M_{1}\rangle\langle M_{2}\rangle\cdots\langle M_{k}\rangle$ if and only if

$\exists$ a chain $c_{1}\leq c_{2}\leq\cdots\leq c_{k+1}$ in $C$ and matrices $X_{1},\cdots,X_{k+1}\in\mathrm{GL}_{q}(\mathbb{F})\ :\ \forall i\in[k],\\ M_{i}\cdot X_{i}=X_{i+1}\cdot F(c_{i}\leq c_{i+1})$ .

By Theorem 10, such matrices $X_{1},\cdots,X_{k+1}$ can exist if and only if for all $1\leq i<i^{\prime}\leq k$ ,

\operatorname{rk}(M_{i}M_{i+1}\cdots M_{i^{\prime}-1})=\operatorname{rk}F(c_{i% }\leq c_{i^{\prime}})\ .

Since each $M_{i}$ is singular and $F(c\leq c)=\mathbf{I}_{q}$ for all $c\in C$ , we conclude that $c_{1},\cdots,c_{k+1}$ are distinct elements if the above condition is to be satisfied. Hence, we must have $c_{1}<c_{2}<\cdots<c_{k+1}$ , as desired. $\hfill\blacktriangleleft$

Now we are ready to prove $\mathsf{NP}$ -hardness for $\mathrm{posFF}$ .

Theorem 28.

$\mathrm{posFF}_{\mathbb{F}}$ is $\mathsf{NP}$ -hard for all fields $\mathbb{F}$ .

Proof.

We will give a polynomial-time reduction from Clique to $\mathrm{posFF}_{\mathbb{F}}$ . Given a simple undirected graph $G$ on the vertex set $[n]$ and a parameter $k$ , we have to decide whether $G$ has a $k$ -clique. Consider the simple undirected graph $G^{\prime}=([n+1],E^{\prime})$ where
$E^{\prime}=\{(i,j)\in[n+1]^{2}\ |\ i=n+1\text{ or }j=n+1\text{ or there is an % edge between vertex $i$ and $j$ in $G$}\}\ .$

Clearly, $G$ has a $k$ -clique if and only if $G^{\prime}$ has a $(k+1)$ -clique containing the vertex $(n+1)$ .

Now, apply Lemma 26 on the graph $G^{\prime}$ with the parameters $k+1$ and $n+1$ . Then we can construct in polynomial time a finitary diagram $F$ from a CLP $C=\{c_{i,j}\ |\ i\in[k+1],j\in[n+1]\}$ to a single-object category $A$ such that for all $1\leq i<i^{\prime}\leq k+1$ and $j,j^{\prime}\in[n+1]$ ,

\operatorname{rk}F(c_{i,j}\leq c_{i^{\prime},j^{\prime}})=f(i,i^{\prime},k+1,n% +1)-\mathbbm{1}_{(j,j^{\prime})\not\in E^{\prime}},

for some function $f:\mathbb{Z}^{4}\rightarrow\mathbb{Z}$ .

Notice that if we applied Lemma 26 on the complete graph on $(n+1)$ vertices instead with the same parameters, then we would obtain another finitary diagram $F^{\prime}$ from the same CLP $C$ to some single-object category $A^{\prime}$ such that for all $1\leq i<i^{\prime}\leq k+1$ and $j,j^{\prime}\in[n+1]$ ,

\operatorname{rk}F^{\prime}(c_{i,j}\leq c_{i^{\prime},j^{\prime}})=f(i,i^{% \prime},k+1,n+1),

because $(j,j^{\prime})$ would always be an edge. We use the second diagram $F^{\prime}$ to define the finitary formula in the $\mathrm{posFF}$ -instance we create, while the first diagram $F$ will be the diagram in it. Let us set $M_{i}:=F^{\prime}(c_{i,1}\leq c_{i+1,1})$ for $1\leq i\leq k$ . Then for all $1\leq i<i^{\prime}\leq k$ ,

\operatorname{rk}(M_{i}M_{i+1}\cdots M_{i^{\prime}-1})=\operatorname{rk}F^{% \prime}(c_{i,1}\leq c_{i^{\prime},1})=f(i,i^{\prime},k+1,n+1)\ .

Note that the single-object categories $A$ and $A^{\prime}$ generated in the above two applications of Lemma 26 may be different. However, with very slight modification in the proof of the lemma, we can ensure that $A$ and $A^{\prime}$ are equal to the same category $\{q\}$ . Hence, each $M_{i}$ is a $q\times q$ matrix.

Now define the object formula $S:=[q]\langle M_{1}\rangle\langle M_{2}\rangle\cdots\langle M_{k}\rangle$ . We claim that $F,c_{1,n+1}\models S$ iff $G^{\prime}$ has a $(k+1)$ -sized clique containing the vertex n+1.

Using Lemma 27, we have $F,c_{1,n+1}\models S$ iff there exists a chain $c_{1,b_{1}}=c_{1,n+1}<c_{2,b_{2}}<\cdots<c_{k+1,b_{k+1}}$ in $C$ (note that any chain of $k+1$ increasing elements in $C$ must pick exactly one element from each layer) such that for all $1\leq i<i^{\prime}\leq k$ ,

	$\displaystyle\operatorname{rk}(M_{i}M_{i+1}\cdots M_{i^{\prime}-1})=% \operatorname{rk}F(c_{i,b_{i}}\leq c_{i^{\prime},b_{i^{\prime}}}),$
	$\displaystyle\text{which means }f(i,i^{\prime},k+1,n+1)=f(i,i^{\prime},k+1,n+1% )-\mathbbm{1}_{(b_{i},b_{i^{\prime}})\not\in E^{\prime}},$
	$\displaystyle\text{which means }(b_{i},b_{i^{\prime}})\in E^{\prime}.$

Therefore, $F,c_{1,n+1}\models S$
iff there is a $(k+1)$ -clique in $G^{\prime}$ formed by the vertices $n+1,b_{2},b_{3},\cdots,b_{k+1}$
iff there is a $k$ -clique in $G$ formed by the vertices $b_{2},\cdots,b_{k+1}$ .

Hence, the problem Clique reduces to $\mathrm{posFF}_{\mathbb{F}}$ , making the latter $\mathsf{NP}$ -hard. $\hfill\blacktriangleleft$

8 Existential theory of special linear matrices

The (generalized) existential theory of special linear matrices is defined in the same way as the (generalized) existential theory of invertible matrices. The only difference is that we quantify over matrices with determinant equal to $1$ . Our efficient algorithm from Section 4 does not work in this situation, since the Schwartz-Zippel lemma can only test whether a polynomial is non-zero, but not whether there is an input at which it evaluates to $1$ . In fact, we will show that the generalized existential theory of special linear matrices $\mathrm{genETSLM}_{\mathbb{R}}$ is $\exists\mathbb{R}$ -complete.

First, we define the $\exists\mathbb{R}$ -complete problem $\mathrm{ETR}_{\mathrm{inv}}$ , which we will reduce to $\mathrm{genETSLM}_{\mathbb{R}}$ .

Definition 29.

In $\mathrm{ETR}_{\mathrm{inv}}$ , we are given formulae of the form $\exists x_{1}\dots\exists x_{n}:\,c_{1}\wedge c_{2}\wedge c_{3}\wedge\dots% \wedge c_{m}$ , where all $c_{i}$ are of one of the following forms:

x=1,\enspace x+y=z,\enspace x\cdot y=1

Here, $x, y$ and $z$ are arbitrary variables. The question is whether there exists an assignment of real nonzero values to the variables such that the given formula evaluates to true.

There are many variants of $\mathrm{ETR}_{\mathrm{inv}}$ known. To the best of our knowledge, the first one was defined by [1], see also [10, Problem L5–L7]. In contrast to our definition, [1] also requires that the domain of the variables is $[\frac{1}{2},2]$ .

Proposition 30.

$\mathrm{ETR}_{\mathrm{inv}}$ is $\exists\mathbb{R}$ -complete.

A self-contained proof of the above proposition can be found in the full version. Now we are ready to prove $\exists\mathbb{R}$ -hardness of $\mathrm{genETSLM}_{\mathbb{R}}$ . In fact, our proof will show that this is true even if we restrict ourselves to two kinds of linear equations in $\mathrm{genETSLM}_{\mathbb{R}}$ , namely matrix equations of the form $XA=BY$ and $XA=YB$ . It remains an interesting open question whether only the first type is sufficient to prove $\exists\mathbb{R}$ -hardness, that is, whether $\mathrm{ETSLM}_{\mathbb{R}}$ is already $\exists\mathbb{R}$ -complete.

8.1 Representing variables

We store variables using $2\times 2$ -matrices $\left(\begin{smallmatrix}x&r_{1}\\ r_{2}&x^{\prime}\end{smallmatrix}\right)$ . By adding the constraint

\displaystyle\begin{pmatrix}x&r_{1}\\ r_{2}&x^{\prime}\end{pmatrix}\begin{pmatrix}1&0\\ 0&0\end{pmatrix}

\displaystyle=\begin{pmatrix}1&0\\ 0&0\end{pmatrix}\begin{pmatrix}x&r_{1}\\ r_{2}&x^{\prime}\end{pmatrix},

which is equivalent to

\displaystyle\begin{pmatrix}x&0\\ r_{2}&0\end{pmatrix}

\displaystyle=\begin{pmatrix}x&r_{1}\\ 0&0\end{pmatrix},

we ensure that $r_{1}=r_{2}=0$ . $x$ and $x^{\prime}$ are not constrained by this equation. However, since we quantify over matrices of determinant $1$ , we get the additional constraint $xx^{\prime}=1$ . This ensures that $x$ can never be zero and also forces that $x^{\prime}$ is the inverse of $x$ .

8.2 Setting variables to $1$

We first show how to simulate equations of the type $x=1$ . For this, we have a special $1\times 1$ -matrix $E$ . Since we quantify only over matrices of determinant $1$ , simply quantifying over $E$ ensures $E=(1)$ . Now we take the $2\times 2$ -matrix $\left(\begin{smallmatrix}x&0\\ 0&x^{\prime}\end{smallmatrix}\right)$ that stores $x$ and add the constraint:

	$\displaystyle E\begin{pmatrix}1&0\end{pmatrix}$	$\displaystyle=\begin{pmatrix}1&0\end{pmatrix}\begin{pmatrix}x&0\\ 0&x^{\prime}\end{pmatrix}$
	$\displaystyle\iff\begin{pmatrix}1&0\end{pmatrix}$	$\displaystyle=\begin{pmatrix}x&0\end{pmatrix}$

This forces $x=1$ , and henceforth $x^{\prime}=1$ .

8.3 Equations of the form $xy=1$

Given the two representations of $x$ and $y$ , $\left(\begin{smallmatrix}x&0\\ 0&x^{\prime}\end{smallmatrix}\right)$ and $\left(\begin{smallmatrix}y&0\\ 0&y^{\prime}\end{smallmatrix}\right)$ , we need to ensure that $x=y^{\prime}$ , since we already know that $xx^{\prime}=1$ (and $yy^{\prime}=1$ ). This is achieved by the following constraint:

	$\displaystyle\begin{pmatrix}x&0\\ 0&x^{\prime}\end{pmatrix}\begin{pmatrix}0&1\\ 1&0\end{pmatrix}$	$\displaystyle=\begin{pmatrix}0&1\\ 1&0\end{pmatrix}\begin{pmatrix}y&0\\ 0&y^{\prime}\end{pmatrix}$
	$\displaystyle\iff\begin{pmatrix}0&x\\ x^{\prime}&0\end{pmatrix}$	$\displaystyle=\begin{pmatrix}0&y^{\prime}\\ y&0\end{pmatrix}\ .$

Note that the two equations $xx^{\prime}=1$ and $yy^{\prime}=1$ then also enforce $y=x^{\prime}$ , so the second constraint is automatically fulfilled.

8.4 Equations of the form $x+y=z$

The tricky part is to simulate the additions. For each addition, we have an extra variable $r$ , for which we set up a $2\times 2$ -matrix as above. Second, for each addition, we have a $4\times 4$ -matrix $H=(h_{i,j})$ over which we will quantify. The difficult part is to cope with the constraint that the determinant of $H$ has to be $1$ .

First we set up the equation

	$\displaystyle\begin{pmatrix}h_{1,1}&h_{1,2}&h_{1,3}&h_{1,4}\\ h_{2,1}&h_{2,2}&h_{2,3}&h_{2,4}\\ h_{3,1}&h_{3,2}&h_{3,3}&h_{3,4}\\ h_{4,1}&h_{4,2}&h_{4,3}&h_{4,4}\end{pmatrix}\begin{pmatrix}1&0\\ 0&0\\ 0&0\\ 0&0\end{pmatrix}$	$\displaystyle=\begin{pmatrix}1&0\\ 0&0\\ 0&0\\ 0&0\end{pmatrix}\begin{pmatrix}r&0\\ 0&r^{\prime}\end{pmatrix}$
	$\displaystyle\iff\begin{pmatrix}h_{1,1}&0\\ h_{2,1}&0\\ h_{3,1}&0\\ h_{4,1}&0\end{pmatrix}$	$\displaystyle=\begin{pmatrix}r&0\\ 0&0\\ 0&0\\ 0&0\end{pmatrix}.$

This constrains the first column of the matrix $H$ and leaves all other columns unconstrained. In a similar way, we constrain the second column:

	$\displaystyle\begin{pmatrix}h_{1,1}&h_{1,2}&h_{1,3}&h_{1,4}\\ h_{1,2}&h_{2,2}&h_{2,3}&h_{2,4}\\ h_{3,1}&h_{3,2}&h_{3,3}&h_{3,4}\\ h_{4,1}&h_{4,2}&h_{4,3}&h_{4,4}\end{pmatrix}\begin{pmatrix}0&0\\ 1&0\\ 0&0\\ 0&0\end{pmatrix}$	$\displaystyle=\begin{pmatrix}1&0\\ 1&0\\ 0&0\\ 0&0\end{pmatrix}\begin{pmatrix}x&0\\ 0&x^{\prime}\end{pmatrix}$
	$\displaystyle\iff\begin{pmatrix}h_{1,2}&0\\ h_{2,2}&0\\ h_{3,2}&0\\ h_{4,2}&0\end{pmatrix}$	$\displaystyle=\begin{pmatrix}x&0\\ x&0\\ 0&0\\ 0&0\end{pmatrix}.$

By adding two similar constraints for the third and the fourth column involving $y$ and $z$ , respectively, we can achieve that $H$ can only take the form

\displaystyle H

\displaystyle=\begin{pmatrix}r&x&y&z\\ 0&x&0&0\\ 0&0&y&0\\ 0&0&0&z\end{pmatrix}

(6)

The reason for this rather involved set of equations is that it ensures that $\det H=1$ can be achieved.

Observation 31.

1.

$\det H=rxyz$ .
2.

In any solution to the equations constructed so far, $x\not=0$ , $y\not=0$ , and $z\not=0$ .
3.

Since $r$ does not appear anywhere else, we can set $r=1/(xyz)$ to achieve $\det H=1$ .

We set up a second matrix $T$ similar to $H$ . We can take the same variable $r$ and also take the same set of equations, but we transpose each equation on both sides. Since the $2\times 2$ -matrices representing the variables are diagonal, they equal their transpose. Therefore, in any solution to the equations, $T$ will be the transpose of $H$ , i.e.,

\displaystyle T=H^{T}=\begin{pmatrix}r&0&0&0\\ x&x&0&0\\ y&0&y&0\\ z&0&0&z\end{pmatrix}.

In particular, $\det T=\det H=1$ . Finally, we set up the equation that simulates the addition using the matrices $H$ and $T$ . It is the only equation that is of the form $XA=YB$ .

	$\displaystyle\begin{pmatrix}r&x&y&z\\ 0&x&0&0\\ 0&0&y&0\\ 0&0&0&z\end{pmatrix}\begin{pmatrix}0\\ 1\\ 1\\ -1\end{pmatrix}$	$\displaystyle=\begin{pmatrix}r&0&0&0\\ x&x&0&0\\ y&0&y&0\\ z&0&0&z\end{pmatrix}\begin{pmatrix}0\\ 1\\ 1\\ -1\end{pmatrix}$		(7)
	$\displaystyle\iff\begin{pmatrix}x+y-z\\ x\\ y\\ -z\end{pmatrix}$	$\displaystyle=\begin{pmatrix}0\\ x\\ y\\ -z\end{pmatrix}\ .$

The equality of the first entries of the resulting vectors simulates the addition. Note that the equations of the other three entries are trivially satisfied, so they do not impose any new constraints on our variables.

Theorem 32.

$\mathrm{ETR}_{\mathrm{inv}}\leq_{\mathrm{P}}\mathrm{genETSLM}_{\mathbb{R}}$ .

Proof.

Assume that $\exists x_{1}\dots\exists x_{k}\,:c_{1}\wedge\dots\wedge c_{m}$ is a yes-instance of $\mathrm{ETR}_{\mathrm{inv}}$ . Let $\xi_{1},\dots,\xi_{k}$ be a satisfying assignment. For each variable $x_{i}$ , we set up a $2\times 2$ -matrix as in Section 8.1. If we set the diagonal entries to $\xi_{i}$ and $\xi_{i}^{-1}$ and the off-diagonal entries to $0$ , then the determinant is $1$ and the equations in Section 8.1 are satisfied. If we have an equation $x_{i}=1$ , then $\xi_{i}=1$ and the $2\times 2$ -matrix corresponding to $x_{i}$ satisfies the equations of Section 8.2 by construction. If we have an equation $c_{\mu}$ of the form $x_{i}x_{j}=1$ , then $\xi_{i}=1/\xi_{j}$ and the equations of Section 8.3 are again satisfied by construction. Finally, if we have an equation $c_{\mu}$ of the form $x_{i}+x_{j}=x_{h}$ , then we first set the values of $H$ as depicted in (6) (substituting $\xi_{i},\xi_{j},\xi_{h}$ for $x, y, z$ ). Since $\xi_{1},\dots,\xi_{k}$ is a feasible solution, all of them are nonzero. Therefore, we can choose $r$ in such a way that the determinant of $H$ is $1$ . $r$ is only used for this addition. The entries of the $2\times 2$ -matrix for $r$ are set as above. In the same way, we can choose the values for $T$ . Since $\xi_{i}+\xi_{j}=\xi_{h}$ also the equations $(\ref{eq:add})$ is satisfied. Thus we have a yes-instance for $\mathrm{genETSLM}_{\mathbb{R}}$ .

Conversely, assume that the $\mathrm{genETSLM}_{\mathbb{R}}$ -instance constructed above is a yes-instance. We claim that the values of the $(1,1)$ -entries $\xi_{i}$ of the $2\times 2$ -matrices corresponding to $x_{1},\dots,x_{k}$ are a satisfying solution to the $\mathrm{ETR}_{\mathrm{inv}}$ -instance. All $\xi_{i}$ are nonzero, since the determinants are $1$ . The equations $c_{1},\dots,c_{m}$ are all satisfied, since for each $c_{\mu}$ we set up a gadget that ensures this.

The reduction is obviously polynomial-time computable. $\hfill\blacktriangleleft$

Corollary 33.

$\mathrm{genETSLM}_{\mathbb{R}}$ is $\exists\mathbb{R}$ -complete.

9 Conclusions

In the present work, we settled the complexity of the model checking problem for finitary formulae ( $\mathsf{NP}$ -complete) and significantly improved the complexity of deciding bisimilarity in finitary diagrams ( $\mathsf{NEXP}$ in general and $\mathsf{PSPACE}$ for finite fields). We gave an efficient randomized algorithm for the (generalized) existential theory of invertible matrices over infinite fields, in particular over the reals. It is an interesting, but very difficult question whether we can derandomize this algorithm for $\mathrm{genETIM}_{\mathbb{R}}$ , since it is equivalent to the complement of symbolic determinant identity testing. Is the subproblem $\mathrm{ETIM}_{\mathbb{R}}$ equivalent to the complement of some identity testing problem? Or is there an efficient deterministic algorithm? In contrast to $\mathrm{genETIM}_{\mathbb{R}}$ , we proved that the generalized existential theory of special linear matrices is $\exists\mathbb{R}$ -complete. Is the existential theory of special linear matrices $\exists\mathbb{R}$ -hard, too?

References

[1] Mikkel Abrahamsen, Anna Adamaszek, and Tillmann Miltzow. The art gallery problem is $\exists$ $\mathbb{R}$ -complete. J. ACM, 69(1):4:1–4:70, 2022. doi:10.1145/3486220.
[2] John Canny. Some algebraic and geometric computations in PSPACE. In Proc. 20th Annual ACM Symposium on Theory of Computing (STOC), pages 460–467. ACM, 1988. doi:10.1145/62212.62257.
[3] Gunnar Carlsson and Afra Zomorodian. The theory of multidimensional persistence. Discrete and Computational Geometry, 42:71–93, June 2007. doi:10.1007/s00454-009-9176-0.
[4] Jérémy Dubut. Bisimilarity of diagrams. In Uli Fahrenberg, Peter Jipsen, and Michael Winter, editors, Relational and Algebraic Methods in Computer Science - 18th International Conference, RAMiCS 2020, Palaiseau, France, April 8-11, 2020, Proceedings [postponed], volume 12062 of Lecture Notes in Computer Science, pages 65–81. Springer, 2020. doi:10.1007/978-3-030-43520-2_5.
[5] Jérémy Dubut, Eric Goubault, and Jean Goubault-Larrecq. Natural homology. In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, volume 9135 of Lecture Notes in Computer Science, pages 171–183. Springer, 2015. doi:10.1007/978-3-662-47666-6_14.
[6] Matthew Hennessy and Robin Milner. On observing nondeterminism and concurrency. In Jacco de Bakker and Jan van Leeuwen, editors, Automata, Languages and Programming (ICALP 1980), volume 85 of Lecture Notes in Computer Science, pages 299–309. Springer, Berlin, Heidelberg, 1980. doi:10.1007/3-540-10003-2_79.
[7] André Joyal, Mogens Nielsen, and Glynn Winskel. Bisimulation from open maps. Information and Computation, 127(2):164–185, 1996. doi:10.1006/inco.1996.0057.
[8] Valentine Kabanets and Russell Impagliazzo. Derandomizing polynomial identity tests means proving circuit lower bounds. Comput. Complex., 13(1-2):1–46, 2004. doi:10.1007/S00037-004-0182-6.
[9] James Renegar. On the computational complexity and geometry of the first-order theory of the reals. Part I: Introduction. Preliminaries. The geometry of semi-algebraic sets. The decision problem for the existential theory of the reals. Journal of symbolic computation, 13(3):255–299, 1992. doi:10.1016/S0747-7171(10)80003-3.
[10] Marcus Schaefer, Jean Cardinal, and Tillmann Miltzow. The existential theory of the reals as a complexity class: A compendium. CoRR, abs/2407.18006, 2024. doi:10.48550/arXiv.2407.18006.
[11] Amir Shpilka and Amir Yehudayoff. Arithmetic circuits: A survey of recent results and open questions. Found. Trends Theor. Comput. Sci., 5(3-4):207–388, 2010. doi:10.1561/0400000039.

[bib.bib1] [1] Mikkel Abrahamsen, Anna Adamaszek, and Tillmann Miltzow. The art gallery problem is $\exists$ $\mathbb{R}$ -complete. J. ACM, 69(1):4:1–4:70, 2022. doi:10.1145/3486220.

[bib.bib2] [2] John Canny. Some algebraic and geometric computations in PSPACE. In Proc. 20th Annual ACM Symposium on Theory of Computing (STOC), pages 460–467. ACM, 1988. doi:10.1145/62212.62257.

[bib.bib3] [3] Gunnar Carlsson and Afra Zomorodian. The theory of multidimensional persistence. Discrete and Computational Geometry, 42:71–93, June 2007. doi:10.1007/s00454-009-9176-0.

[bib.bib4] [4] Jérémy Dubut. Bisimilarity of diagrams. In Uli Fahrenberg, Peter Jipsen, and Michael Winter, editors, Relational and Algebraic Methods in Computer Science - 18th International Conference, RAMiCS 2020, Palaiseau, France, April 8-11, 2020, Proceedings [postponed], volume 12062 of Lecture Notes in Computer Science, pages 65–81. Springer, 2020. doi:10.1007/978-3-030-43520-2_5.

[bib.bib5] [5] Jérémy Dubut, Eric Goubault, and Jean Goubault-Larrecq. Natural homology. In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, volume 9135 of Lecture Notes in Computer Science, pages 171–183. Springer, 2015. doi:10.1007/978-3-662-47666-6_14.

[bib.bib6] [6] Matthew Hennessy and Robin Milner. On observing nondeterminism and concurrency. In Jacco de Bakker and Jan van Leeuwen, editors, Automata, Languages and Programming (ICALP 1980), volume 85 of Lecture Notes in Computer Science, pages 299–309. Springer, Berlin, Heidelberg, 1980. doi:10.1007/3-540-10003-2_79.

[bib.bib7] [7] André Joyal, Mogens Nielsen, and Glynn Winskel. Bisimulation from open maps. Information and Computation, 127(2):164–185, 1996. doi:10.1006/inco.1996.0057.

[bib.bib8] [8] Valentine Kabanets and Russell Impagliazzo. Derandomizing polynomial identity tests means proving circuit lower bounds. Comput. Complex., 13(1-2):1–46, 2004. doi:10.1007/S00037-004-0182-6.

[bib.bib9] [9] James Renegar. On the computational complexity and geometry of the first-order theory of the reals. Part I: Introduction. Preliminaries. The geometry of semi-algebraic sets. The decision problem for the existential theory of the reals. Journal of symbolic computation, 13(3):255–299, 1992. doi:10.1016/S0747-7171(10)80003-3.

[bib.bib10] [10] Marcus Schaefer, Jean Cardinal, and Tillmann Miltzow. The existential theory of the reals as a complexity class: A compendium. CoRR, abs/2407.18006, 2024. doi:10.48550/arXiv.2407.18006.

[bib.bib11] [11] Amir Shpilka and Amir Yehudayoff. Arithmetic circuits: A survey of recent results and open questions. Found. Trends Theor. Comput. Sci., 5(3-4):207–388, 2010. doi:10.1561/0400000039.

The Complexity of Bisimilarity and Model Checking in Finitary Diagrams

Abstract

Keywords and phrases:

Category:

Copyright and License:

2012 ACM Subject Classification:

Related Version:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

1.1 Previous results

1.2 Our contributions

2 Preliminaries

2.1 Finitary diagrams

Definition 1 ([4]).

2.2 Bisimilarity

Definition 2.

Definition 3.

Proposition 4.

2.3 Diagrammatic path logic and finitary formulae

Proposition 5.

2.4 Existential theory of the reals

2.5 Existential theory of invertible matrices

2.6 Nondeterministic reductions

Definition 6.

Proposition 7.

Definition 8.

Proposition 9.

2.7 A tool from quiver theory and persistent homology

Theorem 10.

3 Overview of results and techniques

3.1 Existential theory of invertible matrices

Theorem I (Theorem 12).

Proof overview.

Theorem II (Theorem 15).

Proof overview.

3.2 First results through our algorithm for ETIM

Theorem III (Corollary 18).

Theorem IV (Corollary 23).

3.3 Complexity of bisimilarity checking for finitary diagrams

Theorem V (Theorem 21).

Proof overview.

3.4 Complexity of model checking for finitary formulae

Theorem VI (Theorem 28).

Proof overview.

3.5 Existential theory of special linear matrices

Theorem VII (Corollary 33).

Proof overview.

4 An efficient algorithm for the existential theory of invertible matrices

Lemma 11 (Schwartz-Zippel).

Theorem 12.

Proof.

Corollary 13.

Corollary 14.

Theorem 15.

Proof.

5 An improved algorithm for bisimilarity

Proposition 16 (implicit in [4]).

Lemma 17.

Proof.

Corollary 18.

6 A PSPACE upper bound for bisimilarity over finite fields

Lemma 19.

Proof.

Lemma 20.

Proof.

Theorem 21.

Proof.

7 Complexity of model checking for finitary diagrams

Theorem 22.

Proof.

Corollary 23.

Definition 24 (Constrained Layered Poset (CLP)).

Lemma 25.

Proof.

The poset.

The universe.

Labels.

8.2 Setting variables to $1$

8.3 Equations of the form $xy=1$

8.4 Equations of the form $x+y=z$