Covariant-Contravariant Refinement Modal $\mu$-calculus

TL;DR

This paper introduces a new modal $oldsymbol{ ext{μ}}$-calculus based on covariant-contravariant refinement, extending existing modal logic systems to better specify properties of reactive and generative systems.

Contribution

It defines CCRML$^{ ext{μ}}$, establishes its axiom system, and proves soundness, completeness, and decidability, advancing formal methods for system property specification.

Findings

Introduces CCRML$^{ ext{μ}}$ with CC-refinement quantifiers

Provides an axiom system for CCRML$^{ ext{μ}}$

Proves soundness, completeness, and decidability of the system

Abstract

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. It may be used to formalize some interesting problems in the field of formal methods.