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

Synthesis tool for controllers with reach-avoid specifications.

Application domain/field

• Controller synthesis
• Linear systems
• Reach-avoid specifications
• Vehicle path planning
• Circuit design

Type of tool

Synthesis tool

Expected input

• System A
• Time bound T
• Set of obstacles O
• Goal G that should be reached
• Q and R: Used for linear quadratic regulator (LQR), they are set to the identity matrices for most examples

Expected output

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

Internals

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