# Covariant-Contravariant Refinement Modal μ-calculus

arXiv: https://arxiv.org/abs/2208.02989 · HTML: https://mlsanity.com/paper/2208.02989/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 0 of its 18 references that are in the map.
- First posted on arXiv 5 Aug 2022.

## Abstract (arXiv)

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.