# 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!

## 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.