Covariant-Contravariant Refinement Modal $μ$-calculus
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Unified Functorial Signal Representation III: Foundations, Redundancy, $L^0$ and $L^2$ functors
In this paper we propose and lay the foundations of a functorial framework for representing signals. By incorporating additional category-theoretic relative and generative perspective alongside the classic set-theoretic …
TranslationLearning Manifold and Itô Dynamics with Branched Neural Rough Differential Equations
Neural rough differential equations (NRDEs) stay accurate under irregular sampling while taking far fewer integration steps than standard neural differential equations, summarising a finely sampled driver by its log-sign…
Refinement Modal Logic
In this paper we present {\em refinement modal logic}. A refinement is like a bisimulation, except that from the three relational requirements only `atoms' and `back' need to be satisfied. Our logic contains a new operat…
AllZX-Calculus:Trace-Indexed Dependent Types and Epistemic Semantics
We propose ZX-Calculus (Knowledge Evolution Calculus), a conservative extension of Martin-Lof Dependent Type Theory (MLTT) integrating trace-indexed types, presheaf non-monotone semantics, and constructive AGM belief rev…
Towards Large Language Model Aided Program Refinement
Program refinement involves correctness-preserving transformations from formal high-level specification statements into executable programs. Traditional verification tool support for program refinement is highly interact…
HumanEvalLanguage ModelingLanguage ModellingLarge Language Model+1