Loading…

Lazy Abstraction-Based Controller Synthesis

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 th...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2019-08
Main Authors: Hsu, Kyle, Majumdar, Rupak, Mallik, Kaushik, Schmuck, Anne-Kathrin
Format: Article
Language:English
Subjects:
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2331-8422