Several types of properties can be checked, e.g. deadlock-freeness,
reachability, safety and liveness properties. Except for deadlock-freeness
these properties will be expressed as formulae. Therefore, this page is
structured in two parts:
First we shortly explain our notion of reachability property. It is a
statement about states of the system. For example, the mutual exclusion
property of critical regions can be understood as reachability property
it amounts to the question if there exists a reachable global
state of the system in which two processes have entered their critical
regions at the same time.
These properties can be expressed with so-called
state formulae. A state
formula is a propositional logic formula
consisting of atomic propositions and logical operators.
Details about the syntax are shown
Safety and liveness properties will be expressed in terms of temporal logics
like CTL and LTL. They are the most popular logics, and together they can
express all common safety and liveness properties. A detailed syntax of CTL and
LTL is shown here.
We shall give a short introduction to LTL and CTL according to
||E. A. Emerson.
Temporal and Modal Logic.
Handbook of Theoretical Computer Science, vol. B, pages 997 -
1067, Elsevier Science Publishers B. V., 1990.
Next chapter: Checking properties