The complexity of reasoning about knowledge and time. I. Lower bounds

摘要

We study the propositional model logic of knowledge and time for distributed systems. We consider a number of logics (ninety-six in all!), which vary according to the choice of language and the assumptions made on the underlying system. The major parameters in the language are whether there is a common knowledge operator, whether we reason about the knowledge of one or more than one processor, and whether our temporal operators are branching or linear. The assumptions on distributed systems that we consider are: whether or not processors forget, whether or not processors learn, whether or not time is synchronous, and whether or not there is a unique initial state in the system. We completely characterize the complexity of the validity problem for all the logics we consider. This paper focuses on lower bounds; a sequel will deal with the corresponding upper bounds. Typical results include a ∏-completeness result for the language with common knowledge with respect to systems where processors do not forget, and a corresponding non-elementary-time result for the language without common knowledge. It is shown that, in general, the assumption that processors do not forget or do not learn greatly increases the complexity of reasoning about knowledge and time.