图的互模拟
计算机科学中的逻辑
2020-06-08 v2
摘要
在本文中，我们研究图（diagram），即从任意小范畴到固定范畴的函子，特别是它们的互模拟性。最初使用 Joyal 等人的开放映射理论定义，我们证明了几个等价刻画：它等价于一个关系的存在，类似于事件结构的保历史互模拟，并且它具有类似于 Hennessy-Milner 定理的逻辑刻画。然后，通过考虑执行和执行的扩展的范畴，并形成将每个执行映射到当前问题所关注信息的函子，我们证明捕获了许多不同的已知互模拟。接着，我们考察了取值为实数或有理数向量空间的有限图的特殊情况。我们证明，通过将其归约为在线性条件下可逆矩阵存在性的问题，进而归约至实数的存在性理论，检查图的互模拟性和正公式可满足性均是可判定的。
引用
@article{arxiv.1804.10886,
title = {Bisimilarity of diagrams},
author = {Jérémy Dubut},
journal= {arXiv preprint arXiv:1804.10886},
year = {2020}
}