Submitted: July 2010
Abstract
Model checking is a common technique for the verification of concurrent systems, where the actual system model’s behavior is checked against its intended execution behavior specified in some modal logic. Many important liveness properties can only be checked under the assumption that the components of the system are scheduled in a fair manner. Linear Time Temporal Logic (LTL) is a specification logic that allows to express the linear time behavior of systems. Due to its relative ease of use compared to more powerful logics that allow to express the branching behavior of systems, LTL is widely used in practice and in teaching. Unfortunately, in a setting where systems are modelled by action labelled transition systems (LTS), this logic is incapable to express most fairness constraints. As LTSs are commonly used models for concurrent systems, this renders LTL inadequate as a specification logic for concurrent systems’ behavior. In this thesis we introduce a modified version of LTL called C-LTL, which is capable of expressing arbitrary fairness constraints. We furthermore show that C-LTL is compatible with weak bisimulation minimization and that C-LTL equivalence coincides with a weak variant of ready trace equivalence. We finally show how the C-LTL model checking problem can be reduced to the model checking problem of standard LTL.