Counter Example Guided Synthesis of Polyhedral Control Lyapunov functions for Reach-Avoid properties
- Hyperplane. Find a line that separates an obstacle from the initial and terminal set.
- Split into convex sets and synthesize CLF for each region.
CounterExample-Guided Inductive Synthesis of Polyhedral Control Lyapunov Functions
Julia