Database of Research Tools Developed Using CADP

Interaction Abstraction Algorithm

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, 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 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 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.

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, 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.

Publications: [Liu-00] 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. 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
Contact:
Wayne Liu
Electrical and Computer Engineering Department
University of Waterloo
Waterloo, Ontario, Canada, N2L 3G1
Tel: (519) 888-4567x5167
Fax: (519) 746-3077
E-mail: wbliu@uwaterloo.ca



Further remarks: This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software


Last modified: Fri Feb 19 09:13:01 2016.


Back to the CADP research tools page