BeBoSy: Behavior Examples Meet Bounded Synthesis

Abstract

Bounded synthesis generates a state machine satisfying given temporal specification in linear temporal logic (LTL) while bounding the number of states of the target solution. Bounded synthesis methods currently do not support finite-length behavior examples, which are often helpful when formulating the specification of the desired state machine. In this work we show how to incorporate behavior examples into bounded synthesis methods and exemplify the approach by presenting BeBoSy (Behavior Examples meet BoSy), an extension of the bounded synthesis tool BoSy based on reductions to Boolean satisfiability (SAT) and Quantified Boolean formula satisfiability (QSAT) problems. The proposed approach is to augment the encodings used in BoSy with additional constraints that ensure the compliance of the generated state machine with the given behavior examples. Experiments with openly available data from the annual reactive synthesis competition SYNTCOMP augmented with random behavior examples show that the efficiency of the proposed approach is superior to both BoSy (with naïve representation of behavior examples with LTL formulas) and a state-of-the-art counterexample-guided approach EFSM-tools.

Keywords

• Bounded synthesis
• LTL synthesis
• inference algorithms
• Boolean satisfiability
• quantified Boolean formula