Characterizing perfect recall using next-step temporal operators in S5 and sub-S5 Epistemic Temporal Logic

TL;DR

This paper introduces a new local frame condition for perfect recall in Epistemic Temporal Logic (ETL) with S5 and sub-S5 frames, providing a complete axiomatization and exploring extensions to sub-S5 settings.

Contribution

It presents a novel local frame condition for perfect recall in S5 ETL, along with a complete axiomatization and analysis of sub-S5 extensions.

Findings

New local frame condition for perfect recall in S5 ETL

Complete axiomatization for S5 ETL with perfect recall

Extension of perfect recall notions to sub-S5 settings

Abstract

We review the notion of perfect recall in the literature on interpreted systems, game theory, and epistemic logic. In the context of Epistemic Temporal Logic (ETL), we give a (to our knowledge) novel frame condition for perfect recall, which is local and can straightforwardly be translated to a defining formula in a language that only has next-step temporal operators. This frame condition also gives rise to a complete axiomatization for S5 ETL frames with perfect recall. We then consider how to extend and consolidate the notion of perfect recall in sub-S5 settings, where the various notions discussed are no longer equivalent.