University of Waterloo (CANADA)
Generation and minimization of labelled transition systems
CADP (Construction and Analysis of Distributed Processes)
For large applications, model-checking techniques encounter the state
explosion problem, meaning that the size of the underlying state space
(or labelled transition system) may be exponential w.r.t. the size of
the application. A way to keep the state space manageable for
model-checkers is to include in the model only features that are
relevant to the property being checked. Such a model can be obtained
e.g., by hiding irrelevant actions and then minimizing the model
according to a suitable bisimulation relation, like observational
equivalence. Classical minimization algorithms require to construct
the whole state space and therefore are subject to state explosion.
Compositional and semi-compositional minimization algorithms attempt
to avoid this problem by minimizing components of the system
individually, but still may cause explosion in intermediate state
spaces because subsets of components need to be composed before being
A new algorithm, called interaction abstraction algorithm, is proposed for constructing and minimizing labelled transition systems. The algorithm has similar goals to (semi-)compositional minimization, but attempts to use the information about interactions with the rest of the system to remove redundant information from the model, while keeping the information necessary to preserve the property being checked. The algorithm has a theoretical complexity of O (n^4 m^5) for a system with n components having m states maximum, but it seems to perform quite efficiently in practice. The algorithm has been implemented using the CADP toolset. Its behaviour is illustrated on a private branch exchange (PBX) software. On this case-study, the algorithm compared favourably with other model-checkers (SPIN, ARAPROD, and the EXHIBITOR and ALDEBARAN tools of CADP), by allowing to handle a PBX specification with 5 components.
An original approach for minimizing labelled transition systems modulo
observational equivalence, called interaction abstraction, has been
proposed and implemented using CADP. The algorithm is most useful when
models of systems deal with many aspects, but only one aspect is of
interest at a time. Interaction abstraction can be used in conjunction
with other reduction techniques (e.g., compositional minimization,
on-the-fly search, or partial-order reduction) in order to take a
better advantage of the redundancy that may be present in systems.
Further research is needed in order to extend the algorithm with other
equivalence relations (e.g., safety equivalence) and to allow a better
behaviour in the case of systems with many components.
"Interaction Abstraction for Compositional Finite State Systems".
In K. Havelund, J. Penix, and W. Visser, editors, Proceedings of
the 7th SPIN Workshop (Stanford University, California), LNCS
vol. 1885, pp. 148-162, Springer Verlag, September 2000.
Available on-line at: http://netlib.bell-labs.com/netlib/spin/ws00/18850150.pdf
or also from our FTP site in PDF or PostScript
Electrical and Computer Engineering Department
University of Waterloo
Waterloo, Ontario, Canada, N2L 3G1
Tel: (519) 888-4567x5167
Fax: (519) 746-3077
|Further remarks:||This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software|