Title
Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts
Abstract
Automated synthesis of reactive systems from specifications has been a topic of research for decades. Recently, a variety of approaches have been proposed to extend synthesis of reactive systems from propositional specifications towards specifications over rich theories. We propose a novel, completely automated approach to program synthesis which reduces the problem to deciding the validity of a set of AE-formulas. In spirit of IC3 / PDR, our problem space is recursively refined by blocking out regions of unsafe states, aiming to discover a fixpoint that describes safe reactions. If such a fixpoint is found, we construct a witness that is directly translated into an implementation. We implemented the algorithm on top of the JKind model checker, and exercised it against contracts written using the Lustre specification language. Experimental results show how the new algorithm outperforms JKind’s already existing synthesis procedure based on l-induction and addresses soundness issues in the l-inductive approach with respect to unrealizable results.
Previously Published Citation
24th International Conference onTools and Algorithms for the Construction and Analysis of Systems (TACAS 2018)
Description
Associated research group: Critical Systems Research Group
Suggested Citation
Katis, Andreas; Fedyukovich, Grigory; Guo, Huajun; Gacek, Andrew; Backes, John; Gurfinkel, Arie; Whalen, Michael.
(2018).
Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts.
Retrieved from the University of Minnesota Digital Conservancy,
https://hdl.handle.net/11299/217452.