用于约束和精化的交替关系
Relating Alternating Relations for Conformance and Refinement
摘要：
对于具有输入和输出的状态转换系统，已经定义了各种关系来表示精化和一致性，例如基于模型的测试领域中的ioco和uioco，以及源自博弈论和形式化验证的交替模拟和交替跟踪包含。几篇论文比较了这些独立开发的关系，但这些比较做出了假设（例如，输入使能性），造成限制（例如，决定论-那么它们都一致），使用不同的模型（例如，接口自动机和Kripke结构），或者不处理静止的概念。在本文中，我们提出了集成的ioco/uioco理论的基于模型的测试和理论的交替细化，在域的非确定性，非输入启用接口自动机。一个长期的猜测是ioco和交替跟踪遏制一致。我们的主要结果是，这个猜想并不成立，但uioco符合交替跟踪包容的一个变种，图像有限接口自动机和明确的治疗静止。从ioco理论和交替细化之间的比较，我们得出结论，ioco和原来的关系的交替跟踪包含是太强的现实黑盒场景。本文提出了一个精化关系，它既能表示博弈论中的uioco，又能表示精化，而且更简单，具有更清晰的观察解释。
英文摘要：
Various relations have been defined to express refinement and conformance for state-transition systems with inputs and outputs, such as ioco and uioco in the area of model-based testing, and alternating simulation and alternating-trace containment originating from game theory and formal verification. Several papers have compared these independently developed relations, but these comparisons make assumptions (e.g., input-enabledness), pose restrictions (e.g., determinism - then they all coincide), use different models (e.g., interface automata and Kripke structures), or do not deal with the concept of quiescence. In this paper, we present the integration of the ioco/uioco theory of model-based testing and the theory of alternating refinements, within the domain of non-deterministic, non-input-enabled interface automata. A standing conjecture is that ioco and alternating-trace containment coincide. Our main result is that this conjecture does not hold, but that uioco coincides with a variant of alternating-trace containment, for image finite interface automata and with explicit treatment of quiescence. From the comparison between ioco theory and alternating refinements, we conclude that ioco and the original relation of alternating-trace containment are too strong for realistic black-box scenarios. We present a refinement relation which can express both uioco and refinement in game theory, while being simpler and having a clearer observational interpretation.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
