2018/09/25 by Dubut, Jérémy, Hasuo, Ichiro, Katsumata, Shin-ya +1
#F.1.2 #F.1.7 #F.8 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.1809.09278
We investigate a canonical way of defining bisimilarity of systems when their semantics is given by a coreflection, typically in a category of transition systems. We use the fact, from Joyal et al., that coreflections preserve open morphisms situations in the sense that a coreflection induces a path subcategory in the category of systems in such a way that open bisimilarity with respect to the induced path category coincides with usual bisimilarity of their semantics. We prove that this method is particularly well-suited for systems with quantitative information: we canonically recover the path category of probabilistic systems from Cheng et al., and of timed systems from Nielsen et al., and, finally, we propose a new canonical path category for hybrid systems.