Dynamic Epistemic Logic of Resource Bounded Information Mining Agents

TL;DR

This paper develops SPQ, a dynamic epistemic logic for resource-bounded agents who can purchase information from a reliable source. It combines a multi-agent Kripke framework with per-agent costs $\mathsf{Cost}_i(w,A)$ and budgets $\mathsf{Bdg}_i(w)$, and introduces the semi-public group-query operator $[?_G^A]$ to model costed queries whose answers are private to the group. The authors provide a sound and complete axiomatisation, prove polynomial-time model checking, and establish decidability via a small-model theorem with a $\text{NEXPTIME}$ upper bound and $\text{EXPTIME}$-hardness for satisfiability. They also show how group cooperation and resource sharing enable knowledge acquisition that individual agents cannot achieve alone, outlining practical avenues for epistemic planning under resource constraints.

Abstract

Logics for resource-bounded agents have been getting more and more attention in recent years since they provide us with more realistic tools for modelling and reasoning about multi-agent systems. While many existing approaches are based on the idea of agents as imperfect reasoners, who must spend their resources to perform logical inference, this is not the only way to introduce resource constraints into logical settings. In this paper we study agents as perfect reasoners, who may purchase a new piece of information from a trustworthy source. For this purpose we propose dynamic epistemic logic for semi-public queries for resource-bounded agents. In this logic (groups of) agents can perform a query (ask a question) about whether some formula is true and receive a correct answer. These queries are called semi-public, because the very fact of the query is public, while the answer is private. We also assume that every query has a cost and every agent has a budget constraint. Finally, our framework allows us to reason about group queries, in which agents may share resources to obtain a new piece of information together. We demonstrate that our logic is complete, decidable and has an efficient model checking procedure.

Figures (1)

• Figure 1: (Left) Model ${\mathcal{M}}$ for \ref{['simpleexample']}. The model contains four states $w_1, w_2, w_3$ and $w_4$, and we assume that $w_1$ is the actual one. Arrows represent epistemic equivalence classes for agents $l, m$ and $n$. Reflexive and transitive arrows are omitted for readability. Formulas $b_n=15, b_l=5, c_n(p)=30, c_m(p)=20$ and $c_l(p)=30$ hold in all four states, and we omit them from the figure. (Right) Updated model ${\mathcal{M}}^{?_{\{n, m\}}p}$ for \ref{['simpleexample']}. Formulas $b_l=5, c_n(p)=30, c_m(p)=20$ and $c_l(p)=30$ hold in both $w_1$ and $w_2$ as before. But $b_n=15$ no longer holds, since $n$'s budget is decreased after update: $b_n-\frac{c_m(p)}{|\{n, m\}|}=5$.

Theorems & Definitions (16)

• definition 1: Language
• definition 2: Model
• definition 3: Updated Model
• definition 4: Semantics
• theorem 1
• theorem 2
• definition 5: Closure
• definition 6: Canonical pre-model
• lemma 1
• lemma 2: Truth Lemma