Modal abstractions of concurrent behaviour

Abstract

We present a novel algorithm for the automatic construction of modal transition systems as abstractions of concurrent processes. Modal transition systems are recognised as valuable abstractions for model checking because they allow for the deduction of safety as well as liveness properties. However, the issue of effectively creating these abstractions from specification languages such as process algebras is a missing link that prevents their more widespread usage for model checking of concurrent systems. Our algorithm is based on static analysis and uses a lattice of intervals to express simultaneous over- and under-approximations to the set of process actions available in a particular state. We obtain an abstraction that is 3-valued in both states and transitions and that naturally integrates with model checking approaches for modal transition systems. © 2008 Springer-Verlag.