Reasoning About Knowledge on Regular Expressions is 2EXPTIME-complete
This result provides a precise complexity bound for reasoning about knowledge in multi-agent systems, which is incremental as it extends prior work on epistemic logics.
The paper tackles the computational complexity of satisfiability in Public Observation Logic (POL), a logic for reasoning about knowledge updates from public observations, and proves that the problem is 2EXPTIME-complete.
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.