Bounded Synthesis of Reactive Programs
Abstract
Most algorithms for the synthesis of reactive systems focus on the construction of finite-state machines rather than actual programs. This often leads to badly structured, unreadable code. In this paper, we present a bounded synthesis approach that automatically constructs, from a given specification in linear-time temporal logic (LTL), a program in Madhusudan's simple imperative language for reactive programs. We develop and compare two principal approaches for the reduction of the synthesis problem to a Boolean constraint satisfaction problem. The first reduction is based on a generalization of bounded synthesis to two-way alternating automata, the second reduction is based on a direct encoding of the program syntax in the constraint system. We report on preliminary experience with a prototype implementation, which indicates that the direct encoding outperforms the automata approach.
Cite
@article{arxiv.1807.09047,
title = {Bounded Synthesis of Reactive Programs},
author = {Carsten Gerstacker and Felix Klein and Bernd Finkbeiner},
journal= {arXiv preprint arXiv:1807.09047},
year = {2018}
}