Interactions Between Knowledge and Time in a First-Order Logic for Multi-Agent Systems: Completeness Results
While reactive systems (Pnueli, 1977) are traditionally specified using plain temporal logic, there is a well-established tradition in Artificial Intelligence (AI) and, in particular, Multi-Agent Systems (MAS) research to adopt more expressive languages. The authors investigate a class of first-order temporal-epistemic logics for reasoning about multi-agent systems. They 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. They identify several monodic fragments of first-order temporal-epistemic logic and show their completeness with respect to their corresponding classes of quantified interpreted systems.