PV2 ⊧ autoCode4synthesises a reactive controller based on requirements written in the GXW subset of LTL

autoCode4 synthesizes structured reactive controllers from realizable specifications in the GXW subset of linear temporal logic (LTL)

Application domain/field

• Reactive controllers
• Program synthesis
• Controller synthesis

Type of tool

Reactive controller synthesizer

Expected input

• Specification in the GXW subset of LTL.

Expected output

Reactive controller as a Ptolemy II model. From this model one can automatically generate executable C or HDL code. autoCode4 can also generate reactive controllers in Lustre.

Internals

autoCode4 maintains traceability between individual requirements and the generated controller blocks.