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