Covariant-Contravariant Refinement Modal $μ$-calculus
This work provides a specification language for formal methods, addressing properties of systems with reactive and generative actions, but it appears incremental as it builds on existing modal μ-calculus frameworks.
The paper tackles the problem of generalizing bisimulation, simulation, and refinement by introducing CC-refinement modal μ-calculus (CCRML^μ), establishing an axiom system with soundness, completeness, and decidability properties.
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.