TY - GEN
T1 - Bisimilarity of Diagrams
AU - Dubut, Jérémy
N1 - Publisher Copyright:
© 2020, Springer Nature Switzerland AG.
PY - 2020/1/1
Y1 - 2020/1/1
N2 - 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 two characterisations of this bisimilarity: it is equivalent to the existence of a bisimulation-like relation and has a logical characterisation à la Hennessy and Milner. We then prove that we capture both path bisimilarity and strong path bisimilarity of any small open maps situation. 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.
AB - 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 two characterisations of this bisimilarity: it is equivalent to the existence of a bisimulation-like relation and has a logical characterisation à la Hennessy and Milner. We then prove that we capture both path bisimilarity and strong path bisimilarity of any small open maps situation. 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.
KW - Diagrams
KW - Existential theories
KW - Open maps
KW - Path logic
UR - https://www.scopus.com/pages/publications/85083956494
U2 - 10.1007/978-3-030-43520-2_5
DO - 10.1007/978-3-030-43520-2_5
M3 - Conference contribution
AN - SCOPUS:85083956494
SN - 9783030435196
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 65
EP - 81
BT - Relational and Algebraic Methods in Computer Science - 18th International Conference, RAMiCS 2020, Proceedings
A2 - Fahrenberg, Uli
A2 - Jipsen, Peter
A2 - Winter, Michael
PB - Springer
T2 - 18th International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS 2020
Y2 - 8 April 2020 through 11 April 2020
ER -