Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Dynamic Logic of Trust-Based Beliefs

Junli Jiang, Pavel Naumov, Wenxuan Zhang

TL;DR

This work develops a dynamic logic for trust-based beliefs where data-informed knowledge $K_X$ and trust-modulated beliefs $B^T_X$ interact with public data announcements $[X]$. It introduces a sound and complete axiomatisation, including a non-trivial Commutativity axiom $[Y] B^T_X φ ↔ B^T_{Y∪X}[Y] φ$, and a ternary semantics $w,U ⊨ φ$ to capture how publicly announced data affects belief under trust. A canonical tree-based model proves completeness, and a polynomial-time model-checking algorithm is provided, enabling scalable reasoning about data-driven beliefs in multi-agent settings. The framework is illustrated with data- and trust-centric scenarios such as public AP tweets influencing automated trading, offering formal tools for data-driven belief revision in data-rich environments.

Abstract

Traditionally, an agent's beliefs would come from what the agent can see, hear, or sense. In the modern world, beliefs are often based on the data available to the agents. In this work, we investigate a dynamic logic of such beliefs that incorporates public announcements of data. The main technical contribution is a sound and complete axiomatisation of the interplay between data-informed beliefs and data announcement modalities. We also describe a non-trivial polynomial model checking algorithm for this logical system.

Dynamic Logic of Trust-Based Beliefs

TL;DR

This work develops a dynamic logic for trust-based beliefs where data-informed knowledge and trust-modulated beliefs interact with public data announcements . It introduces a sound and complete axiomatisation, including a non-trivial Commutativity axiom , and a ternary semantics to capture how publicly announced data affects belief under trust. A canonical tree-based model proves completeness, and a polynomial-time model-checking algorithm is provided, enabling scalable reasoning about data-driven beliefs in multi-agent settings. The framework is illustrated with data- and trust-centric scenarios such as public AP tweets influencing automated trading, offering formal tools for data-driven belief revision in data-rich environments.

Abstract

Traditionally, an agent's beliefs would come from what the agent can see, hear, or sense. In the modern world, beliefs are often based on the data available to the agents. In this work, we investigate a dynamic logic of such beliefs that incorporates public announcements of data. The main technical contribution is a sound and complete axiomatisation of the interplay between data-informed beliefs and data announcement modalities. We also describe a non-trivial polynomial model checking algorithm for this logical system.

Paper Structure

This paper contains 10 sections, 10 theorems, 10 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Related Literature
  3. Contribution and Outline
  4. Trustworthiness Model
  5. Syntax and Semantics
  6. Belief Revision
  7. Axioms
  8. Completeness
  9. Canonical Model
  10. Properties of the Canonical Model

Key Result

theorem thmcountertheorem

For any dataset $U\subseteq V$, any world $w$ of a trustworthiness model, any set of formulae $F\subseteq \Phi$, and any formula $\varphi\in\Phi$, if $w,U\Vdash f$ for each formula $f\in F$ and $F\vdash \varphi$, then $w,U\Vdash \varphi$.

Figures (3)

  • Figure 1: Trustworthiness model. Data variable $t$ is trustworthy in worlds $w_1$ and $w_3$ and is not trustworthy in world $w_2$.
  • Figure 2: Trustworthiness model.
  • Figure 3: Fragment of tree $W$.

Theorems & Definitions (16)

  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • theorem thmcountertheorem: strong soundness
  • lemma thmcounterlemma
  • lemma thmcounterlemma
  • lemma thmcounterlemma
  • lemma thmcounterlemma
  • lemma thmcounterlemma
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • ...and 6 more