2022

[1]Swen Jacobs [2]Guillermo A. Pérez

1]CISPA Helmholtz Center for Information Security, Stuhlsatzenhaus 5,
Saarbrücken, 66123, Germany 2]University of Antwerp – Flanders Make,
Middelheimlaan 1, Antwerpen, 2020, Belgium 3]University of Twente, The
Netherlands 4]University of Mons, Belgium 5]DePaul University, USA
6]Laboratoire de Recherche et Développement de l’Epita, France 7]Saarland
University Germany 8]Université libre de Bruxelles, Belgium 9]Technische
Universität München, Germany 10]University of Luxembourg, Luxembourg

# The Reactive Synthesis Competition (SYNTCOMP): 2018–2021

<EMAIL_ADDRESS><EMAIL_ADDRESS>Remco Abraham  Véronique Bruyère
Michaël Cadilhac  Maximilien Colange  Charly Delfosse  Tom van Dijk  Alexandre
Duret-Lutz  Peter Faymonville  Bernd Finkbeiner  Ayrat Khalimov  Felix Klein
Michael Luttenberger  Klara Meyer  Thibaud Michaud  Adrien Pommellet  Florian
Renkin  Philipp Schlehuber-Caissier  Mouhammad Sakr  Salomon Sickert  Gaëtan
Staquet  Clément Tamines  Leander Tentrup  Adam Walker  [  [  [  [  [  [  [  [
[  [

###### Abstract

We report on the last four editions of the reactive synthesis competition
(SYNTCOMP 2018–2021). We briefly describe the evaluation scheme and the
experimental setup of SYNTCOMP. Then, we introduce new benchmark classes that
have been added to the SYNTCOMP library and give an overview of the
participants of SYNTCOMP. Finally, we present and analyze the results of our
experimental evaluations, including a ranking of tools with respect to
quantity and quality of solutions.

###### keywords:

Reactive synthesis, algorithmic verification, zero-sum games

##  1 Introduction

Reactive systems are systems that maintain a continuous interaction with their
environment. The act of automatically constructing such a system from a given
formal specification (or determining that no such system exists) is called
_reactive synthesis_. The current definition of reactive synthesis is usually
attributed to Alonzo Church (Church, 1957, 1964). In the last 60 years,
several works have laid the theoretical foundations that underpin all current
synthesis algorithms for different instantiations of reactive synthesis.
Indeed, depending on the format in which a specification for the reactive
system is formalized, different synthesis problems arise.

Reactive synthesis has the potential to revolutionize the way in which
reactive systems are designed. This is due to the fact that a synthesized
system is correct by construction and therefore does not need to be tested nor
verified for correctness. Despite its potential, industry has not yet adopted
it nor the prototype tools implemented by academic researchers. This is in
contrast to other formal verification techniques such as model checking (Baier
and Katoen, 2008; Clarke et al, 2018). With an aim at increasing the impact of
reactive synthesis in industry and improve the quality of synthesis tools, the
Reactive Synthesis competition (SYNTCOMP) was founded in 2014 (Jacobs et al,
2017b). In short, the competition is designed to foster research into well-
engineered, scalable, and user-friendly synthesis tools. To realize this, the
competition organizers have proposed standards for benchmark formats, and
maintain a library of benchmarks with entries that remain challenging for
state-of-the-art tools. Most importantly, SYNTCOMP provides a dedicated and
independent platform for the objective comparison of synthesis tools.

SYNTCOMP has become an annual event associated with the International
Conference on Computer Aided Verification (CAV) and the Workshop on Synthesis
(SYNT). The organization team of competition has changed slightly from its
inception: In 2019, Guillermo A. Pérez joined the organization team and, since
2020, the competition has an advisory committee that presently consists of of
Roderick Bloem, Armin Biere, Salomon Sickert, Jean-François Raskin, Bernd
Finkbeiner, and Ayrat Khalimov. In terms of specification formats, the
competition currently has three of them: one for safety specifications defined
by monitoring circuits, one for linear-temporal-logic specifications, and one
for parity-game specifications. The last one, i.e. parity games, is the most
recent addition.

In this article we present the list of benchmark families that have been added
to the competition from 2018 to 2021 as well as the tools which participated
in the competition during the same years. Finally, we also highlight the most
interesting experimental results from these editions of the competition and
discuss the progress of synthesis tools observed in this time.

##  2 Setup, Rules, and Execution

We begin this section with a reminder on the foundations of the synthesis
problem.

###  2.1 Synthesis and realizability

An _infinite word_ $\alpha$ over an _alphabet_ $A$, i.e. $\alpha\in
A^{\omega}$, can be seen as a function $\alpha\colon\mathbb{N}_{>0}\to A$.
Thus, we write $\alpha(i)$ to refer to the $i$-th letter of $\alpha$.

######  Definition 1 (Infinite-word automata).

An ($\omega$-word) _automaton_ is a tuple $\mathcal{N}=(Q,q_{0},A,\Delta)$
where $Q$ is a finite set of states, $q_{0}\in Q$ is the initial state, $A$ is
a finite alphabet, and $\Delta\subseteq Q\times A\times Q$ is the transition
relation. We assume that for all $p\in Q$ and all $a\in A$ there exists $q\in
Q$ such that $(p,a,q)\in Q$.

The automaton is said to be _deterministic_ if for all $p\in Q$ and all $a\in
A$ we have that $(p,a,q_{1}),(p,a,q_{2})\in\Delta$ implies $q_{1}=q_{2}$. A
_run_ of $\mathcal{N}$ on a word $\alpha\in A^{\omega}$ is an infinite
sequence $\rho=q_{0}\alpha(1)q_{1}\alpha(2)\dots\in(Q\cdot A)^{\omega}$ such
that $(q_{i},\alpha(i+1),q_{i+1})\in\Delta$ for all $i\in\mathbb{N}$.

Automata are paired with a condition that determines which runs are
_accepting_. For the competition, we consider four such _acceptance
conditions_.

  * •

The _safety_ condition is defined with respect to a set $U\subseteq Q$ of
_unsafe states_. A run $\rho=q_{0}a_{1}q_{1}a_{2}\dots$ is accepting for this
condition, or safe, if and only if for all $i\in\mathbb{N}$ we have that
$q_{i}\not\in U$.

  * •

The _Büchi_ condition is defined with respect to a set of _Büchi_ states
$B\subseteq Q$. A run $\rho=q_{0}a_{1}q_{1}a_{2}\dots$ is accepting for this
condition if and only if for all $i\in\mathbb{N}$ there exists $j\geq i$ such
that $q_{j}\in B$. That is, the run visits Büchi states infinitely often.

  * •

The _co-Büchi_ condition is also defined with respect to the set $B\subseteq
Q$ of states. A run $\rho=q_{0}a_{1}q_{1}a_{2}\dots$ is accepting for the
condition if and only if there exists $i\in\mathbb{N}$ such that for all
$j\geq i$ we have that $q_{j}\not\in B$.

  * •

The _parity_ condition is defined with respect to a _priority function_
$p\colon Q\to\mathbb{N}$. A run $\rho=q_{0}a_{1}q_{1}a_{2}\dots$ is accepting
for the parity condition if and only if the value
$\liminf_{i\to\infty}p(q_{i})$ is even. That is, the smallest priority that
appears infinitely often along the run is even.

A word $\alpha$ is accepted by an automaton $\mathcal{N}$ if it has a run on
$\alpha$ that is accepting. In the sequel, it will sometimes be useful to
consider _universal automata_. Such an automaton $\mathcal{N}$ accepts a word
$\alpha$ if all its runs on $\alpha$ are accepting.

We denote by $\mathcal{L}(\mathcal{N})$ the _language_ of the automaton
$\mathcal{N}$, that is, the set of words that $\mathcal{N}$ accepts.

####  2.1.1 Synthesis games and strategies

######  Definition 2 (Games).

A _(Gale-Stewart) game_ on input and output alphabets $I$ and $O$,
respectively, is a two-player perfect-information game played by Eve and Adam
in rounds: Adam chooses an element $i_{k}\in I$ and Eve responds with an
element $o_{k}\in O$. A _play_ in such a game is an infinite word $\langle
i_{1},o_{1}\rangle\langle i_{2},o_{2}\rangle\dots\in(I\times O)^{\omega}$.

A game is paired with a _payoff set_ $P\subseteq(I\times O)^{\omega}$ that
determines who wins a play $\pi$. If $\pi\in P$ then _$\pi$ is winning for
Eve_, otherwise it is _winning for Adam_.

######  Definition 3 (Strategies).

A _strategy_ for Adam is a function $\tau\colon(I\times O)^{*}\to I$ which
maps every (possibly empty) play prefix to a choice of input letter.
Similarly, a _strategy for Eve_ is a function $\sigma\colon(I\times O)^{*}I\to
O$ which maps every play prefix and input letter to a choice of output letter.

A play $\pi=\langle i_{1},o_{1}\rangle\langle i_{2},o_{2}\rangle\dots$ is
_consistent with_ a strategy $\tau$ for Adam if $i_{k}=\tau(\langle
i_{1},o_{1}\rangle\dots\langle i_{k-1},o_{k-1}\rangle)$ for all
$k\in\mathbb{N}$; it is consistent with a strategy $\sigma$ for Eve if
$o_{k}=\sigma(\langle i_{1},o_{1}\rangle\dots\langle
i_{k-1},o_{k-1}\rangle,i_{k})$. A pair of strategies $\sigma$ and $\tau$ for
Eve and Adam, respectively, induces a unique play $\pi_{\sigma\tau}$
consistent with both $\sigma$ and $\tau$.

In a game with payoff set $P$, the strategy $\sigma$ for Eve is a _winning
strategy_ if for all strategies $\tau$ for Adam it holds that
$\pi_{\sigma\tau}\in P$; the strategy $\tau$ for Adam is winning if for all
strategies $\sigma$ for Eve we have $\pi_{\sigma\tau}\not\in P$.

The realizability and synthesis problems are defined for games whose payoff
sets are given as the language of an automaton. We sometimes refer to these as
_games played on automata_.

######  Definition 4 (Synthesis and realizability).

Consider finite input and output alphabets $I$ and $O$, respectively, and an
automaton $\mathcal{N}$ with alphabet $I\times O$. The _realizability problem_
asks whether there exists a winning strategy for Eve in the game with payoff
set $\mathcal{L}(\mathcal{N})$. The _synthesis problem_ further asks to
compute and output such a strategy if one exists.

####  2.1.2 Finite-memory strategies

A _finite-memory_ strategy $\sigma$ for Eve in a game played on the automaton
$\mathcal{N}=(Q,q_{0},I\times O,\Delta)$ with finite input and output
alphabets $I$ and $O$ is a strategy that can be encoded as a _(deterministic)
Mealy machine_ , that is, a finite-state machine that outputs a letter from
$\ignorespaces O$ when given a letter from  $\ignorespaces I$ . Formally, such
a machine is a tuple $\mathcal{M}=(S,s_{0},I,\lambda_{u},\lambda_{o})$ where
$S$ is a finite set of (memory) states, $s_{0}$ is the initial state,
$\lambda_{u}\colon S\times(Q\times I)\to S$ is the update function and
$\lambda_{o}\colon S\times(Q\times I)\to O$ is the output function. The
machine encodes $\sigma$ in the following way. For all play prefixes $\langle
i_{1},o_{1}\rangle\dots\langle i_{k-1},o_{k-1}\rangle$ and input letters
$i_{k}\in I$ we have that $\sigma(\langle i_{1},o_{1}\rangle\dots\langle
i_{k-1},o_{k-1}\rangle,i_{k})=\lambda_{o}(s_{k},i_{k})$ where
$s_{\ell+1}=\lambda_{u}(s_{\ell},i_{\ell})$ for all $\ell<k$. We then say the
strategy $\sigma$ has _memory_ $\lvert S\rvert$. In particular, when $\lvert
S\rvert=1$, we say the strategy is _memoryless_ (the term _positional_ is also
used in the literature). For all games considered in the competition, it holds
that there exists a winning strategy for Eve in the game if and only if there
exists a memoryless winning strategy for Eve.

###  2.2 Safety, parity, and linear-temporal specifications

Let $I$ and $O$ be finite input and output alphabets. SYNTCOMP has tracks
corresponding to three different versions of the synthesis and realizability
problems. The _safety tracks_ correspond to these problems for games played on
deterministic automata with a safety acceptance condition; the _parity tracks_
, to the same problems for games played on deterministic automata with a
parity acceptance condition. The remaining tracks correspond to games whose
payoff set is given in the form of a _linear-temporal-logic_ (LTL) formula. We
explain the connection between LTL formulas and infinite-word automata in the
following.

####  2.2.1 LTL-defined payoff sets

LTL (Pnueli, 1977) is a logic that allows one to naturally specify time
dependence among events that make up the formal specification of a system.
Formulas in LTL are constructed from a set $P$ of atomic propositions, the
usual Boolean connectives, and temporal operators
$\mathop{\mathtt{X}},\mathop{\mathtt{F}},\mathop{\mathtt{G}},\mathrel{\mathtt{U}}$
which intuitively correspond to “next”, “eventually”, “always”, and “until” in
English. Formally, LTL formulas conform to the following syntax:

$\varphi\Coloneqq a\in
P\mid\varphi\land\varphi\mid\lnot\varphi\mid\mathop{\mathtt{X}}\varphi\mid\mathop{\mathtt{F}}\varphi\mid\mathop{\mathtt{G}}\varphi\mid\varphi\mathrel{\mathtt{U}}\varphi$

with derived operators such as implication defined as usual. For instance, the
formula
$\mathop{\mathtt{G}}(\mathit{req}\rightarrow\mathop{\mathtt{F}}\mathit{grant})$,
over atomic propositions $\mathit{req}$ and $\mathit{grant}$, can be read as
“it is always the case that if there is a request then eventually it is
granted”. We refer the reader to the book by Baier and Katoen (2008) for the
formal semantics of LTL. In the context of words over an input-output alphabet
$I\times O$, the atomic propositions can be assumed to be an encoding of
letters in the alphabet. That is, the truth value of the propositions is
defined for each letter.

It is well known that the set $\mathrm{Words}(\varphi)$ of all words
satisfying a given LTL formula $\varphi$ can be “compiled” into an infinite-
word automaton. For instance, one can construct (in exponential time) an
automaton $\mathcal{N}$ with a Büchi acceptance condition such that
$\mathcal{L}(\mathcal{N})=\mathrm{Words}(\varphi)$ (Vardi and Wolper, 1984).
One can also construct (in doubly-exponential time) a deterministic automaton
$\mathcal{N}$ with a parity acceptance condition with the same property
(Safra, 1988; Piterman, 2007). The _LTL tracks_ of the competition correspond
to synthesis and realizability problems that can be solved by playing games on
a deterministic parity automaton compiled from a given LTL formula.

Note that, since the automaton is not explicitly given as input, algorithms
for either problem might construct different automata. Furthermore, algorithms
for both problems exist which avoid constructing a deterministc parity
automaton altogether.

####  2.2.2 Specification formats

We now briefly touch on the encoding used by the competition to represent the
input for the safety, parity, and LTL tracks.

Safety specifications.

To represent deterministic automata with a safety acceptance condition, we use
an extended version of the AIGER format (Biere, 2011). The latter is the
standard format in the hardware model checking competition (Biere, 2007). The
main reason that the basic format has to be extended is to allow for the
partitioning of the alphabet into $I$ and $O$ (Jacobs, 2014).

Parity specifications.

For automata with a parity acceptance condition, we use an extended version of
the Hanoi Omega-Automata (HOA) format (Babiak et al, 2015). The HOA format is
a flexible exchange format for infinite-word automata. Just like the AIGER
format, extending it is necessary to be able to include the partitioning of
alphabet into $I$ and $O$ (Pérez, 2019).

LTL specifications.

Finally, to represent LTL specifications we use the Temporal Logic Synthesis
Format (TLSF) (Jacobs et al, 2016). TLSF allows to define _families_ of LTL
specifications via parameters. Additionally, it allows to use high level
constructs, such as sets and functions, to provide a compact and human-
readable representation.

####  2.2.3 Output format

For the synthesis tracks, tools are expected to produce a strategy if the
specification is realizable. AIGER is the format used by the competition to
encode the Mealy machine implementing the strategy. In this case the standard
AIGER format is sufficient.

###  2.3 Rules

All tracks are divided into subtracks for realizability checking and
synthesis, and into two execution modes: sequential (using a single core of
the CPU) and parallel (using up to 4 cores). Every tool can run in up to three
configurations per subtrack and execution mode. Before the competition, all
tools are tested on a small benchmark set, and authors can submit bugfixes if
problems are found. Tools submitted by the organizers are not allowed to
submit bugfixes.

####  2.3.1 Ranking schemes

In all tracks, there is a ranking based on the number of correctly solved
problems within a $3600$s timeout. In the synthesis tracks, correctness of the
solution additionally has to be confirmed by a model checker. Additionally, in
synthesis tracks there is a ranking based on the quality of the solution,
measured by the number of gates in the produced AIGER circuit. To this end,
the size of the solution is compared to the size $r$ of a reference solution.
A circuit of the same size is rewarded $2$ points, and smaller or larger
solutions are awarded more or less points, respectively (see, e.g. Jacobs et
al (2017a), for more details).

####  2.3.2 Selection of benchmarks

In 2018, benchmarks were selected according to the same scheme as in previous
years, based on a categorization into different classes. From 2019 onward, all
available benchmarks were used. For TLSF-encoded families of benchmarks, more
instances are generated whenever all the existing ones are considered “too
easy” for more than one tool.

###  2.4 Execution

In 2018, SYNTCOMP was run at Saarland University. Benchmarking was again
organized on the EDACC platform (Balint et al, 2011). Since 2019, the
competition has been run on StarExec (Stump et al, 2014). This has had a few
consequences. The main such consequence is that not all legacy tools were
successfully migrated: some of them relied on deprecated packages while others
were implemented in languages with limited compiler support. Furthermore, such
tools lacked an active maintainer.

Our use of StarExec has significantly simplified the organizational effort,
while admittedly raising the entry threshold for participants a bit, since
they can, and must, themselves make sure that their code runs on the
competition servers. For an up-to-date overview of the specifications of the
StarExec service, we refer the reader to its website
111https://www.starexec.org/ and
wiki.222https://wiki.uiowa.edu/display/stardev/User+Guide

##  3 Benchmarks

We shortly comment on families of benchmarks that were added to each one of
the tracks during the relevant years.

###  3.1 LTL

Between 2018 and 2019, several _temporal-stream logic_ (TSL) benchmarks were
submitted to the LTL tracks of SYNTCOMP. TSL is a new temporal logic that
allows to separate control and data (Finkbeiner et al, 2019b). Among others,
the logic can be used to specify components of games implemented for FPGAs
(Geier et al, 2019) and to specify functional reactive programs (Finkbeiner et
al, 2019a). Importantly, bounded TSL specifications can be translated into LTL
specifications — this is how the benchmarks are obtained.

In addition to the TSL benchmarks, Felix Klein also submitted LTL benchmarks
based on hardware-component specifications and an encoding of an “infinite
duration tic-tac-toe”. In 2020 and 2021, TLSF files encoding families of LTL
specifications were used to generate more challenging benchmarks, i.e., larger
parameter values were used to generate more difficult instances of each family
to gauge how well tools scale w.r.t. the parameters.

###  3.2 Safety

In 2019, random examples were systematically generated by Mouhammad Sakr by
uniformly sampling from the set of all specifications with given values for
the number of (un)controllable inputs and latches. The techniques used for
this were subsequently improved and described by Jacobs and Sakr (2021).

###  3.3 Parity games

In 2020, Spot (Duret-Lutz et al, 2016) was used to generate deterministic
parity automata from some LTL benchmarks. It is important to mention that,
perhaps because this translation is doubly exponential in general, not many
specifications could be translated. Furthermore, the ones that did yield a
deterministic parity automaton resulted in small ones. In 2021,
combinatorially hard benchmarks were generated using the PGSolver parity-game
suite (Friedmann and Lange, 2009) and then translated to the extended HOA
format.

##  4 Active participants

In this section we give an overview of the participants of the 2018–2021
editions of SYNTCOMP. We mostly focus on the participants of the parity and
LTL tracks. The safety track had minimal active participation: in 2018, the
only tool that received an update was Simple BDD Solver, and the only new tool
was LazySynt, which participated hors concours. No updates or new tools were
submitted to the safety track after 2018.

Table 1: Links to tools and source code covered in this section Strix | https://github.com/meyerphi/strix | subsection 4.1
---|---|---
Otus | https://doi.org/10.5281/zenodo.5046346 | subsection 4.2
BoWSer | https://www.react.uni-saarland.de/tools/bowser/ | subsection 4.3
BoSy | https://www.react.uni-saarland.de/tools/bosy/ | subsection 4.4
LazySynt | https://github.com/mhdsakr/Lazy-Safety-Synthesis | subsection 4.6
Simple BDD Solver | https://github.com/adamwalker/syntcomp | subsection 4.5
Knor | https://github.com/trolando/knor | subsection 4.7
Party/Kid & sdf | https://github.com/5nizza/sdf-hoa | subsection 4.8
Ltlsynt | https://spot.lrde.epita.fr/ltlsynt.html | subsection 4.9
SPORE | https://github.com/Skar0/spore | subsection 4.10
Acacia bonsai | https://github.com/gaperez64/acacia-bonsai | subsection 4.11

Some of the tool descriptions below may refer to specialized techniques. We
refer the interested reader to the publications cited in the text further
details on such techniques.

###  4.1 Strix

Strix is a tool for LTL synthesis using transition-based deterministic parity
automata (tDPW) and parity games as intermediate steps. Since its inception
(Meyer et al, 2018), it proceeds in four stages: 1) Formula Rewriting and
Decomposition, 2) Automaton Construction, 3) Winning Strategy Computation, and
4) Controller Extraction. Note that stages 2 and 3 run in parallel, are on-
the-fly, and exchange information, such that the automaton construction can be
focused on critical states and early termination is possible. The improvements
applied for SYNTCOMP 2019 and 2020 are described by Luttenberger et al (2020)
and include a refined controller extraction stage or updates to the LTL-
translations based upon (Esparza et al, 2020) provided by Owl (Kretínský et
al, 2018). For SYNTCOMP 2021 the following major changes have been applied
(Meyer and Sickert, 2021):

  * •

LTL formulas are now translated to transition-based deterministic Emerson-Lei
automata (tDELA) by combining constructions ($\Delta_{2}$-normalisation,
direct translation to deterministic automata) from (Sickert and Esparza, 2020)
with a product construction adapted from (Müller and Sickert, 2017). Then
either a tDELA-to-tDPW construction based on Zielonka-trees or the Alternating
Cycle Decomposition is applied (Casares et al (2021, 2022)).

  * •

The strategy iteration algorithm by Luttenberger (2008) has been replaced by a
Rust implementation of the distraction fixpoint iteration algorithm (DFI) (van
Dijk and Rubbens, 2019).

###  4.2 Otus

Otus (Abraham, 2021) is a tool for LTL synthesis using symbolically-
represented parity automata and games. It proceeds as follows: the LTL formula
is decomposed into a Boolean combination of _simpler_ formulas, each of these
formulas are separately translated to BDD-encoded deterministic automata, and
then recomposed by computing the (deterministic) union and intersection on the
BDD-representation. Concretely, Otus makes use of the
$\Delta_{2}$-normalisation and the translation to deterministic (co-)Büchi
automata found in (Sickert and Esparza, 2020) implemented by Owl (Kretínský et
al, 2018), then computes the symbolic representation of a deterministic Rabin
automaton by union and intersection, and then applies a symbolic
implementation (Boker et al, 2010) to obtain a parity automaton. This symbolic
automaton is reinterpreted as a parity game and a symbolic implementation of
the distraction fix-point iteration (van Dijk and Rubbens, 2019; Lijzenga and
van Dijk, 2020a) is applied. In order to speed up the BDD-operations, Otus
makes use of the Sylvan BDD package (van Dijk and van de Pol, 2017).

###  4.3 BoWSer

BoWSer was updated by B. Finkbeiner and F. Klein. It implements different
extensions of the _bounded synthesis_ approach that solves the LTL synthesis
problem by first translating the complement of the specification into a Büchi
automaton, and then encoding acceptance of a transition system with bounded
number of states into a constraint system, in this case a propositional
satisfiability (SAT) problem. The details of all encodings are described in
Finkbeiner and Klein (2016). Compared to 2017, a number of small improvements
to speed up computations were implemented, and an experimental preprocessor to
simplify LTL formulas has been added. The sequential configurations of the
tool spawn multiple threads that are executed on a single CPU core. The
parallel configurations are mostly the same as the sequential ones, but use a
slightly different strategy for exploring the search space of solutions.

###  4.4 BoSy

BoSy was updated by P. Faymonville, B. Finkbeiner and L. Tentrup, and competed
in 2018 in both the realizability and the synthesis track. To detect
realizability, BoSy translates the (complement of the) LTL specification into
a safety automaton by bounding the number of visits to Büchi states. The
resulting safety game is solved by SafetySynth. For synthesis, BoSy relies on
an encoding into quantified Boolean formulas (QBF). A full account of the
algorithms implemented in the tool is given by Faymonville et al (2017). Two
configurations of BoSy competed in SYNTCOMP 2018: configuration (basic) and
configuration (opt), where the latter further improves the size of the
strategy by encoding the existence of an AIGER circuit representing the
strategy directly into a QBF query. Both configurations support a parallel
mode, if more than one core is available.

###  4.5 Simple BDD Solver

An update of Simple BDD Solver, submitted by Adam Walker, competed in the 2018
safety-realizability track. Simple BDD Solver implements the classical BDD-
based fixpoint algorithm for safety games (Jacobs et al, 2017b). In sequential
mode, it runs in three configurations, two of which are based on an
abstraction-refinement approach inspired by de Alfaro and Roy (2010), and one
without any abstraction. All three implement many important optimizations.
These configurations are the same as in 2017. Additionally, three new
configurations were entered for the parallel mode. These run different
portfolios of the algorithms in the sequential mode.

###  4.6 LazySynt

The _Symbolic Lazy Synthesis_ (LazySynt) tool was submitted in 2018 by M. Sakr
and S. Jacobs. It participated hors concours in the safety-synthesis track. In
contrast to the classical BDD-based algorithm and the SAT-based methods
implemented in Demiurge (Bloem et al, 2014; Seidl and Könighofer, 2014),
LazySynt implements a combined forward-backward search that is embedded into a
refinement loop, generating candidate solutions that are checked and refined
with a combination of backward model checking and forward generation of
additional constraints (Jacobs and Sakr, 2021).

###  4.7 Knor

Knor is a BDD-based solver for parity specifications. It leverages the Sylvan
BDD package (van Dijk and van de Pol, 2017) and the Oink parity-game solver
(van Dijk, 2018).

Knor implements a translation from HOA to a symbolic parity automaton encoded
using BDDs. Importantly, the chosen variable ordering encodes first source
states, then uncontrollable inputs, controllable inputs, and finally the
target states. The resulting symbolic parity automaton can then be treated in
two ways: First, it can be solved directly using a symbolic parity game
algorithm (Lijzenga and van Dijk, 2020b) optimized to utilize the
aforementioned variable ordering. This solution immediately yields a
controller that can be dumped as an AIG. Alternatively, the symbolic parity
automaton can be output as an explicit parity game. (Note that the previous
encoding into BDDs might have reduced the size of the automaton, exponentially
in some cases.) Such an explicit parity game can then solved by any of the
algorithms implemented in Oink. This last option does not yet support
synthesis, only realizability.

For the first solution, synthesis is realized using a naïve construction of an
AIG realizing the Mealy controller. There is a lot to be improved in the
latter step as it is a simple application of the Shannon expansion of the BDD-
encoded functions. Additionally, no preprocessing to improve the number of
latches of the controller, i.e. the state space of the parity-game solution,
is implemented.

For parity games derived from practical examples, the purely symbolic approach
performs very well; for contrived artificial constructions, solving an
explicit parity game in Oink is superior, though the choice of explicit
algorithm makes a big difference.

###  4.8 Party/Kid and sdf

Party/Kid and sdf implement variants of symbolic bounded synthesis (Ehlers,
2011, 2010). Both tools run two tasks, realizability and unrealizability, in
parallel. Below, we describe how the realizability check is done.
Unrealizability can be checked in a similar fashion by adequately modifying
the given LTL formula.

First, the tool translates the given LTL formula into a universal co-Büchi
automaton (UCW) using the TLSF-manipulation tool syfco (Jacobs et al, 2016)
and the Spot automata library (Duret-Lutz et al, 2016). Then, it iterates over
increasing bounds on the number of visits to final states of the UCW: given
such a bound, it translates the UCW into a universal safety automaton. The
universal safety automaton is then encoded into a safety game in a BDD-based
representation (using the CUDD library (Somenzi, 2005)), where each state of
the universal automaton gets a separate variable in the BDDs, thus avoiding
explicit determinization. The game is then solved using the standard fix-point
algorithm. The strategy extraction is also standard and does not use any
third-party tools.

Over the years 2017, 2018, 2021, three versions participated, with only
technical differences. The latest version (sdf, 2021) is written in C++.

###  4.9 Ltlsynt

Table 2: Versions of Spot on which ltlsynt submissions to SYNTCOMP were based. Year | Version |  Main changes in ltlsynt
---|---|---
2017 | pre-2.4 |  first implementation
2018 | 2.5.3 |  optimizations to determinization, and game solving; incremental determinization approach
2019 | 2.7.4 |  (bogus) LAR; improved LTL translation; incremental determinization removed
2020 | 2.9 |  reimplemented LAR, split, and game solving; parity minimization
2021 | 2.9.7 |  input decomposition; strategy simplification and specialized construction

The program ltlsynt, introduced to SYNTCOMP in 2017 (see Table 2) is part of
Spot (Duret-Lutz et al, 2016). It relies on a translation of the LTL
specification to a parity game whose winning strategy is then encoded as an
AIGER circuit. The version submitted to the 2021 edition features the
following improvements (Renkin et al, 2021):

  * •

A decomposition of the input specification when possible (Finkbeiner et al,
2021).

  * •

An LTL translation to Deterministic Emerson-Lei Automata (DELA) that handles
various simplifications: splitting the input formula in a manner similar to
the delag tool (Müller and Sickert, 2017), detecting _obligation_ subformulas
(Esparza et al, 2018), relying on weak automata and suspendable properties
(Babiak et al, 2013).

  * •

An SCC-based paritization algorithm (Renkin et al, 2020) for DELA that relies
on a _color appearance record_.

  * •

A transition-based parity game solver adapted from van Dijk (2018), supporting
(non-recursive) SCC decomposition and parity compression.

  * •

Optimization of the winning strategy through a variant of Spot’s simulation-
based reduction based on BDD signatures or an improvement of a SAT-based
minimization algorithm for Incompletely Specified Mealy Machines (Renkin et
al, 2022).

###  4.10 SPORE

SPORE is a prototype tool designed to assess the viability of using
generalized parity games for LTL realizability. The input LTL formula is first
decomposed into a conjunction of sub-formulas, which are in turn translated
into deterministic parity automata, composed into a synchronised (generalized
parity) product automaton, and finally translated into a generalized parity
game using the tlsf2gpg333See https://github.com/gaperez64/tlsf2gpg tool. The
game is then solved using a combination of the recursive algorithm for
generalized parity games (Chatterjee et al, 2007) and incomplete polynomial-
time algorithms, called partial solvers, presented in Bruyère et al (2019).
SPORE contains an explicit and a symbolic implementation of those algorithms,
the latter relying on Binary Decision Diagrams (BDDs) to represent the game
arena. The version presented in 2021 is implemented in Python with dd444See
https://github.com/tulip-control/dd as a library to manipulate BDDs.

###  4.11 Acacia bonsai

Acacia bonsai, the spiritual successor of Acacia+ (Bohy et al, 2012),
participated hors concours in the 2021 edition of the LTL-realizability track.
It implements _downset_ -based algorithms that avoid constructing a
deterministic automaton for the given LTL specification. Instead, the downsets
are used to efficiently store sets of states in an on-the-fly determinization
process. These algorithms were introduced by Filiot et al. in the 2010s and
implemented in the tools Acacia and Acacia+ in C and Python (Bohy, 2014).
Acacia bonsai is a complete rewrite of Acacia in C++20, articulated around
genericity and leveraging modern techniques for better performance. These
techniques include compile-time specialization of the algorithms, the use of
SIMD registers to store vectors, and several preprocessing steps, some relying
on efficient Binary Decision Diagram (BDD) libraries. It also includes
different data structures to store downsets such as k-d trees.

It is worth mentioning that, to compile the input LTL formula into an
automaton, Acacia bonsai uses Spot (Duret-Lutz et al, 2016).

##  5 Rankings and experiments

In this section we elaborate on the results of each track of the relevant
editions of SYNTCOMP. All data used for the graphs and analyses given below
can be fetched from https://syntcomp.react.uni-saarland.de/ for the 2018
edition and
https://www.starexec.org/starexec/secure/explore/spaces.jsp?id=329383 for
later editions.

###  5.1 Safety track

Despite the update submitted for the Simple BDD Solver tool, the tool rankings
did not change in 2018 compared to 2017. We refer the interested reader to the
SYNTCOMP’17 report (Jacobs et al, 2017a). In the following years, the safety
track has seen neither new participants nor updates to existing tools.

###  5.2 Parity track

In 2020 and 2021, two tools participated in the parity tracks: Strix and Knor.
The former is, oversimplifying, the parity-game solving component of the tool
Strix that is currently dominating the LTL track. Knor implements several
classical and novel parity-game solving algorithms and combinations thereof.
In 2020, both tools competed in the realizability track only. In 2021, they
competed in the synthesis track only and in a special _combinatorially hard_
realizability track. For these two initial editions of the parity tracks, no
distinction was made between sequential and parallel subtracks.

The rankings are summarized in Table 3. Probably the most important insight
from the results of these tracks is that Knor-BDD — which only participated
hors concours in 2020, but later became the default configuration of Knor —
outperformed both Strix and Knor by almost an order of magnitude only by
switching to a symbolic representation of the input game.

Table 3: Rankings for the parity tracks of the 2020 and 2021 editions of SYNTCOMP | Real. (2020) | Synth. (2021) | Qual. Rank (2021) | Hard Real (2021)
---|---|---|---|---
1st place | Strix | Knor-BDD | Strix | Knor-BDD
2nd place | Knor | Strix | Knor-BDD | Strix

###  5.3 LTL track

The LTL track has been running since 2016 and the set of (actively)
participating tools has changed a bit since. In Figure 1, we depict the
changes in the LTL-realizability rankings every year since 2017. Here, and in
similar graphs shown in the rest of this article, we have selected the best
configuration submitted per tool. Additionally, all tools — regardless of
whether they were parallel or sequential — were assigned as score the number
of benchmarks solved within the same time limits. It is noteworthy that the
best tool in 2017 implemented bounded-synthesis algorithms, whereas in recent
years the competition has been dominated by parity-game-based tools which
focus on optimizing the LTL-to-automaton compilation. Namely, Strix has
remained first in all rankings since 2018.

Figure 1: Bump plot of the rankings for the LTL realizability tracks for all
editions of SYNTCOMP 2017–2021 (2017 included for reference since some tools
are no longer actively participating)

Regarding 2021, in Figure 2 we have plotted the total amount of time it takes
for each tool to solve increasing numbers of benchmarks. Once more, we do not
distinguish between parallel and sequential tools. For reference, we have also
included Acacia bonsai in the plot, even if it only participated hors
concours.

Figure 2: Cactus (a.k.a. survival) plots for the participants of the LTL
realizability track of SYNTCOMP 2021; Note that the y-axis is displayed using
logarithmic scale

In what follows, we analyze the time and quality rankings of the tools in the
synthesis subtrack of the 2018 and 2021 editions of SYNTCOMP. Note that from
2019 to 2020 only ltlsynt and Strix participated, and they did so too in 2021,
hence our choice of representative years. Additionally, we present the state
of the art in terms of scalability for different parameterized families of
benchmarks we have used for the competition.

Figure 3: Cactus (a.k.a. survival) plots for the participants of the LTL
synthesis track of SYNTCOMP 2018 (left) and 2021 (right); Again, the y-axis is
displayed using logarithmic scale

####  5.3.1 Synthesis subtrack 2018, 2021

In Figure 3 we have plotted, for each tool, the total amount of time it takes
for it to solve increasing numbers of benchmarks. Here, we included
configurations from previous years of tools which were updated and Party (as
legacy tool) for reference. Additionally, both realizable and unrealizable
benchmarks were counted for the score. The previous results should be compared
with Figure 4, where we have plotted the total size of the outputs generated
for increasing numbers of (realizable) benchmarks.

Figure 4: Cactus plots for the participants of the LTL synthesis track of
SYNTCOMP 2018 (left) and 2021 (right) — this time, showing total output size
instead of time (counting AND-gates only); Note that the y-axis is displayed
using logarithmic scale

####  5.3.2 Parameterized families of benchmarks

Presently, we focus on families of LTL specifications defined by TLSF
benchmarks with parameters. In 2021, LTL specifications coming from 26 such
TLSF files were used in the competition. For most of those families, the
results are consistent with the previously summarized results, i.e., the
rankings of the tools are preserved when restricting the score to solved
benchmarks in that set only. However, some exceptions do exist.

For instance, the families of combinatorial logic specifications mux and
shift, which specify transducers realizing a mutiplexer and a barrel shifter,
respectively, are solved most efficiently by tools other than Strix. See
Figure 5 for the relevant plots. Other exceptions include the collector_v2 and
detector families of benchmarks, see Figure 6. For the former, the (total)
solving time for the best tool is more than order of magnitude smaller than
that of Strix. Other interesting families include arbiter specifications such
as the round_robin_arbiter and the full_arbiter families. There, Strix is
still best overall, but not consistently so, see Figure 7.

Figure 5: Cactus plots for all the participants of the LTL synthesis track of
SYNTCOMP 2021, restricted to the mux (left) and shift (right) benchmark
families

Figure 6: Cactus plots for all the participants of the LTL synthesis track of
SYNTCOMP 2021, restricted to the collector_v2 (left) and detector (right)
benchmark families

Figure 7: Cactus plots for all the participants of the LTL synthesis track of
SYNTCOMP 2021, restricted to the round_robin_arbiter (left) and full_arbiter
(right) benchmark families

##  6 Conclusion

In this article we have reported on the last four editions of SYNTCOMP, the
reactive synthesis competition. Furthermore, we analyzed the results of our
experimental evaluations, including a ranking of the participating tools with
respect to quantity and quality of solutions. We observe a measurable
improvement in terms of the performance of the top solvers in each track.
Additionally, the number of collected benchmarks continues to grow.

In future editions, we will try to replicate the success of the new parity
track. Indeed, several teams submitting solvers to it eventually ended up
extending their tool to participate in the LTL tracks as well. Finally, we
will also update some of the rules of the competition so that it remains
interesting to the community.

##### Changes to rules

Starting with the 2022 edition of the competition, the following changes will
be implemented:

Benchmark copyright.

All submitted benchmarks will be made publicly available via our
repository555Currently hosted here: https://github.com/SYNTCOMP/benchmarks
under a CC-BY license.

Parallel tracks.

We will no longer differentiate between tool submissions to sequential and
parallel tracks. Instead, we will make this distinction in the rankings by
basing it on the wallclock time and user-CPU time used by the tools per
benchmark. Regarding concrete time limits, all tools will be allowed $10.000$s
wall-clock time and $4\times 10.000$s user-CPU time since each _job pair_ ran
on StarExec has access to one 4-core CPU.

StarExec.

For the next 3–5 years, at least, we will continue using StarExec to host the
competition. We will follow its evolution in terms of hardware and will later
revisit the question of whether alternative (locally hosted) frameworks better
fit the needs of the competition and the community.

## References

  *   * Abraham (2021) Abraham R (2021) Symbolic LTL reactive synthesis. URL http://essay.utwente.nl/87386/
  * de Alfaro and Roy (2010) de Alfaro L, Roy P (2010) Solving games via three-valued abstraction refinement. Inf Comput 208(6):666–676. 10.1016/j.ic.2009.05.007, URL https://doi.org/10.1016/j.ic.2009.05.007
  * Babiak et al (2013) Babiak T, Badie T, Duret-Lutz A, et al (2013) Compositional approach to suspension and other improvements to LTL translation. In: Proceedings of the 20th International SPIN Symposium on Model Checking of Software (SPIN’13), Lecture Notes in Computer Science, vol 7976. Springer, pp 81–98, 10.1007/978-3-642-39176-7_6
  * Babiak et al (2015) Babiak T, Blahoudek F, Duret-Lutz A, et al (2015) The hanoi omega-automata format. In: Kroening D, Pasareanu CS (eds) Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, Lecture Notes in Computer Science, vol 9206. Springer, pp 479–486, 10.1007/978-3-319-21690-4_31, URL https://doi.org/10.1007/978-3-319-21690-4_31
  * Baier and Katoen (2008) Baier C, Katoen J (2008) Principles of model checking. MIT Press
  * Balint et al (2011) Balint A, Diepold D, Gall D, et al (2011) EDACC - an advanced platform for the experiment design, administration and analysis of empirical algorithms. In: Coello CAC (ed) Learning and Intelligent Optimization - 5th International Conference, LION 5, Rome, Italy, January 17-21, 2011. Selected Papers, Lecture Notes in Computer Science, vol 6683. Springer, pp 586–599, 10.1007/978-3-642-25566-3_46, URL https://doi.org/10.1007/978-3-642-25566-3_46
  * Biere (2007) Biere A (2007) Hardware model checking competition. http://fmv.jku.at/hwmcc/
  * Biere (2011) Biere A (2011) Aiger format and toolbox. http://fmv.jku.at/aiger/
  * Bloem et al (2014) Bloem R, Könighofer R, Seidl M (2014) Sat-based synthesis methods for safety specs. In: McMillan KL, Rival X (eds) Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings, Lecture Notes in Computer Science, vol 8318. Springer, pp 1–20, 10.1007/978-3-642-54013-4_1, URL https://doi.org/10.1007/978-3-642-54013-4_1
  * Bohy (2014) Bohy A (2014) Antichain based algorithms for the synthesis of reactive systems. PhD thesis, University of Mons
  * Bohy et al (2012) Bohy A, Bruyère V, Filiot E, et al (2012) Acacia+, a tool for LTL synthesis. In: Madhusudan P, Seshia SA (eds) CAV, LNCS, vol 7358. Springer, pp 652–657, 10.1007/978-3-642-31424-7_45, URL https://doi.org/10.1007/978-3-642-31424-7_45
  * Boker et al (2010) Boker U, Kupferman O, Steinitz A (2010) Parityizing rabin and streett. In: Lodaya K, Mahajan M (eds) IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010, December 15-18, 2010, Chennai, India, LIPIcs, vol 8. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp 412–423, 10.4230/LIPIcs.FSTTCS.2010.412, URL https://doi.org/10.4230/LIPIcs.FSTTCS.2010.412
  * Bruyère et al (2019) Bruyère V, Pérez GA, Raskin J, et al (2019) Partial solvers for generalized parity games. In: Filiot E, Jungers RM, Potapov I (eds) Reachability Problems - 13th International Conference, RP 2019, Brussels, Belgium, September 11-13, 2019, Proceedings, Lecture Notes in Computer Science, vol 11674. Springer, pp 63–78, 10.1007/978-3-030-30806-3_6, URL https://doi.org/10.1007/978-3-030-30806-3_6
  * Casares et al (2021) Casares A, Colcombet T, Fijalkow N (2021) Optimal transformations of games and automata using muller conditions. In: Bansal N, Merelli E, Worrell J (eds) 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, July 12-16, 2021, Glasgow, Scotland (Virtual Conference), LIPIcs, vol 198. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp 123:1–123:14, 10.4230/LIPIcs.ICALP.2021.123, URL https://doi.org/10.4230/LIPIcs.ICALP.2021.123
  * Casares et al (2022) Casares A, Duret-Lutz A, Meyer KJ, et al (2022) Practical applications of the alternating cycle decomposition. In: Fisman D, Rosu G (eds) Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II, Lecture Notes in Computer Science, vol 13244. Springer, pp 99–117, 10.1007/978-3-030-99527-0_6, URL https://doi.org/10.1007/978-3-030-99527-0_6
  * Chatterjee et al (2007) Chatterjee K, Henzinger TA, Piterman N (2007) Generalized parity games. In: Seidl H (ed) Foundations of Software Science and Computational Structures, 10th International Conference, FOSSACS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007, Braga, Portugal, March 24-April 1, 2007, Proceedings, Lecture Notes in Computer Science, vol 4423. Springer, pp 153–167, 10.1007/978-3-540-71389-0_12, URL https://doi.org/10.1007/978-3-540-71389-0_12
  * Church (1957) Church A (1957) Application of Recursive Arithmetic to the Problem of Circuit Synthesis, Summaries of the Summer Institute of Symbolic Logic, vol 1, American Mathematical Society, pp 3–50
  * Church (1964) Church A (1964) Logic, arithmetic, and automata. Journal of Symbolic Logic 29(4)
  * Clarke et al (2018) Clarke EM, Henzinger TA, Veith H, et al (eds) (2018) Handbook of Model Checking. Springer, 10.1007/978-3-319-10575-8, URL https://doi.org/10.1007/978-3-319-10575-8
  * van Dijk (2018) van Dijk T (2018) Oink: An implementation and evaluation of modern parity game solvers. In: Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’18), Springer, pp 291–308, 10.1007/978-3-319-89960-2_16
  * van Dijk and van de Pol (2017) van Dijk T, van de Pol J (2017) Sylvan: multi-core framework for decision diagrams. Int J Softw Tools Technol Transf 19(6):675–696. 10.1007/s10009-016-0433-2, URL https://doi.org/10.1007/s10009-016-0433-2
  * van Dijk and Rubbens (2019) van Dijk T, Rubbens B (2019) Simple fixpoint iteration to solve parity games. In: Leroux J, Raskin J (eds) Proceedings Tenth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2019, Bordeaux, France, 2-3rd September 2019, pp 123–139, 10.4204/EPTCS.305.9, URL https://doi.org/10.4204/EPTCS.305.9
  * Duret-Lutz et al (2016) Duret-Lutz A, Lewkowicz A, Fauchille A, et al (2016) Spot 2.0 — a framework for LTL and $\omega$-automata manipulation. In: Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA’16), Lecture Notes in Computer Science, vol 9938. Springer, pp 122–129, 10.1007/978-3-319-46520-3_8
  * Ehlers (2010) Ehlers R (2010) Symbolic bounded synthesis. In: International conference on computer aided verification, Springer, pp 365–379
  * Ehlers (2011) Ehlers R (2011) Unbeast: Symbolic bounded synthesis. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer, pp 272–275
  * Esparza et al (2018) Esparza J, Křetínský J, Sickert S (2018) One theorem to rule them all: A unified translation of LTL into $\omega$-automata. In: Dawar A, Grädel E (eds) Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS’18). ACM, pp 384–393, 10.1145/3209108.3209161
  * Esparza et al (2020) Esparza J, Kretínský J, Sickert S (2020) A unified translation of linear temporal logic to  $\ignorespaces\omega$ -automata. J ACM 67(6):33:1–33:61. 10.1145/3417995, URL https://doi.org/10.1145/3417995
  * Faymonville et al (2017) Faymonville P, Finkbeiner B, Tentrup L (2017) Bosy: An experimentation framework for bounded synthesis. In: Majumdar R, Kuncak V (eds) Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II, Lecture Notes in Computer Science, vol 10427. Springer, pp 325–332, 10.1007/978-3-319-63390-9_17, URL https://doi.org/10.1007/978-3-319-63390-9_17
  * Finkbeiner and Klein (2016) Finkbeiner B, Klein F (2016) Bounded cycle synthesis. In: Chaudhuri S, Farzan A (eds) Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, Lecture Notes in Computer Science, vol 9779. Springer, pp 118–135, 10.1007/978-3-319-41528-4_7, URL https://doi.org/10.1007/978-3-319-41528-4_7
  * Finkbeiner et al (2019a) Finkbeiner B, Klein F, Piskac R, et al (2019a) Synthesizing functional reactive programs. In: Eisenberg RA (ed) Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell, Haskell@ICFP 2019, Berlin, Germany, August 18-23, 2019. ACM, pp 162–175, 10.1145/3331545.3342601, URL https://doi.org/10.1145/3331545.3342601
  * Finkbeiner et al (2019b) Finkbeiner B, Klein F, Piskac R, et al (2019b) Temporal stream logic: Synthesis beyond the bools. In: Dillig I, Tasiran S (eds) Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I, Lecture Notes in Computer Science, vol 11561. Springer, pp 609–629, 10.1007/978-3-030-25540-4_35, URL https://doi.org/10.1007/978-3-030-25540-4_35
  * Finkbeiner et al (2021) Finkbeiner B, Geier G, Passing N (2021) Specification decomposition for reactive synthesis. In: Proceedings for the 13th NASA Formal Methods Symposium (NFM’21), 10.1007/978-3-030-76384-8_8
  * Friedmann and Lange (2009) Friedmann O, Lange M (2009) Solving parity games in practice. In: Liu Z, Ravn AP (eds) Automated Technology for Verification and Analysis, 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009. Proceedings, Lecture Notes in Computer Science, vol 5799. Springer, pp 182–196, 10.1007/978-3-642-04761-9_15, URL https://doi.org/10.1007/978-3-642-04761-9_15
  * Geier et al (2019) Geier G, Heim P, Klein F, et al (2019) Syntroids: Synthesizing a game for FPGAs using temporal logic specifications. In: Barrett CW, Yang J (eds) 2019 Formal Methods in Computer Aided Design, FMCAD 2019, San Jose, CA, USA, October 22-25, 2019. IEEE, pp 138–146, 10.23919/FMCAD.2019.8894261, URL https://doi.org/10.23919/FMCAD.2019.8894261
  * Jacobs (2014) Jacobs S (2014) Extended AIGER format for synthesis. CoRR abs/1405.5793. URL http://arxiv.org/abs/1405.5793, https://arxiv.org/abs/1405.5793
  * Jacobs and Sakr (2021) Jacobs S, Sakr M (2021) AIGEN: random generation of symbolic transition systems. In: Silva A, Leino KRM (eds) Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II, Lecture Notes in Computer Science, vol 12760. Springer, pp 435–446, 10.1007/978-3-030-81688-9_20, URL https://doi.org/10.1007/978-3-030-81688-9_20
  * Jacobs et al (2016) Jacobs S, Klein F, Schirmer S (2016) A high-level LTL synthesis format: TLSF v1.1. In: Piskac R, Dimitrova R (eds) Proceedings Fifth Workshop on Synthesis, SYNT@CAV 2016, Toronto, Canada, July 17-18, 2016, pp 112–132, 10.4204/EPTCS.229.10, URL https://doi.org/10.4204/EPTCS.229.10
  * Jacobs et al (2017a) Jacobs S, Basset N, Bloem R, et al (2017a) The 4th reactive synthesis competition (SYNTCOMP 2017): Benchmarks, participants & results. In: Fisman D, Jacobs S (eds) Proceedings Sixth Workshop on Synthesis, SYNT@CAV 2017, Heidelberg, Germany, 22nd July 2017, pp 116–143, 10.4204/EPTCS.260.10, URL https://doi.org/10.4204/EPTCS.260.10
  * Jacobs et al (2017b) Jacobs S, Bloem R, Brenguier R, et al (2017b) The first reactive synthesis competition (SYNTCOMP 2014). Int J Softw Tools Technol Transf 19(3):367–390. 10.1007/s10009-016-0416-3, URL https://doi.org/10.1007/s10009-016-0416-3
  * Kretínský et al (2018) Kretínský J, Meggendorfer T, Sickert S (2018) Owl: A library for  $\ignorespaces\omega$ -words, automata, and LTL. In: Lahiri SK, Wang C (eds) Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings, Lecture Notes in Computer Science, vol 11138. Springer, pp 543–550, 10.1007/978-3-030-01090-4_34, URL https://doi.org/10.1007/978-3-030-01090-4_34
  * Lijzenga and van Dijk (2020a) Lijzenga O, van Dijk T (2020a) Symbolic parity game solvers that yield winning strategies. In: Raskin J, Bresolin D (eds) Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2020, Brussels, Belgium, September 21-22, 2020, pp 18–32, 10.4204/EPTCS.326.2, URL https://doi.org/10.4204/EPTCS.326.2
  * Lijzenga and van Dijk (2020b) Lijzenga O, van Dijk T (2020b) Symbolic parity game solvers that yield winning strategies. In: Raskin J, Bresolin D (eds) Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2020, Brussels, Belgium, September 21-22, 2020, pp 18–32, 10.4204/EPTCS.326.2, URL https://doi.org/10.4204/EPTCS.326.2
  * Luttenberger (2008) Luttenberger M (2008) Strategy iteration using non-deterministic strategies for solving parity games. CoRR abs/0806.2923. URL http://arxiv.org/abs/0806.2923, https://arxiv.org/abs/arXiv:0806.2923
  * Luttenberger et al (2020) Luttenberger M, Meyer PJ, Sickert S (2020) Practical synthesis of reactive systems from LTL specifications via parity games. Acta Informatica 57(1-2):3–36. 10.1007/s00236-019-00349-3, URL https://doi.org/10.1007/s00236-019-00349-3
  * Meyer and Sickert (2021) Meyer PJ, Sickert S (2021) Modernising strix. Presented at the 10th Workshop on Synthesis
  * Meyer et al (2018) Meyer PJ, Sickert S, Luttenberger M (2018) Strix: Explicit reactive synthesis strikes back! In: Chockler H, Weissenbacher G (eds) Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I, Lecture Notes in Computer Science, vol 10981. Springer, pp 578–586, 10.1007/978-3-319-96145-3_31, URL https://doi.org/10.1007/978-3-319-96145-3_31
  * Müller and Sickert (2017) Müller D, Sickert S (2017) LTL to deterministic Emerson-Lei automata. In: Bouyer P, Orlandini A, Pietro PS (eds) Proceedings of the Eighth International Symposium on Games, Automata, Logics and Formal Verification (GandALF’17), pp 180–194, 10.4204/EPTCS.256.13
  * Pérez (2019) Pérez GA (2019) The extended HOA format for synthesis. CoRR abs/1912.05793. URL http://arxiv.org/abs/1912.05793, https://arxiv.org/abs/1912.05793
  * Piterman (2007) Piterman N (2007) From nondeterministic büchi and streett automata to deterministic parity automata. Log Methods Comput Sci 3(3). 10.2168/LMCS-3(3:5)2007, URL https://doi.org/10.2168/LMCS-3(3:5)2007
  * Pnueli (1977) Pnueli A (1977) The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977. IEEE Computer Society, pp 46–57, 10.1109/SFCS.1977.32, URL https://doi.org/10.1109/SFCS.1977.32
  * Renkin et al (2020) Renkin F, Duret-Lutz A, Pommellet A (2020) Practical “paritizing” of Emerson-Lei automata. In: Proceedings of the 18th International Symposium on Automated Technology for Verification and Analysis (ATVA’20), Lecture Notes in Computer Science, vol 12302. Springer, pp 127–143, 10.1007/978-3-030-59152-6_7
  * Renkin et al (2021) Renkin F, Schlehuber P, Duret-Lutz A, et al (2021) Improvements to ltlsynt. Presented at the 10th Workshop on Synthesis, URL https://hal.archives-ouvertes.fr/hal-03523385
  * Renkin et al (2022) Renkin F, Schlehuber-Caissier P, Duret-Lutz A, et al (2022) Effective reductions of Mealy machines. In: Proceedings of the 42nd International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE’22). Springer, Lecture Notes in Computer Science, to appear
  * Safra (1988) Safra S (1988) On the complexity of omega-automata. In: 29th Annual Symposium on Foundations of Computer Science, White Plains, New York, USA, 24-26 October 1988. IEEE Computer Society, pp 319–327, 10.1109/SFCS.1988.21948, URL https://doi.org/10.1109/SFCS.1988.21948
  * Seidl and Könighofer (2014) Seidl M, Könighofer R (2014) Partial witnesses from preprocessed quantified boolean formulas. In: Fettweis GP, Nebel W (eds) Design, Automation & Test in Europe Conference & Exhibition, DATE 2014, Dresden, Germany, March 24-28, 2014. European Design and Automation Association, pp 1–6, 10.7873/DATE.2014.162, URL https://doi.org/10.7873/DATE.2014.162
  * Sickert and Esparza (2020) Sickert S, Esparza J (2020) An efficient normalisation procedure for linear temporal logic and very weak alternating automata. In: Hermanns H, Zhang L, Kobayashi N, et al (eds) LICS ’20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020. ACM, pp 831–844, 10.1145/3373718.3394743, URL https://doi.org/10.1145/3373718.3394743
  * Somenzi (2005) Somenzi F (2005) CUDD package, release 2.4.1. http://vlsi.colorado.edu/~fabio/CUDD/
  * Stump et al (2014) Stump A, Sutcliffe G, Tinelli C (2014) Starexec: A cross-community infrastructure for logic solving. In: Demri S, Kapur D, Weidenbach C (eds) Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings, Lecture Notes in Computer Science, vol 8562. Springer, pp 367–373, 10.1007/978-3-319-08587-6_28, URL https://doi.org/10.1007/978-3-319-08587-6_28
  * Vardi and Wolper (1984) Vardi MY, Wolper P (1984) Automata theoretic techniques for modal logics of programs (extended abstract). In: DeMillo RA (ed) Proceedings of the 16th Annual ACM Symposium on Theory of Computing, April 30 - May 2, 1984, Washington, DC, USA. ACM, pp 446–456, 10.1145/800057.808711, URL https://doi.org/10.1145/800057.808711