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

*(English)*Zbl 0672.03015The 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.

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.

Reviewer: G.Tseytlin

##### MSC:

03B70 | Logic in computer science |

68N25 | Theory of operating systems |

03D15 | Complexity of computation (including implicit computational complexity) |

68Q25 | Analysis of algorithms and problem complexity |

##### Keywords:

propositional time logic; specification of distributed computing systems; parallel interacting processes; synchronization
PDF
BibTeX
XML
Cite

\textit{J. Y. Halpern} and \textit{M. Y. Vardi}, J. Comput. Syst. Sci. 38, No. 1, 195--237 (1989; Zbl 0672.03015)

Full Text:
DOI

##### References:

[1] | Abrahamson, K.R., Decidability and expressiveness of logics of processes, Ph.D. thesis, university of Washington technical report 80-08-01, (1980) |

[2] | Chandy, M.; Misra, J., How processes learn, Distrib. comput., 1, 1, 40-52, (1986) · Zbl 0602.68026 |

[3] | Chandra, A.K.; Kozen, D.C.; Stockmeyer, L.J., Alternation, J. assoc. comput. Mach., 28, 114-133, (1981) · Zbl 0473.68043 |

[4] | Dwork, C.; Moses, Y., Knowledge and common knowledge in a Byzantine environment I: crash failures, (), 149-169 |

[5] | Emerson, E.A., Alternative semantics for temporal logics, Theoret. comput. sci., 26, 121-130, (1983) · Zbl 0559.68050 |

[6] | Emerson, E.A.; Clarke, E.M., Using branching time temporal logic to synthesize synchronization skeletons, Sci. comput. programming, 2, 241-266, (1982) · Zbl 0514.68032 |

[7] | Emerson, E.A.; Halpern, J.Y., Decision procedures and expressiveness in the temporal logic of branching time, J. comput. system sci., 30, No. 1, 1-24, (1985) · Zbl 0559.68051 |

[8] | Emerson, E.A.; Halpern, J.Y., “sometimes“ and “not never” revisited: on branching vs. linear time, J. assoc. comput. math., 33, No. 1, 151-178, (1986) · Zbl 0629.68020 |

[9] | Facin, R.; Halpern, J.Y.; Vardi, M.Y., A model-theoretic analysis of knowledge, (), 268-278 |

[10] | Facin, R.; Halpern, J.Y.; Vardi, M.Y., What can machines know? on the epistemic properties of machines, (), 428-434, (A revised appears as IBM Research Report RJ 6250, 1988.) |

[11] | Fischer, M.J.; Immerman, N., Foundations of knowledge for distributed systems, (), 171-185 |

[12] | Fischer, M.J.; Immerman, N., Interpreting logics of knowledge in propositional dynamic logic with converse, Inform. process. lett., 25, No. 3, 175-182, (1987) · Zbl 0634.03012 |

[13] | Gabbay, D.; Pnueli, A.; Shelah, S.; Stavi, J., On the temporal analysis of fairness, (), 163-173 |

[14] | Halpern, J.Y., Using reasoning about knowledge to analyze distributed systems, () · Zbl 0943.68016 |

[15] | Halpern, J.Y.; Fagin, R., A formal model of knowledge, action, and communiction in distributed systems: preliminary report, (), 224-236 |

[16] | Halpern, J.Y.; Moses, Y.O., Knowledge and common knowledge in a distributed environment, (), 50-61, revised report |

[17] | Halpern, J.Y.; Moses, Y.O., A guide to the modal logics of knowledge and belief: preliminary report, (), 480-490 |

[18] | Halpern, J.Y.; Reif, J.H., The propositional dynamic logic of deterministic well-structured programs, Theoret. comput. sci., 27, 127-165, (1983) · Zbl 0552.68035 |

[19] | Halpern, J.Y.; Vardi, M.Y., The complexity of reasoning about knowledge and time: extended abstract, (), 304-315 |

[20] | Harel, D., Recurring dominoes: making the highly undecidable highly understandable, (), 177-194 · Zbl 0531.68002 |

[21] | Harel, D.; Pnueli, A.; Stavi, J., Propositional dynamic logic of nonregular programs, J. comput. system sci., 26, No. 2, 222-243, (1983) · Zbl 0536.68041 |

[22] | \scD. Harel, A. Pnueli, and M. Y. Vardi, Two-dimensional temporal logic and PDL with intersection, unpublished. |

[23] | Ladner, R.; Reif, J.H., The logic of distributed protocols, (), 207-221 |

[24] | Lamport, L., What good is temporal logic?, (), 657-668 |

[25] | Lamport, L., “sometime“ is sometimes “not never”: on the temporal logic of programs, (), 174-185 |

[26] | Lehmann, D.J., Knowledge, common knowledge, and related puzzles, (), 62-67 |

[27] | Lehmann, D.J., (), Talk given at the |

[28] | Manna, Z.; Wolper, P.L., Synthesis of communicating processes from temporal logic specifications, ACM trans. programming lang. systems, 6, No. 1, 68-93, (1984) · Zbl 0522.68030 |

[29] | Moore, R.C., Reasoning about knowledge and action, () |

[30] | Moses, Y.O.; Dolev, D.; Halpern, J.Y., Cheating husbands and other stories: A case study of knowledge, action, and communication, Distrib. comput., 1, No. 3, 167-176, (1986) · Zbl 0609.68072 |

[31] | Moses, Y.; Tuttle, M., Programming simultaneous actions using common knowledge, (), 208-221 |

[32] | Parikh, R.; Ramanujam, R., Distributed processing and the logic of knowledge, (), 256-268 · Zbl 0565.68025 |

[33] | Pease, M.; Shostak, R.; Lamport, L., Reaching agreement in the presence of faults, J. assoc. comput. Mach., 27, No. 2, 228-234, (1980) · Zbl 0434.68031 |

[34] | Pnueli, A., Linear and branching structures in the semantics and logics of reactive systems, (), 15-32, New York/Berlin |

[35] | Reif, J.; Sistla, A.P., A multiprocess network logic with temporal and spatial modalities, J. comput. system sci., 30, No. 1, 41-53, (1985) · Zbl 0565.68031 |

[36] | Rogers, H., Theory of recursive functions and effective computability, (1967), McGraw-Hill New York · Zbl 0183.01401 |

[37] | Rosenschein, S., Formal theories of knowledge in at and robotics, New generation comput., 3, 345-357, (1985) · Zbl 0596.68061 |

[38] | Rosenschein, S.; Kaelbling, L., The synthesis of digital machines with provable epistemic properties, (), 83-97 |

[39] | Sato, M., A study of Kripke-style methods of some modal logics by Gentzen’s sequential method, Publ. res. inst. math. sci., 13, No. 2, (1977) · Zbl 0405.03013 |

[40] | Sistla, A.P.; Clarke, E.M., The complexity of propositional linear temporal logics, J. assoc. comput. Mach., 32, 3, 733-749, (1985) · Zbl 0632.68034 |

[41] | Sistla, A.P.; German, S.M., Reasoning with many processes, (), 138-153 |

[42] | Sistla, A.P.; Zuck, L.D., On the eventually operator in temporal logic, (), 153-166 |

[43] | Stockmeyer, L.J., The complexity of decision problems in automata theory and logic, () · Zbl 0444.94037 |

[44] | Vardi, M.Y.; Stockmeyer, L.J., Improved upper and lower bounds for modal logics of programs, (), 240-251 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.