We provide a fine classification of bisimilarities between states of possibly different labelled Markov processes (LMP). We show that a bisimilarity relation proposed by Panangaden that uses direct sums coincides with "event bisimilarity" from his joint work with Danos, Desharnais, and Laviolette. We also extend Giorgio Bacci's notions of bisimilarity between two different processes to the case of nondeterministic LMP and generalize the game characterization of state bisimilarity by Clerc et al. for the latter.
翻译:我们针对可能不同的标号马尔可夫过程(LMP)的状态间互模拟关系,提供了一种精细的分类。研究证明,Panangaden提出的基于直和的互模拟关系,与其与Danos、Desharnais及Laviolette合作研究中定义的“事件互模拟”等价。同时,我们将Giorgio Bacci关于两个不同过程间互模拟的概念扩展至非确定性LMP情形,并推广了Clerc等人针对后者提出的状态互模拟博弈刻画方法。