Interactions between Time and Knowledge in a First-order Logic for Multi-Agent Systems

We investigate a class of first-order temporal epistemic logics for the specification of multi-agent systems. We consider well-known properties of multi-agent systems including perfect recall, synchronicity, no learning, unique initial state, and define natural correspondences of these into quantified interpreted systems, the semantics we use to reason about multiagent systems in a first-order setting. Our findings identify several monodic fragments of first-order temporal epistemic logic that we prove to be both sound and complete with respect to the corresponding classes of quantified interpreted systems. The results show that interaction axioms for propositional temporal epistemic logic can be lifted to the monodic fragment.