figure a

1 Introduction

The reactive synthesis problem is to check whether a given \(\omega \)-regular specification, usually presented as an LTL formula, has an implementation, and, if the answer is yes, to construct such an implementation. As a theoretical problem, reactive synthesis dates back all the way to Alonzo Church’s solvability question [6] in the 1950s; as a practical engineering challenge, the problem is fairly new. Tools for reactive synthesis started to come out around 2007 [5, 9, 11, 17]. The first SYNTCOMP tool competition took place at CAV 2014 and was originally restricted to safety specifications, and only later, starting with CAV 2016, extended with an LTL synthesis track [14].

In this paper, we present \(\textsf {BoSy}\), the winner of the 2016 LTL synthesis track. \(\textsf {BoSy}\) is based on the bounded synthesis approach [12]. Bounded synthesis ensures the minimality of the synthesized implementation by incrementally increasing a bound on the size of the solutions it considers. For each bound, the existence of a solution is encoded as a logical constraint solving problem that is solved by an appropriate solver. If the solver returns “unsat”, the bound is increased and a new constraint system is constructed; if the solver returns a satisfying assignment, an implementation is constructed.

From an engineering perspective, an interesting feature of the bounded synthesis approach is that it is highly modular. The construction of the constraint system involves a translation of the specification into an \(\omega \)-automaton. Because the same type of translation is used in model checking, a lot of research has gone into optimizing this construction; well-known tools include \(\textsf {ltl3ba}\) [1] and \(\textsf {spot}\) [8]. On the solver side, the synthesis problem can be encoded in a range of logics, including boolean formulas (SAT), quantified boolean formulas (QBF), dependency quantified boolean formulas (DQBF), the effective propositional fragment of first-order logic (EPR), and logical formulas with background theories (SMT) (cf. [10]). For each of these encodings, there are again multiple competing solvers.

\(\textsf {BoSy}\) leverages the best tools for the LTL-to-automaton translation and the best tools for solving the resulting constraint systems. In addition to its main purpose, which is the highly effective synthesis of reactive implementations from LTL specifications, \(\textsf {BoSy}\) is therefore also an experimentation framework, which can be used to compare individual tools for each problem, and even to compare tools across different logical encodings. For example, the QBF encoding is more compact than the SAT encoding, because it treats the inputs of the synthesized system symbolically. \(\textsf {BoSy}\) can be used to validate, experimentally, whether QBF solvers translate this compactness into better performance (spoiler alert: in our experiments, they do). Likewise, the DQBF/EPR encoding is more compact than the QBF encoding, because this encoding treats the states of the synthesized system symbolically. In our experiments, the QBF solvers nevertheless outperform the currently available DQBF solvers.

In the remainder of this paper, we present the tool architecture, including the interfaces to other tools, and report on experimental resultsFootnote 1.

Fig. 1.
figure 1

Tool architecture of \(\textsf {BoSy}\)

Full size image

2 Tool Architecture

An overview of the architecture of \(\textsf {BoSy}\) is given in Fig. 1. For a given bounded synthesis instance, \(\textsf {BoSy}\) accepts a JSON-based input format that contains a specification \(\varphi \) given in LTL, the signature of the implementation given as a partition of the set of atomic propositions into inputs and outputs, and the target semantics as a Mealy or a Moore implementation. In the preprocessing component, the tool starts to search for a system strategy with \(\varphi \) and an environment counter-strategy with \(\lnot \varphi \) in parallel.Footnote 2

After parsing, the LTL formula is translated into an equivalent universal co-Büchi automaton using an external automata translation tool. Currently, we support \(\textsf {ltl3ba}\) [1] and \(\textsf {spot}\) [8] for this conversion, but further translation tools can be integrated easily. Tools that output \(\textsf {SPIN}\) never-claims or the HOA format are supported.

To the resulting automaton, we apply some basic optimization steps like replacing rejecting terminal states with safety conditions and an analysis of strongly connected components to reduce the size of the constraint system [12].

The encoding component is responsible for creating the constraint system based on the selected encoding, the specification automaton, and the current bound on the number of states of the system. The component constructs a constraint system using a logic representation which supports propositional logic, different kinds of quantification, and comparison operators (between natural numbers). Our implementation contains the following encoding options. These encodings differ in their ability to support the symbolic encoding of the existence of functions. We refer the reader to [10] for details.

  • A propositional backend for SAT, where all functions are unrolled to conjunctions over their domain.

  • An input-symbolic encoding employing QBF solvers, where functions with one application context are symbolically represented.

  • Two encodings (state-symbolic, symbolic) using DQBF/EPR solvers, where functions, which are used in multiple contexts, are encoded symbolically.

  • An SMT encoding resembling the original bounded synthesis encoding [12].

