The complexity of reasoning about knowledge and time. I: Lower bounds (Q1119565)

The paper investigates problems of the computational complexity for propositional time logic oriented towards the specification of distributed computing systems. The basic result of the investigation is a classification of parallel interacting processes based on the corresponding formalized models and properties of specification languages and distributed systems. Formalization is based on the notions of path (route of states), synchronization (system clock readout), protocol, and system interpretation. System types differ in their ability to acquire and lose knowledge of the passed path and in the synchronization. Depending on type and interpretation of systems a table of complexity estimates is given. Lower bound theorems are proved for some of the obtained estimates. The obtained results are of interest for the solution of practical problems in connection with the necessity of estimating the required memory volumes, for synthesizing the activity protocol of distributed systems from their specifications.