Tableau methods to decide strong bisimilarity on LOTOS processes involving pure interleaving and enabling

JACK, standing for Just Another Concurrency Kit, is a new environment integrating a set of verification tools, supported by a graphical interface offering facilities to use these tools separately or in combination. The environment proposes several functionalities for the design, analysis and verification of cuncurrent systems specified using process algebra. Tools exchange information through a text format called Fc2. Users are able to graphically layout their specifications, that will be automatically converted into the Fc2 format and then minimised with respect to various kinds of equivalences. A branching time and action based logic, ACTIVE, is used to describe the properties that a specification must satisfy, and a model checking of ACTI, formulae on the specification is performed in linear time. A translator from Natural Language to ACTI, furmulae is provided, in order to simplify the job of describing specification properties by ACTI, formulae. A description of the graphical interface is given together with its functionalities and the exchange format used by the tools.