PV2 RealSynsynthesises a set of controllers that meet the reach-avoid specification

Synthesis tool for controllers with reach-avoid specifications.

Application domain/field

Type of tool

Synthesis tool

Expected input

Expected output

Set of controllers that meet the specification (reach G while avoiding O)


Controller synthesis is asks whether we can generate an input for a given system (or plant) so that it achieves a specification. This is interesting for applications such as vehicle path planning, motion control, and circuit design. RealSyn synthesizes provably correct controllers for linear systems with reach-avoid specifications. Reach-avoid specifications: Specifications that require the system to reach a goal G while avoiding unsafe states or obstacles O. Uses Z3, CVC4, Yices


Repository: https://github.com/umangm/realsyn

Related papers

Controller Synthesis Made Real: Reach-Avoid Specifications and Linear Dynamics (CAV 2018)

Last publication date

18 July 2018

Related tools

Other controller synthesis algorithms: CoSyMa, Pessoa, LTLMop, Tulip, SCOTS

ProVerB specific

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