The Complexity of Bisimilarity and Model Checking in Finitary Diagrams (opens in new tab)

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 ...