Organisation: 
University of Waterloo (CANADA)


Functionality: 
Generation and minimization of labelled transition systems

Tools used: 
CADP (Construction and Analysis of Distributed Processes)

Period: 
2000

Description: 
For large applications, modelchecking 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
modelcheckers 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 semicompositional 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
minimized.
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 casestudy, the algorithm compared favourably with other modelcheckers (SPIN, ARAPROD, and the EXHIBITOR and ALDEBARAN tools of CADP), by allowing to handle a PBX specification with 5 components. 
Conclusions: 
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,
onthefly search, or partialorder 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.

Publications: 
[Liu00]
Wayne Liu.
"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. 148162, Springer Verlag, September 2000.
Available online at: http://netlib.belllabs.com/netlib/spin/ws00/18850150.pdf or also from our FTP site in PDF or PostScript 
Contact:  Wayne Liu Electrical and Computer Engineering Department University of Waterloo Waterloo, Ontario, Canada, N2L 3G1 Tel: (519) 8884567x5167 Fax: (519) 7463077 Email: wbliu@uwaterloo.ca 
Further remarks:  This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software 