This constraint system is then translated to a format that the selected solver understands, and the solver is called as an external tool. We support SAT solvers that accept the DIMACS input format and that can output satisfying assignments, currently \(\textsf {PicoSAT}\) [3] and \(\textsf {CryptoMiniSat}\) [24]. We have three categories of QBF solving tools: QDIMACS/QCIR solver that can output top-level assignments (\(\textsf {RAReQS}\) [16], \(\textsf {CAQE}\) [21], and \(\textsf {DepQBF}\) [18]), QDIMACS preprocessors (\(\textsf {Bloqqer}\) [4]), and certifying QDIMACS/QCIR solver that can provide boolean functions witnessing satisfiable queries (\(\textsf {QuAbS}\) [25], \(\textsf {CADET}\) [20], and \(\textsf {CAQE}\) [21]). For the remaining formats, i.e., DQDIMACS (\(\textsf {iDQ}\) [13]), TPTP3, and SMT (\(\textsf {Z3}\) [19], \(\textsf {CVC4}\) [2]), we only require format conformance as witness extraction is not supported, yet.

After the selected solver with corresponding encoding has finished processing the query and reports unsatisfiable, the search strategy determines how the bound for the next constraint encoding is increased. Currently, we have implemented a linear and an exponential search strategy. In case the solver reports satisfiable, the implementation will be extracted in the postprocessing component. The extraction depends on the encoding and solver support, we currently support it for SAT and QBF.

In case of the encoding to SAT, the solver delivers an assignment, which is then translated to our representation of the synthesized implementation. The transition function and the functions computing the outputs are represented as circuits.

In case of the QBF-encoding, we take a two-step approach for synthesis. The QBF query has the quantifier prefix \(\exists \forall \exists \) [10]. In synthesis mode, the query is solved by a combination of QBF preprocessor and QBF solver. From a satisfiable query, the assignment of the top-level existential quantification is extracted [23] and then used to reduce the original query by eliminating the top level existential quantifier. The resulting query, now with a \(\forall \exists \) prefix, is then solved using a certifying QBF solver that returns a certificate, that is a circuit representing the witnessing boolean functions. This certificate is then translated into the same functional representation of the synthesized implementation as in the SAT case.

This common representation of the implementations allows the translation into different output formats. From our representation, it is possible to translate the implementation into an AIGER circuit as required by the SYNTCOMP rules, to a SMV model for model checking, or to a graphical representation using the DOT format.

Further encodings can be integrated as extra components in the tool. Such an encoder component has access to the automaton, the semantics, and the input and output signals. The encoder must provide a method solve that takes as its parameter a bound and returns whether there is an implementation with the given bound that realizes the specification. The method is implemented by building the constraint system and solving it using a theory solver. One can either use our logic representation or build the textual solver representation directly. If the component supports synthesis, it implements a second method extractSolution that is called if solve returns true. It returns a representation of the realizing implementation as described above. In order to integrate new solver formats, one has to provide a translator from our logic representation to this format.

3 Experimentation

The reactive synthesis competition has a library of LTL benchmarks that can be transformed into the \(\textsf {BoSy}\) file format using the organizers’ conversion tool [15]. The tool \(\textsf {runsolver}\) [22] is used in our experiments to get predictable timing results and to set appropriate time and memory limits. Figure 2 compares the performance of the different encodings for determining realizability on the SYNTCOMP benchmark set. Notably, the encoding employing QBF solving performed better than the SAT-based one and both solve more instances than the original SMT encoding. The two encodings using DQBF are not yet competitive due to limited availability of DQBF solvers.

Fig. 2.
figure 2

Number of solved instances within 1 h among the 195 instances from SYNTCOMP 2016. The time axis has logarithmic scale. The experiment was run on a machine with a \(3.6\,\text {GHz}\) quad-core Intel Xeon processor.

Full size image

Different configurations of \(\textsf {BoSy}\) may not only result in varying running times, but may also effect the quality of the synthesized implementation. A measurement of the quality of the implementation that has also been used in the reactive synthesis competition is the size of the implementation, measured in the number of gates in the circuit representation. The correctness of an implementation, i.e., whether the synthesized solution actually satisfies the original specification can be verified by model checking. One can either encode the solution as a circuit and use an AIGER model checker, or one can use the SMV representation and model check it with \(\textsf {NuSMV}\) [7].

For a sample benchmark, a parametric load-balancer [9] instantiated with 5 clients, we provide experimental results for different configurations of \(\textsf {BoSy}\) in Fig. 3. The two automaton conversion tools produce significantly different automata, where the state space of the automaton produced by \(\textsf {spot}\) is only one third of the one produced by \(\textsf {ltl3ba}\). Consequently, the constraint system generated for the \(\textsf {ltl3ba}\) version is larger and thereby the running time worse compared to the \(\textsf {spot}\) version. This impact is stronger on the propositional encoding than on the input-symbolic one for realizability. An observation that also translates to other benchmarks is that the size of the implementation is usually smaller using the input-symbolic encoding. On the other hand, extracting solutions is cheaper in the propositional case as only assignments are extracted.

Fig. 3.
figure 3

The diagram shows the result on solving time and implementation quality for different configurations of \(\textsf {BoSy}\) on a sample specification.

Full size image