Alexander Weber, Elisei Macoveiciuc and
Gunther Reissig.
ABS: A formally correct software tool for space-efficient symbolic synthesis.
Proc. 25th ACM Intl. Conf. Hybrid Systems: Computation and Control
(HSCC), Milan, Italy, May 4-6, 2022
The source code of ABS is publicly available
under GNU General Public License.
Please refer to the User's Manual
for information on how to get, to compile and to use the software.
Full text.
(Definitive publication; restricted access.)
Abstract:
We present ABS, a software for Abstraction-Based Synthesis of
controllers for continuous-state control systems.
The tool distinguishes itself from previously known such software by
being formally correct, i.e., any controller synthesized by ABS is
mathematically guaranteed to solve the control problem provided as
input.
ABS achieves this quality by providing an input language with
mathematically defined semantics and a respective compiler, and by
carefully taking into account all numerical and rounding errors that
might be incurred at either compile- or run-time.
To mitigate computational overhead caused by the aforementioned
approach, ABS implements, e.g. on-the-fly synthesis algorithms with
greatly reduced memory requirement.
The tool is currently applicable to invariance and reachability
problems and requires state measurement.
We discuss structure, algorithmic details and basic usage
of ABS, and we demonstrate on two examples that its performance
compares favorably with that of competing, not formally correct
synthesis software.
BibTeX entry:
@InProceedings{WeberMacoveiciucReissig22,
author = {Alexander Weber and Elisei Macoveiciuc and Gunther Reissig},
title = {{ABS}: A formally correct software tool for space-efficient symbolic synthesis},
pages = {19:1--19:10},
booktitle = {Proc. 25th {ACM} Intl. Conf. on Hybrid Systems: Computation and Control (HSCC), Milan, Italy, } # may # { 4-6, 2022},
editor = {Ezio Bartocci and Sylvie Putot},
year = 2022,
doi = {10.1145/3501710.3519519}
}
Impressum und Haftungsausschluß