输入输出一致性模拟的逻辑刻画、规则格式与组合性
Logical characterisations, rule formats and compositionality for input-output conformance simulation
AI总结：
本文为输入输出一致性模拟（iocos）发展理论，给出其模态逻辑刻画、特征公式构造、预同余规则格式，并利用模态分解方法实现组合性验证。
摘要：
输入输出一致性模拟（iocos）由Gregorio-Rodríguez、Llana和Martínez-Torres提出，作为一种基于模拟的行为预序，用于基于模型的测试。该关系受Tretmans经典ioco关系的启发，但其最坏情况复杂度优于ioco，并支持逐步细化。本文的目标是通过研究该关系的逻辑刻画、规则格式及其组合性来发展iocos理论。具体而言，本文以模态逻辑的形式给出了iocos的刻画，并将其与Beohar和Mousavi提出的现有ioco逻辑刻画进行比较。本文还在所提出的模态逻辑的扩展中加入最大不动点，为有限过程上的iocos提供了特征公式构造。此外，本文给出了iocos的预同余规则格式，以及确保操作正确考虑静止（quiescence）的规则格式。这两种规则格式均基于Bloom、Istrail和Meyer的GSOS格式。本文使用Fokkink和van Glabbeek的通用模态分解方法，展示了如何以组合方式检查由iocos预同余规则格式中的规则所指定的操作是否满足iocos逻辑中表达的属性。
英文摘要：
Input-output conformance simulation (iocos) has been proposed by Gregorio-Rodríguez, Llana and Martínez-Torres as a simulation-based behavioural preorder underlying model-based testing. This relation is inspired by Tretmans' classic ioco relation, but has better worst-case complexity than ioco and supports stepwise refinement. The goal of this paper is to develop the theory of iocos by studying logical characterisations of this relation, rule formats for it and its compositionality. More specifically, this article presents characterisations of iocos in terms of modal logics and compares them with an existing logical characterisation for ioco proposed by Beohar and Mousavi. It also offers a characteristic-formula construction for iocos over finite processes in an extension of the proposed modal logics with greatest fixed points. A precongruence rule format for iocos and a rule format ensuring that operations take quiescence properly into account are also given. Both rule formats are based on the GSOS format by Bloom, Istrail and Meyer. The general modal decomposition methodology of Fokkink and van Glabbeek is used to show how to check the satisfaction of properties expressed in the logic for iocos in a compositional way for operations specified by rules in the precongruence rule format for iocos .
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
