Game-theoretic characterizations of process equivalences traditionally form a central topic in concurrency; for example, most equivalences on the classical linear-time / branching-time spectrum come with such characterizations. Recent work on so-called graded semantics has led to a generic behavioural equivalence game that covers the mentioned games on the linear-time~/ branching-time spectrum and moreover applies in coalgebraic generality, and thus instantiates also to equivalence games on systems with non-relational branching type (probabilistic, weighted, game-based etc.). In the present work, we generalize this approach to cover other types of process comparison beyond equivalence, such as behavioural preorders or pseudometrics. At the most general level, we abstract such notions of behavoiural conformance in terms of topological categories, and later specialize to conformances presented as relational structures to obtain a concrete syntax. We obtain a sound and complete generic game for behavioural conformances in this sense. We present a number of instantiations, obtaining game characterizations of, e.g., trace inclusion, probabilistic trace distance, bisimulation topologies, and simulation distances on metric labelled transition systems.
翻译:过程等价的博弈论刻画传统上是并发理论的核心课题;例如,经典线性时间/分支时间谱上的大多数等价关系都具备此类刻画。近期关于所谓分级语义的研究导出了一个通用的行为等价博弈,该博弈不仅涵盖了线性时间/分支时间谱上的既有博弈,更在余代数层面具有普适性,因而可实例化为非关系分支类型系统(概率型、加权型、博弈型等)上的等价博弈。本文工作中,我们将此方法推广至涵盖等价关系之外的其他过程比较类型,如行为预序或伪度量。在最广义层面,我们通过拓扑范畴对行为符合性概念进行抽象,随后特化为以关系结构呈现的符合性以获得具体语法。由此我们得到了此类行为符合性的一个可靠且完备的通用博弈。我们给出了若干实例化案例,获得了诸如迹包含、概率迹距离、度量标记转移系统上的互模拟拓扑及模拟距离等概念的博弈刻画。