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

Type of tool

Reactive controller synthesizer

Expected input

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.


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


Related papers

autoCode4: Structural Controller Synthesis (TACAS '17)

Last publication date

31 March 2017

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.