PV2 ⊧ PARTYgenerates an automaton from source code or spec

Bounded synthesis tool that supports CTL* synthesis

Application domain/field

• SMT-based synthesis
• Bounded synthesis
• Synthesis
• Reactive synthesis
• CTL* synthesis

Type of tool

Synthesis tool

Expected input

Specification file

Format:

• elli.py: Acacia+ or TLSF format
• star.py: Python

Expected output

• elli.py: If realisable, PARTY outputs a Mealy or Moore machine in dot or NuSMV format.
• star.py: returns unknown or realizable

If realisable, then an automaton in dot or AIGER format.

Internals

• This tool uses bounded synthesis. In bounded synthesis an LTL property is translated to Büchi automata, and the verification of LTL properties can be reduced to deciding emptiness of the product of this automaton and a Kripke structure representing an implementation.
• This tool is actually a collection of several tools for bounded synthesis, the most notable being:
• The elli.py implements Bounded Synthesis, as explained in the CAV '13 paper.
• The star.py extends bounded synthesis to branching logics (CTL*), as explained in the CAV '17 paper.