Lazy Abstraction-Based Controller Synthesis
For control synthesis of nonlinear systems, lazy ABCS reduces computational overhead by computing only necessary abstract transitions, offering a practical efficiency gain.
Lazy ABCS constructs abstractions on demand, achieving over 4x speedup on standard benchmarks compared to prior multi-layered ABCS for continuous-time nonlinear systems with reach-avoid and safety specifications.
We present lazy abstraction-based controller synthesis (ABCS) for continuous-time nonlinear dynamical systems against reach-avoid and safety specifications. State-of-the-art multi-layered ABCS pre-computes multiple finite-state abstractions of varying granularity and applies reactive synthesis to the coarsest abstraction whenever feasible, but adaptively considers finer abstractions when necessary. Lazy ABCS improves this technique by constructing abstractions on demand. Our insight is that the abstract transition relation only needs to be locally computed for a small set of frontier states at the precision currently required by the synthesis algorithm. We show that lazy ABCS can significantly outperform previous multi-layered ABCS algorithms: on standard benchmarks, lazy ABCS is more than 4 times faster.