Interactions between Knowledge and Time in a First-Order Logic for Multi-Agent Systems: Completeness Results
This work addresses formal verification challenges for multi-agent systems, providing foundational completeness results, but it is incremental as it builds on existing logical frameworks.
The paper tackles the problem of reasoning about multi-agent systems by investigating first-order temporal-epistemic logics, encoding properties like perfect recall and synchronicity, and shows completeness results for several monodic fragments with respect to quantified interpreted systems.
We investigate a class of first-order temporal-epistemic logics for reasoning about multi-agent systems. We encode typical properties of systems including perfect recall, synchronicity, no learning, and having a unique initial state in terms of variants of quantified interpreted systems, a first-order extension of interpreted systems. We identify several monodic fragments of first-order temporal-epistemic logic and show their completeness with respect to their corresponding classes of quantified interpreted systems.