Acacia is no longer maintained. Try its successor: Acacia+

Acacia is an analysis tool for LTL realizability check and synthesis. Its main purpose is to demonstrate the usefulness of antichain-based techniques applied to the realizability problem of formal specifications. You can download it here.

About the tool

The Acacia tool is an implementation of some of the theoretical results obtained by our research team. See the Antichain for Verification page for more details about antichain-based verification algorithms.

Given a controller specification, which includes a set of LTL formulas and a partition of input/output variables, Acacia is able to perform the following :

• Checking the realizability of the controller specification,
• Synthesizing a Moore machine which encodes a winning strategy of the controller if the specification is realizable,
• Synthesizing a Mealy machine which encodes a winning strategy of the environment if the specification is unrealizable,
• Verifying the correctness of the machines in aid of VIS.

Acacia is free software and is distributed under the terms of the GPLv2.

On this site, you can :

• Download the tool for local use
• Get information on how to use Acacia
• Read about experimentations we made to compare the performance of Acacia to other tools
• Find the research papers where the theoretical background of Acacia can be found