Reasoning about knowledge and time in asynchronous systems

We investigate the complexity of reasoning about knowledge and time, with emphasis on the case of asynchronous time. We show that in the case of no forgetting (Ladner and Reif's Tree Logic of Protocols, TLP) the validity problem is complete for nonelementary time. This settles the open problem of [HV86, LR86]. This result is somewhat surprising in light of Ladner and Reif 's undecidability result for a similar logic, LLP. We show that the undecidability result for LLP is caused by two quite natural properties of models in that logic, which we call no learning and unique initial state. Both of these properties are necessary for the undecidability result in [LR86]. We completely characterize the complexity of all ninety-six logics that result by varying the relevant parameters. Many of the results are quite delicate, and require substantially new techniques. © 1988 ACM.