Using optimal simulations to reduce reachability graphs

We here discuss an approach which uses the optimal simulation — a kind of reachability relation — to enable reasoning about important dynamic properties of a concurrent system. The optimal simulation usually involves only a very small subset of the possible behaviours generated by the system, yet provides a sufficient information to reason about a number of interesting system's properties (such as deadlock-freeness and liveness). In this paper …