figure a

1 Introduction

Reactive synthesis refers to the problem of finding for a formal specification of an input-output relation, in our case a linear temporal logic (LTL), a matching implementation [22], e.g. a Mealy machine or an and-inverter-graph (AIG). Since the automata-theoretic approach to synthesis involves the construction of a potentially double exponentially sized automaton (in the length of the specification) [13], most existing tools focus on symbolic and bounded methods in order to combat the state-space explosion [5, 9, 11, 18]. A beneficial side effect of these approaches is that they tend to yield succinct implementations.

In contrast to these approaches, we present a prototype implementation of an LTL synthesis tool which follows the automata theoretic approach using parity games as an intermediate step. StrixFootnote 1 uses the LTL-to-DPA translation presented in [10, 23] and the multi-threaded explicit-state parity game solver presented in [14, 20]: First, the given formula is decomposed into much simpler requirements, often resulting in a large number of safety and co-safety conditions and only a few requiring Büchi or parity acceptance conditions, which is comparable to the approach of [5, 21]. These requirements are then translated on-the-fly into automata, keeping the invariant that the parity game solver can easily compose the actual parity game. Further, by querying only for states that are actually required for deciding the winner, the implementation avoids unnecessary work.

The parity game solver is based on the strategy iteration of [19] which iteratively improves non-deterministic strategies, i.e. strategies that can allow several actions for a given state as long as they all are guaranteed to lead to the specified system behaviour. When translating the winning strategy into a Mealy automaton or an AIG this non-determinism can be used similarly to “don’t cares” when minimizing boolean circuits. Strategy iteration offers us two additional advantages, first, we can directly take advantage of multi-core systems; second, we can reuse the winning strategies which have been computed for the intermediate arenas.

Related Work and Experimental Evaluation. From the tools submitted to syntcomp2017, ltlsynt [15] is closest to our approach: it also combines an LTL-to-DPA-translation with an explicit-state parity game solver, but it does not intertwine the two steps, instead it uses a different approach for the translation leading to one monolithic DPA which is then turned in a parity game. In contrast, the two best performing tools from syntcomp2017, BoSy and Party, use bounded synthesis, by reduction either to SAT, SMT, or safety games.

In order to give a realistic estimation of how our tool would have faired at syntcomp2017 (TLSF/LTL track), we tried to re-create the benchmark environment of syntcomp2017 as close as possible on our hardware: in its current state, our tool would have been ranked below Party, but before ltlsynt and BoSy. Due to time and resource constraints, we could only do an in-depth comparison with the current version of ltlsynt; in particular we used the TLSF specification of the completeFootnote 2 AMBA protocol for \(n=2\) as a benchmark. We refer to Sect. 3 for details on the benchmarking procedure.

2 Design and Implementation

Strix is implemented in Java and C++. It supports LTL and TLSF [16] (only the reduced basic variant) as input languages, while the latter one is preferred, since it contains more information about the specification. We describe the main steps of the tool in the following paragraphs with examples given in Fig. 1.

Splitting and Translation. As a preprocessing step the specification is split into syntactic (co)safety and (co)Büchi formulas, and one remaining general LTL formula. These are then translated into the simplest deterministic automaton class using the constructions of [10, 23]. To speed up the process these automata are constructed on-the-fly, i.e., states are created only if requested by later stages. Furthermore, since DPAs can be easily complemented, the implementation translates the formula and its negation and chooses the faster obtained one.

Fig. 1.
figure 1

Synthesis of a simple arbiter with two clients. Here, a winning strategy is already obtained on the partial arena: always take any of the non-dashed edges.

Full size image

Arena Construction. Here we construct one product automaton and combine the various acceptance conditions into a single parity acceptance condition: for this, we use the idea underlying the last-appearance-record construction, known from the translation of Muller to parity games, to directly obtain a parity game again.

Parity Game Solving. The parity game solver runs in parallel to the arena construction on the partially constructed game in order to guide the translation process, with the possibility for early termination when a winning strategy for the system player is found. It uses strategy iteration that supports non-deterministic strategies [19] from which we can benefit in several ways: First, in the translation process, the current strategy stays valid when adding nodes to the arena and thus can be used as initial strategy when solving the extended arena. Second, the non-deterministic strategies allow us to later heuristically select actions of the strategy that minimize the generated controller and to identify irrelevant output signals (similar to “don’t care”-cells in Karnaugh maps). Finally, the strategy iteration can easily take advantage of multi-core architectures [14, 20].

Controller Generation and Minimization. From the non-deterministic strategy we obtain an incompletely specified Mealy machine and optionally pass it to the external SAT-based minimizer MeMin [1] for Mealy machines and extract a more compact description.

AIGER Circuit Generation and Minimization. We translate the minimized Mealy machine with the tool SpeculoosFootnote 3 into an AIGER circuit. In parallel, we also construct an AIGER circuit out of the non-minimized Mealy machine, since this can sometimes result in smaller circuits. The two AIGER circuits are then further compressed using ABC [6], and the smaller one is returned.

3 Experimental Evaluation

