The idea to represent a (reactive) system as a temporal logic expression has been suggested by Amir Pnueli in the late 1970ies. Temporal logic has evolved over the years into a major specification- and verification tool.
Leslie Lamport suggested the Temporal Logic of Actions (TLA) as a special form of temporal logic. Starting with a TLA-representation of a system's decisive properties, the representation is systematically refined into a (usually large) TLA representation resembling an executable program. Verification of an implementation is thus reduced to logical implication. The principles of "implementation is implication" and "composition is conjunction" has been realized in TLA to a great extent with the help of the semantic model of "stuttering sequences".
The Temporal Logic of Distributed Actions (TLDA) has been constructed at the chair, employing distributed runs (i.e. causally ordered sets of actions) as a semantic model. This allows a fine grained treatment of subtle phenomena as they occur in the behavior of distributed systems. This includes a clear separation of concurrency and nondeterminism, and subtle problems of fairness assumptions. TLDA is particularly useful to model and to analyze systems that are composed of components with synchronized actions.