Bisimilarity of diagrams

TL;DR

This paper explores the concept of bisimilarity in diagrams, providing multiple characterizations, unifying various known bisimilarities, and demonstrating decidability results for diagrams with vector space values.

Contribution

It introduces new equivalent characterizations of bisimilarity for diagrams, unifies different bisimilarities under a common framework, and proves decidability for diagrams valued in vector spaces.

Findings

Bisimilarity characterized via relations similar to history-preserving bisimulations.

Logical characterization of bisimilarity akin to Hennessy-Milner theorem.

Decidability of bisimilarity for vector space-valued diagrams via linear algebra.

Abstract

In this paper, we investigate diagrams, namely functors from any small category to a fixed category, and more particularly, their bisimilarity. Initially defined using the theory of open maps of Joyal et al., we prove several equivalent characterizations: it is equivalent to the existence of a relation, similar to history-preserving bisimulations for event structures and it has a logical characterization similar to the Hennessy-Milner theorem. We then prove that we capture many different known bismilarities, by considering the category of executions and extensions of executions, and by forming the functor that maps every execution to the information of interest for the problem at hand. We then look at the particular case of finitary diagrams with values in real or rational vector spaces. We prove that checking bisimilarity and satisfiability of a positive formula by a diagram are both decidable by reducing to a problem of existence of invertible matrices with linear conditions, which in turn reduces to the existential theory of the reals.