Welcome !

Acacia+ is a tool for LTL realizability and synthesis, based on symbolic antichain techniques.
Acacia+ is extended to synthesis from LTL specifications with secondary mean-payoff objectives.
NEW! Acacia+ contains a new feature: the synthesis of the optimal strategy in a stochastic environment among a set of winning strategies in the worst-case.

Try it online!

or download it (release 2.3).

Other branches of the project

Acacia+ has recently been packaged into the framework acacia4aiger (hosted in github). This framework includes a tool which translated TLSF specifications into LTL ones which Acacia+ can handle. Additionally, it includes a translator from explicit Mealy machine output (the default for Acacia+) to AIGER. The acacia4aiger framework participates in the 2016 edition of the Reactive Synthesis Competition SYNTCOMP.

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. It uses the public library AaPAL for the manipulation of antichains and pseudo-antichains.

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 consist of conjunctions of smaller specifications. For monolithic unrealizable specifications, Acacia+ can synthesize a counter strategy for the environment.

Acacia+ v.2 proposes an extension to synthesis from LTL specifications with secondary mean-payoff objectives. Given an LTL formula, a partition of the signals into output and input signals, a weight function that associates a value to signals, and a threshold value, it checks for, and in positive case outputs, a strategy for the system to (1) satisfy the LTL formula and (2) ensure a value greater than or equal to the given threshold, against any strategy of the environment, where the value of an infinite word is the mean-payoff of the weights of its letters.

To summarize, Acacia+ has 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 (for LTL and mean-payoff objectives),
  • Synthesis of a winning strategy for the environment if the specification is monolithic and unrealizable (only for LTL),
  • Synthesis of the optimal strategy in a stochastic environment (when synthesizing from LTL with mean-payoff objectives) among a set of winning strategies in the worst-case.