Description of the Benchmarks
=============================

The C, D and E examples stem from a case study from an industrial
project partner of the UniForM-project (B. Krieg-Brückner, J. Peleska
et al., The UniForM Workbench, a Universal Development Environment for
Formal Methods, in Proc. Formal Methods, 1999) where the problem is to
design a distributed real-time controller for a segment of tracks
where trams share a piece of track. For the evaluation of our approach
we chose the property that never both directions are given permission
to enter the shared segment simultaneously. We flawed the models by
weakening a temporal constraint.

The M and N examples come from a study that models a real-time
protocol to ensure mutual exclusion of a state in a distributed system
via asynchronous communication. The protocol is described in full
detail in (H. Dierks, Comparing Model-Checking and Logical
Reasoning for Real-Time Systems,2004 Formal Aspects of Computing 16,
104--120).

The FA and FB benchmarks are two flawed versions of the Fischer
protocol for mutual exclusion.
 
The A examples model arbiter trees to establish mutual exclusion
between 2^k client processes. The benchmarks A2-A6 contain arbiter
trees of height 2-6, with an exponentially growing number of
processes.