Formal Verification of Epistemic States with Uncertainty in Multi-Agent Systems

• Jefferson O. Andrade Instituto Federal do Espírito Santo https://orcid.org/0000-0002-5321-9239

Resumo

Multi-agent systems operating in real-world environments must reason about knowledge and information under uncertainty, with varying degrees of trust and incomplete evidence. While Dynamic Epistemic Logic (DEL) provides a robust framework for modeling knowledge change, its classical binary foundation limits its applicability to scenarios involving gradations of truth and knowledge. The Bilattice Logic of Epistemic Actions and Knowledge (BEAK) addresses this limitation by grounding DEL in bilattice structures, but restricts its semantics to the four-valued bilattice FOUR, limiting expressiveness for complex applications. This paper introduces GEAK (Generalized Bilattice-based Epistemic Logic of Actions and Knowledge), a generalization of BEAK that operates over arbitrary logical bilattices. GEAK preserves the elegant product update mechanism of DEL while extending it to handle multi-valued accessibility relations with custom truth-value structures tailored to specific domains. We present the formal syntax and semantics of GEAK, demonstrate its theoretical properties, and provide a model checker for bilattice-based dynamic epistemic logic. Our contributions are validated through a case study using Ginsberg’s seven-valued default logic for multi-agent route planning, where autonomous vehicles coordinate under uncertainty with default assumptions about road conditions. Preliminary results suggest that GEAK offers greater expressiveness than classical approaches while maintaining computational tractability, enabling more realistic modeling and verification of multi-agent systems with sophisticated reasoning patterns involving definite and default information.

Palavras-chave: Model Checking, Epistemic Logic, Bilattices, Multi-Valued Logic, Dynamic Epistemic Logic, Action Model