Reference
Abstract
This paper presents a controller synthesis approach using disjunctive polyhedral abstract interpretation. Our approach synthesizes infinite time-horizon controllers for safety properties with discrete-time, linear plant model and a switching feedback controller that is suitable for time-triggered implementations. The core idea behind our approach is to perform an abstract interpretation over disjunctions of convex polyhedra to identify states that are potentially uncontrollable. Complementing this set yields the set of controllable states, starting from which, the safety property can be guaranteed by an appropriate control function. Since, a straightforward disjunctive domain is computationally inefficient, we present an abstract domain based on a state partitioning scheme that allows us to efficiently control the complexity of the intermediate representations. Next, we focus on the automatic generation of controller implementation from our final fixed point. We show that a balanced tree approach can yield efficient controller code with guarantees on the worst-case execution time of the controller. Finally, we evaluate our approach on a suite of benchmarks, comparing different instantiations with related synthesis tools. Our evaluation shows that our approach can successfully synthesize controller implementations for small to medium sized benchmarks.
BibTeX
@string{EMSOFT = "ACM SIGBED International Conference on Embedded Software (EMSOFT)"}
@inproceedings{controller-emsoft14,
author = {Hadi RavanbakhshSriram Sankaranarayanan},
title = {Infinite Horizon Safety Controller Synthesis through Disjunctive Polyhedral Abstract Interpretation},
booktitle = EMSOFT,
year = {2014},
}