Covariant-Contravariant Refinement Modal $\mu$-calculus. (arXiv:2208.02989v1 [cs.LO])

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 $\mu$-calculus (CCRML$^{\mu}$)
obtained from the modal $\mu$-calculus system K$^{\mu}$ by adding CC-refinement
quantifiers, establishes an axiom system for CCRML$^{\mu}$ and explores the
important properties: soundness, completeness and decidability of this axiom
system. The language of CCRML$^{\mu}$ may be considered as a specification
language for describing the properties of a system referring to reactive and
generative actions. …

arxiv calculus