We evaluate Strix on the TLFS/LTL-track benchmark of the syntcomp2017 competition, which consists of 177 realizable and 67 unrealizable temporal logic synthesis specifications [15]. The experiment was run on a server with an Intel E5-2630 v4 clocked at 2.2 GHz (boost disabled). To mimic syntcomp2017 we imposed a limit of 8 threads for parallelization, a memory limit of 32 GB and a timeout of one hour for each specification. Every specification for that a tool correctly decides realizability within these limits is counted as solved for the category Realizability, and every specification for that it can additionally produce an AIGER circuit that is successfully verified is counted as solved for the category Synthesis. For this we verified the circuits with an additional time limit of one hour using the nuXmv model checker [7] with the check_ltlspec and check_ltlspec_klive routines in parallel.

We compared Strix with ltlsynt in the latest available release (version 2.5) at time of writing. This version differs from the one used during syntcomp2017 as it contains several improvements, but also performs worse in a few cases and exhibits erroneous behaviour: for Realizability, it produced one wrong answer, and for Synthesis, it failed in 72 cases to produce AIGER circuits due to a program error.

Additionally, we compare our results with the best configuration of the top tools competing in syntcomp2017: Party (portfolio), ltlsynt and BoSy (spot). Due to the difficulty of recreating the syntcomp2017 hardware setupFootnote 4, we compiled the results for these tools in Table 1 from the syntcomp2017 webpageFootnote 5 combining them with our results.

The Quality rating compares the size of the solutions according to the syntcomp2017 formula, where a tool gets \({2-\log _{10}\frac{n+1}{r+1}}\) quality points for each verified solution of size n for a specification with reference size r. We now move on to a detailed discussion of the results and their interpretation.

Table 1. Results for Strix compared with ltlsynt and selected results from syntcomp2017 on the TLSF/LTL-track benchmark and on noteable instances. We mark timeouts by time, memouts by mem, and errors by err.
Full size table

Realizability. We were able to correctly decide realizability for 163 and unrealizability for 51 specifications, resulting in 214 solved instances. We solve five instances that were previously unsolved in syntcomp2017.

Synthesis. We produced AIGER circuits for 148 of the realizable specifications. In 15 cases, we only constructed a Mealy machine, but the subsequent steps (MeMin for minimization or  Speculoos for circuit generation) reached the time or memory limit. We were able to verify correctness for 146 of the circuits, reaching the model checking time limit in two case. Together with the 51 specifications for which we determined unrealizability, this results in 197 solved instances.

Quality. We produced 36 solutions that are smaller than any solution during syntcomp2017. The most significant reductions are for the AMBA encoder and the full arbiter, with reductions of over 75%, and for ltl2dba_E_4 and ltl2dba_E_6, where we produce indeed the smallest implementation there is.

3.1 Effects of Minimization

We could reduce the size of the Mealy machine in 80 cases, and on average by 45%. However the data showed that this did not always reduce the size of the generated AIGER circuit: in 13 cases (most notably for several arbiter specifications) the size of the circuit generated from the Mealy machine actually increased when applying minimization (on average by 190%), while it decreased in 62 cases (on average by 55%).

We conjecture that the structure of the product-arena is sometimes amenable to compact representation in an AIGER circuit, while after the (SAT-based) minimization this is lost. In these cases the SAT/SMT-based bounded synthesis tools such as BoSy and Party also have difficulties producing a small solution, if any at all.

3.2 Synthesis of Complete AMBA AHB Arbiter

To test maturity and scalability of our tool, we synthesized the AMBA AHB arbiter [2], a common case study for reactive synthesis. We used the parameterized specification from [17] for \(n=2\) masters, which was also part of SYNTCOMP2016, but was left unsolved by any tool. With a memory limit of 128 GB, we could decide realizability within 26 min and produce a Mealy machine with 83 states after minimization. While specialised GR(1) solvers [2, 4, 12] or decompositional approaches [3] are able to synthesize the specification in a matter of minutes, to the best of our knowledge we are the first full LTL synthesis tool that can handle the complete non-decomposed specification in a reasonable amount of time. For comparison, ltlsynt (2.5) needs more than 2.5 days on our system and produces a Mealy machine with 340 states.

3.3 Discussion

The ltlsynt tool is part of Spot [8], which uses a Safra-style determinization procedure for NBAs. Conceptually, it also uses DPAs and a parity game solver as a decision procedure. However, as shown in [10] the produced automata tend to be larger compared to our translation, which probably results in the lower quality score. Our approach has similar performance and scales better on certain cases. The instances where ltlsynt performs better than Strix are specifications that we cannot split efficiently and the DPA construction becomes the bottleneck.

Bounded synthesis approaches tend to produce smaller Mealy machines and to be able to handle larger alphabets. However, they fail when the minimal machine implementing the desired property is large, even if there is a compact implementation as a circuit. In our approach, we can often solve these cases and still regain compactness of the implementation through minimization afterwards. The strength of the Party portfolio is the combination of traditional bounded synthesis and a novel approach by reduction to safety games, which results in a large number of solved instances, but reduces the avg. quality score.

Future Work. Strix combines Java (LTL simplification and automata translations) and C++ (parity game construction and solving). We believe that a pure C++ implementation will further improve the overall runtime and reduce the memory footprint. Next, there are several algorithmic questions we want to investigate going forward, especially expanding parallelization of the tool. Furthermore, we want to reduce the dependency on external tools for circuit generation in order to be able to fine-tune this step better. Especially replacing Speculoos is important, since it turned out that it was unable to handle complex transition systems.