Formal Models for Parallel and Distributed Systems
326.619, Mon 8:30-10:00, T711
WS 1999/2000 (Start: October 11)
Modeling of and Reasoning about Reactive Systems
A reactive system maintains an ongoing interaction with its environment,
as opposed to computing some final value on termination. Examples of reactive
systems are concurrent programs, embedded and process control programs, and
Reactive systems have a complex nature; a merely intuitive understanding is
not sufficient to draw conclusions about their behavior. For the
specification and design of such system, a professional engineer
therefore needs formal frameworks that allow to model the system and to
reason about its behavior.
This course focuses on two such frameworks:
- Temporal Logic
Temporal logic describes and reasons about sequences of states evolving in
time. A reactive system is translated into a logic formula; an implementation
meets a specification, if the implementation implies the specification.
- Process Calculus
Process calculus describes and reasons about the interaction of a system with
its environment. The system is translated into an expression that can be
transformed according to a set of algebraic laws without changing its
The course will provide the necessary formal basis but then concentrate on the
application of these frameworks for designing correct reactive systems.
- Leslie Lamport
- The Temporal Logic of
ACM Transactions on Programming Languages and Systems, 16(3):872-923, May
- Zohar Manna and Amir Pnueli
- Temporal Verification of Reactive
Systems -- Safety, Springer, New York, 1995.
- Robin Milner
- Communication and Concurrency, Prencice Hall,
Englewood Cliffs, NJ, 1989.
- The Temporal Logic of Actions I (PostScript)
Logic of actions, the raw logic, TLA, fairness, syntax and semantics of TLA,
- The Temporal Logic of Actions II (PostScript)
Proving simple program properties, invariance proofs, eventuality proofs,
proof of fairness, formal specification, quantification, refinement mappings.
- A Process Calculus I
Agents and behaviors, exxamples, composition of agents, equality of agents,
restrictions, transition graphs, the basic language, derivation trees, the
- A Process Calculus II
Equational laws, equivalence of agents, strong bisimulation and strong
equivalence, weak bisimulation and observation equivalence, observation
Maintained by: Wolfgang Schreiner
Last Modification: October 9, 1999