Automata acceptance can, in several situations of interest, be captured game-theoretically via acceptance games. The existence of a winning strategy for Verifier then captures the existence of a winning run-tree of a given automaton over a model. However, such acceptance is rigid, in that it does not allow a measurable defect budget, which can be a challenge in software verification. In this paper, we draw inspiration from how bisimulation distance can be defined as an extension of bisimilarity to define epsilon-acceptance games. Our main theorem shows that a tree T is epsilon-accepted iff there is a tree T' that is accepted in the traditional (rigid) sense and the bisimulation distance of T' and T is at most epsilon. Our work also suggests a strong connection with measure theory, of which we give a preliminary exploration via appropriate examples. Our framework is defined over binary trees with leaves and infinite branches, and strictly contains the case in which binary nodes are seen as probabilistic choice and the defect measures the probability of the set of rejected branches.

翻译：摘要：自动机接受性在多种重要场景中可通过接受博弈的博弈论框架加以刻画。验证者存在获胜策略对应着给定自动机在模型上存在获胜运行树。然而这种接受性是刚性的，不允许存在可测量的缺陷预算，这在软件验证中可能构成挑战。本文借鉴双模拟距离作为双模拟关系扩展的定义方式，提出ε-接受博弈。主要定理表明：树T被ε-接受当且仅当存在一棵在传统（刚性）意义上被接受的树T'，且T'与T的双模拟距离不超过ε。本文还揭示了与测度论之间的强关联，并通过适当示例进行了初步探索。该框架定义于带叶子和无穷分支的二叉树上，严格涵盖了将二叉节点视为概率选择、缺陷度量被拒绝分支集概率的情形。