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 operator 'all' in
addition to the standard modalities 'box' for each agent. The operator 'all'
acts as a quantifier over the set of all refinements of a given model. As a
variation on a bisimulation quantifier, this refinement operator or refinement
quantifier 'all' can be seen as quantifying over a variable not occurring in
the formula bound by it. The logic combines the simplicity of multi-agent modal
logic with some powers of monadic second-order quantification. We present a
sound and complete axiomatization of multi-agent refinement modal logic. We
also present an extension of the logic to the modal mu-calculus, and an
axiomatization for the single-agent version of this logic. Examples and
applications are also discussed: to software verification and design (the set
of agents can also be seen as a set of actions), and to dynamic epistemic
logic. We further give detailed results on the complexity of satisfiability,
and on succinctness.
Code (0)
등록된 구현이 없습니다.
Tasks
AllSimilar Papers 제목 키워드 기반
MultiVis-Agent: A Multi-Agent Framework with Logic Rules for Reliable and Comprehensive Cross-Modal Data Visualization
Real-world visualization tasks involve complex, multi-modal requirements that extend beyond simple text-to-chart generation, requiring reference images, code examples, and iterative refinement. Current systems exhibit fu…
Refining Labelled Systems for Modal and Constructive Logics with Applications
This thesis introduces the "method of structural refinement", which serves as a means of transforming the relational semantics of a modal and/or constructive logic into an 'economical' proof system by connecting two proo…
Unimodal and Crossmodal Refinement Network for Multimodal Sequence Fusion
Effective unimodal representation and complementary crossmodal representation fusion are both important in multimodal representation learning. Prior works often modulate one modal feature to another straightforwardly and…
Representation LearningCoarse-to-Fine Non-rigid Multi-modal Image Registration for Historical Panel Paintings based on Crack Structures
Art technological investigations of historical panel paintings rely on acquiring multi-modal image data, including visual light photography, infrared reflectography, ultraviolet fluorescence photography, x-radiography, a…
Graph Neural NetworkKeypoint DetectionImage RegistrationCovariant-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$^…