• People
• Events
• Research

Tactics for State Space Reduction on the Concurrency Workbench

Abstract: The Concurrency Workbench is a software tool catering for the automatic analysis of finite state processes expressed in Robin Milner's Calculus of Communicating Systems (CCS). This system is highly flexible in that analyses of concurrent systems can be carried out using a variety of different process semantics. However, the Workbench is limited in its application to realistic problems by spatial constraints. These are imposed by the fact that the analyses carried out deal with a transition graph representation of processes which, for finite state systems, can be exponential in the number of agents in the CCS expression. To address this problem we apply some heuristic transformations in order to arrive at a semantically equivalent expression that leads to a smaller transition graph. This article discusses the techniques employed, the new features available in the Workbench, and suggests how they might be applied in reducing larger problems prior to analysis.

LFCS report ECS-LFCS-90-109, February 1990.