DROPS

Document

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

DOI: 10.4230/LIPIcs.ICALP.2026.166

The Complexity of Bisimilarity and Model Checking in Finitary Diagrams

Authors: Markus Bläser, Sagnik Dutta, and Samuel Okyay

Published in: LIPIcs, Volume 374, 53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026)

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.

Cite as

Markus Bläser, Sagnik Dutta, and Samuel Okyay. The Complexity of Bisimilarity and Model Checking in Finitary Diagrams. In 53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 374, pp. 166:1-166:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{blaser_et_al:LIPIcs.ICALP.2026.166,
  author =	{Bl\"{a}ser, Markus and Dutta, Sagnik and Okyay, Samuel},
  title =	{{The Complexity of Bisimilarity and Model Checking in Finitary Diagrams}},
  booktitle =	{53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026)},
  pages =	{166:1--166:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-428-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{374},
  editor =	{Bhattacharya, Sayan and Nanongkai, Danupon and Benedikt, Michael and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2026.166},
  URN =		{urn:nbn:de:0030-drops-265548},
  doi =		{10.4230/LIPIcs.ICALP.2026.166},
  annote =	{Keywords: Bisimilarity, Finitary diagrams, Model checking, Existential Theory of the Reals}
}

Document

DOI: 10.4230/LIPIcs.MFCS.2022.18

Improved Lower Bound, and Proof Barrier, for Constant Depth Algebraic Circuits

Authors: C. S. Bhargav, Sagnik Dutta, and Nitin Saxena

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract

We show that any product-depth Δ algebraic circuit for the Iterated Matrix Multiplication Polynomial IMM_{n,d} (when d = O(log n/log log n)) must be of size at least n^Ω(d^{1/(φ²)^Δ}) where φ = 1.618… is the golden ratio. This improves the recent breakthrough result of Limaye, Srinivasan and Tavenas (FOCS'21) who showed a super polynomial lower bound of the form n^Ω(d^{1/4^Δ}) for constant-depth circuits. One crucial idea of the (LST21) result was to use set-multilinear polynomials where each of the sets in the underlying partition of the variables could be of different sizes. By picking the set sizes more carefully (depending on the depth we are working with), we first show that any product-depth Δ set-multilinear circuit for IMM_{n,d} (when d = O(log n)) needs size at least n^Ω(d^{1/φ^Δ}). This improves the n^Ω(d^{1/2^Δ}) lower bound of (LST21). We then use their Hardness Escalation technique to lift this to general circuits. We also show that our lower bound cannot be improved significantly using these same techniques. For the specific two set sizes used in (LST21), they showed that their lower bound cannot be improved. We show that for any d^o(1) set sizes (out of maximum possible d), the scope for improving our lower bound is minuscule: there exists a set-multilinear circuit that has product-depth Δ and size almost matching our lower bound such that the value of the measure used to prove the lower bound is maximum for this circuit. This results in a barrier to further improvement using the same measure.

Cite as

C. S. Bhargav, Sagnik Dutta, and Nitin Saxena. Improved Lower Bound, and Proof Barrier, for Constant Depth Algebraic Circuits. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 18:1-18:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bhargav_et_al:LIPIcs.MFCS.2022.18,
  author =	{Bhargav, C. S. and Dutta, Sagnik and Saxena, Nitin},
  title =	{{Improved Lower Bound, and Proof Barrier, for Constant Depth Algebraic Circuits}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{18:1--18:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.18},
  URN =		{urn:nbn:de:0030-drops-168161},
  doi =		{10.4230/LIPIcs.MFCS.2022.18},
  annote =	{Keywords: polynomials, lower bounds, algebraic circuits, proof barrier, fibonacci numbers}
}

Search Results

Documents authored by Dutta, Sagnik

The Complexity of Bisimilarity and Model Checking in Finitary Diagrams

Abstract

Cite as

Improved Lower Bound, and Proof Barrier, for Constant Depth Algebraic Circuits

Abstract

Cite as

Thanks for your feedback!

Could not send message