The complexity of reasoning about knowledge and time

Abstract

We study the propositional modal logic of knowledge and time for distributed systems. Models are categorized in terms of three parameters: whether processors have bounded memory or unbounded memory, whether time is synchronous or asynchronous, and whether time is linear or branching. We show that if we have common knowledge in the language, then in the unbounded memory case the validity problem is undecidable. Without common knowledge, the validity problem is hard for nonelementary time, and in the synchronous case is actually decidable in nonelementary time. If processors have bounded memory, then there is no real interaction between knowledge and time, and the validity problem is no worse than the validity problem for knowledge and time separately.