论文标题
在煤堡方法中解释非三个相似性：游戏和区分公式
Explaining Non-Bisimilarity in a Coalgebraic Approach: Games and Distinguishing Formulas
论文作者
论文摘要
行为等效性可以通过双仿真，模态逻辑和扰流器 - 绘制器游戏来表征。在本文中，我们在山地的一般环境中工作，并专注于一般算法，用于计算两者中两名玩家的获胜策略。然后，扰流板的获胜策略（如果存在的话）被转变为一种区分给定非生物态状态的模态公式。公式所需的方式也可以在直觉上合成，我们提出了一种以不同方式来重新编码公式的食谱，该方法由一组分离的谓词举起给出。游戏和产生的区分公式都在一种称为T-BEG的工具中实现。
Behavioural equivalences can be characterized via bisimulation, modal logics, and spoiler-duplicator games. In this paper we work in the general setting of coalgebra and focus on generic algorithms for computing the winning strategies of both players in a bisimulation game. The winning strategy of the spoiler (if it exists) is then transformed into a modal formula that distinguishes the given non-bisimilar states. The modalities required for the formula are also synthesized on-the-fly, and we present a recipe for re-coding the formula with different modalities, given by a separating set of predicate liftings. Both the game and the generation of the distinguishing formulas have been implemented in a tool called T-BEG.
