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.

翻译：受Dubut、Goubault和Goubault-Larrecq（ICALP 2015）关于自然同调的工作启发，Dubut（RAMiCS 2020）引入了有限图并研究了其中的互模拟和图示路径逻辑。为此，他定义了实数存在性理论的一个片段，称为可逆矩阵存在性理论（ETIM）。利用该片段的PSPACE上界，他证明了对于有限图，互模拟可在EXPSPACE内判定，而图示路径逻辑的模型检测可在PSPACE内完成。我们显著改进了这两个界，并彻底解决了有限图模型检测的复杂度问题。作为第一个主要结果，我们展示了ETIM存在一个高效随机化算法。结合Dubut先前的工作，我们得到了有限图互模拟的NEXP上界和图示路径逻辑的NP上界。我们还为后者提供了匹配的NP-困难性证明。该困难性证明引入了约束分层偏序集问题（可能具有独立研究价值），并通过路径箭图表示的Gabriel定理将其与有限图关联起来。对于有限域上的互模拟，我们进一步将上界改进为PSPACE。在ETIM中，我们对可逆矩阵进行量词化。最后，我们探讨若将量词化对象改为特殊线性群中的矩阵（即行列式为1的矩阵）会如何。我们证明，在此情况下，所得片段在允许线性约束的适当推广下等价于实数存在性理论。