Refinement is complete for implementations
Refinement is complete for implementations
复制标题
实施细化已完成
作者：
M. Huth
模态转换系统通过Larsen & Bethesen的共归纳精化概念指定了实现的集合，它们的精化标记了转换系统。我们证明，细化精确地捕捉到一个模态转换系统的识别与它的一组实现：细化是反向包含的实现集。这一结果扩展到模型，结合联合收割机状态和事件的可观的，是从SFP域的元素是等价类的模态转换系统下细化[HJS 04]，和抽象为基础的有限模型的性质证明了本文。作为一个推论，有效性检查是Hennessy-Milner公式的模型检查，该公式表征具有有界计算路径的模态转换系统。最后，我们勾勒出如何在本文中开发的技术可以用来检测多个模态转换系统之间的不一致，如果一致，验证所有常见的实现属性。
Modal transition systems specify sets of implementations, their refining labelled transition systems, through Larsen & Thomsen’s co-inductive notion of refinement. We demonstrate that refinement precisely captures the identification of a modal transition system with its set of implementations: refinement is reverse containment of sets of implementations. This result extends to models that combine state and event observables and is drawn from a SFP-domain whose elements are equivalence classes of modal transition systems under refinement [HJS04], and abstraction-based finite-model properties proved in this paper. As a corollary, validity checking is model checking for Hennessy-Milner formulas that characterize modal transition systems with bounded computation paths. We finally sketch how techniques developed in this paper can be used to detect inconsistencies between multiple modal transition systems and, if consistent, to verify properties of all common implementations.