2022/08/05 by Xing, Huili
#Computation and Language (cs.CL) #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.2208.02989
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.