PV2 ⊧ BAS: Bounded Asynchronous Synthesissynthesises asynchronous programs based on an LTL formula

Application domain/field

• Program synthesis
• Reactive asynchronous systems
• Asynchronous synthesis

Type of tool

Synthesis tool

Expected input

LTL formula $\phi$

Format:

? (probably LTL3BA format)

Expected output

• UNREALIZABLE if the LTL specification is synchronously unrealizable
• REALIZABLE and implementation if $PR(\phi )$ (Pnueli-Rosner closure of $\phi$) is synchronously realizable.
• UNREALIZABLE if $PR(\neg \phi )$ (Pnueli-Rosner closure of $\neg \phi$) is not synchronously realizable.

Internals

• Uses LTL3BA, BoSy, Acacia+
• Uses BDDs (Binary Decision Diagrams).
• Given an LTL specification, they use that asynchronous synthesis can be reduced to checking whether a specification is synchronously synthesizable.

Comments

Tool to synthesize (i.e. automatic construction from specification) asynchronous programs from temporal specifications