双仿和抽象的游戏
摘要：用于进程代数的弱相似性通常使用静默步骤来抽象出内部行为。它们有助于将实现与规范相关联。当实现与其规范不一致时，确定根本原因可能具有挑战性。在本文中，我们提供了一个通用的分支-延迟-$eta$-和弱相似性的游戏化特征，作为Spoiler和Duplicator之间的游戏，以提供对关系的操作理解。我们展示了这些游戏如何在诊断实现与规范不一致方面发挥作用。此外，我们还展示了如何扩展这些游戏以区分发散现象。
作者：David De Frutos Escrig, Jeroen J.A. Keiren and Tim A.C. Willemse
论文ID：1611.00401
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22