A Logic of Secrecy on Simplicial Models

TL;DR

This paper introduces a new logic of secrecy for multi-agent systems modeled by simplicial complexes, enriching standard models with agent-specific secrecy neighborhoods and providing a sound and complete axiomatization.

Contribution

It develops simplicial secrecy models with a new secrecy operator, extending knowledge semantics to capture local-state-based secrecy in a geometric framework.

Findings

Defines simplicial secrecy models with neighborhood functions.

Introduces a primitive secrecy operator $S_a$ with semantic conditions.

Proves soundness and completeness of the logic $ extsf{SSL}$ for multi-agent secrecy.

Abstract

We develop a logic of secrecy on simplicial models for multi-agent systems. Standard simplicial models provide a geometric semantics for knowledge by representing global states as facets of a chromatic simplicial complex and agents' local states as coloured vertices. However, secrecy cannot in general be captured as a genuinely new modality by relying on the ordinary simplicial knowledge structure alone. This motivates the introduction of an additional secrecy layer. To this end, we define \emph{simplicial secrecy models}, which enrich standard simplicial epistemic models with agent-relative secrecy neighborhood functions attached to local states. On this basis, we introduce a primitive secrecy operator $S_a\varphi$. Semantically, $S_a\varphi$ holds when agent $a$ knows $\varphi$ in the ordinary simplicial sense and, moreover, the truth set of $\varphi$ belongs to one of the designated secrecy neighborhoods associated with $a$'s current local state. The clause for secrecy thus combines an ordinary knowledge requirement with an additional local-state-based neighborhood requirement, while the frame condition ensures that designated secrecy events remain non-trivial from the perspective of every other agent. We formulate a system $\mathsf{SSL}$ for the resulting language and show that it is sound with respect to the class of simplicial secrecy models. For the genuinely multi-agent case $|A|\ge 2$, we prove completeness by first constructing an auxiliary-colour canonical model and then representing it inside the original class of pure $A$-chromatic simplicial secrecy models. The resulting framework yields a primitive, local-state-based, and geometrically grounded account of secrecy on simplicial models, together with a sound axiomatization and, in the genuinely multi-agent case, a complete one.