Reasoning About Knowledge on Regular Expressions is 2EXPTIME-complete

TL;DR

This paper proves that the satisfiability problem for Public Observation Logic, used in multi-agent epistemic planning, is computationally very complex, specifically 2EXPTIME-complete.

Contribution

It establishes the exact computational complexity of reasoning about knowledge updates in POL, a logic for multi-agent systems.

Findings

Satisfiability problem for POL is 2EXPTIME-complete.

Provides formal complexity bounds for reasoning in epistemic planning.

Enhances understanding of computational limits in knowledge update logics.

Abstract

Logics for reasoning about knowledge and actions have seen many applications in various domains of multi-agent systems, including epistemic planning. Change of knowledge based on observations about the surroundings forms a key aspect in such planning scenarios. Public Observation Logic (POL) is a variant of public announcement logic for reasoning about knowledge that gets updated based on public observations. Each state in an epistemic (Kripke) model is equipped with a set of expected observations. These states evolve as the expectations get matched with the actual observations. In this work, we prove that the satisfiability problem of $\POL$ is 2EXPTIME-complete.