论文标题
协变量对抗性改进模态$μ$ -calculus
Covariant-Contravariant Refinement Modal $μ$-calculus
论文作者
论文摘要
协变量对比度的改进（简称CC-进行）的概念是对双性仿真，模拟和改进的概念的概括。本文介绍了从模态$ $ $ $ $ -CALCULUS SYSTEM K $^μ$获得的CC-REFINEMENT $ $ $ -CALCULUS（CCRML $^μ$），通过添加CC-REFINEMENT量化器来建立CCRML $ $ $ $的Axiom System，并探索了重要的属性，并确定了重要的属性，并探索了重要的属性。 CCRML $^μ$的语言可以被视为一种规范语言，用于描述指代反应性和生成动作的系统的属性。它可以用来形式化正式方法领域中一些有趣的问题。
The notion of covariant-contravariant refinement (CC-refinement, for short) is a generalization of the notions of bisimulation, simulation and refinement. This paper introduces CC-refinement modal $μ$-calculus (CCRML$^μ$) obtained from the modal $μ$-calculus system K$^μ$ by adding CC-refinement quantifiers, establishes an axiom system for CCRML$^μ$ and explores the important properties: soundness, completeness and decidability of this axiom system. The language of CCRML$^μ$ may be considered as a specification language for describing the properties of a system referring to reactive and generative actions. It may be used to formalize some interesting problems in the field of formal methods.
