Adaptive synthesis improves controllers when environment assumptions fail
Learning to adapt GR(1) specifications through degradation
Software EngineeringArtificial IntelligenceLogic in Computer Science
Summary
Controllers made with formal rules can fail if the outside world acts in ways not planned for. The authors propose a method that watches for these unexpected behaviors and then adjusts the rules so the controller still works, losing as few guarantees as possible. Their method finds different possible fixes and helps pick the best one to keep the system robust. In tests, they often keep all original guarantees intact while adapting to new situations.
What this means in practice
- •For embedded system developers: Automatically adjust control software when device environments differ from initial assumptions to maintain safe operation.
- •For autonomous vehicle engineers: Ensure vehicle controllers adapt specifications on-the-fly as real-world conditions deviate from models without losing key safety properties.
Authors
Tiberiu-Andrei Georgescu, Dalal Alrajeh, Sebastian Uchitel
Abstract
Reactive synthesis is a powerful tool for generating correct-by-construction controllers from formal specifications. GR(1) is an assume-guarantee specification framework that enables efficient synthesis, allowing synthesised controllers to be used in a wide array of applications. The limitation of such controllers is that, should they encounter environment behaviour unspecified in the assumptions of the specification, the specified system guarantees are no longer ensured. Our work proposes an approach based on oracle-guided inductive synthesis to adapt the specification to be consistent with the observed assumption violation, while degrading system guarantees as little as possible to maintain realisability. Our methodology discovers multiple potential solutions, so we propose a preference criteria, based on the ability of the specification to enable robustness under adaptation. Although our approach is capable of degrading the entire specification, for our case studies we successfully discover degradations that preserve the entire set of original guarantees.