Acacia+ is a tool for LTL realizability and synthesis, based on symbolic antichain techniques.

Try it online!

or download it (release 1.4).

About the tool

Acacia+ is an open source implementation in Python/C of some of the theoretical results obtained by our research team. It is the successor of Acacia, written in Perl, but Acacia+ is more scalable, flexible and modular. Given an LTL formula and a partition of the signals into output signals controlled by the system and input signals controlled by the environment, Acacia+ checks for realizability of the formula. If the formula is realizable, it synthesizes a Moore machine such that no matter the environment sends, the executions of the machine all satisfy the LTL formula. Acacia+ also supports compositional synthesis from LTL specifications that consists of conjunctions of smaller specifications. For monolithic unrealizable specifications, Acacia+ can synthesize a counter strategy for the environment. To summarize, Acacia+ have the following features:

• Realizability check of the controller specification,
• Compositional realizability from conjunctions of sub-specifications,
• Synthesis of a winning strategy for the controller if the specification is realizable,
• Synthesis of a winning strategy for the environment if the specification is monolithic and unrealizable.