In a seminal paper, Lamport argued that the requirements that designers wish to impose on reactive systems fall into two categories. Safety properties state that ``something bad never happens''; a system meeting such a property must not engage in the proscribed activity. Liveness properties, on the other hand, state that ``something good eventually happens''; to satisfy such a property, a system must engage in some beneficial action. Although informal, this classification has proved enormously successful, and providing a formal account of safety and liveness has been a main motivation for much of the work done on specification and verification of concurrent systems. Some of this work has aimed at semantic characterizations of these properties []. Others have developed logics that allow the precise formulation of safety and liveness properties. The most widely studied are temporal logics, which were first introduced into the computer science community by Pnueli [] and support the formulation of properties of system behavior over time. The remainder of this section reviews some of the research into temporal logic.
The dichotomies presented earlier in modeling concurrency also reveal themselves in the development of temporal logics. In particular, two schools of temporal logic have emerged.
The other two dichotomies---intensional vs. extensional, and interleaving vs. true concurrency---remain relatively unexplored. Traditional temporal logics have generally adopted an extensional view of system behavior and an interleaving model of concurrency, although recent work has explored logics for true concurrency.
Finally, other logics have also been developed for reasoning about concurrent systems, including various dynamic logics and logics of knowledge. The former permit the inclusion of programs inside formulas, while the latter allow users to express the understanding that individual agents have of other agents' states at a given point in time.