Almost-Symbolic Synthesis via Delta-2-Normalisation for Linear Temporal Logic

Tom van Dijk, Remco Abraham, Salomon Sickert

Research output: Contribution to conferencePaperpeer-review


The classic approach to synthesis of reactive systems from linear temporal logic (LTL) specifications involves the translation of the specification to a deterministic omega-automaton and computing a winning strategy for the corresponding game with an omega-regular winning condition. Unfortunately, this procedure has an unavoidable double-exponential blow-up in the worst-case and suffers from the state-explosion problem. To address this state-explosion problem in practice we propose an almost-symbolic version of this classic idea that performs the following steps: (1) normalisation of the specification into a Boolean combination of simple fragment of LTL, (2) translation of each simple subformula into a deterministic automaton, (3) encoding of each automaton into a binary decision diagram (BDD), (4) construction of a parity automaton (and thus game) by operations on the BDD, (5) symbolic computation of a winning strategy, and finally (6) extraction of a symbolic controller. We prototype this approach in the tool Otus, compare it against Strix, the winner of SYNTCOMP 2018-2020, on the SYNTCOMP benchmarks, and identify several specifications where Otus outperforms Strix.
Original languageEnglish
Publication statusPublished - 19 Jul 2021
Event10th Workshop on Synthesis - Online
Duration: 19 Jul 202119 Jul 2021
Conference number: 10


Workshop10th Workshop on Synthesis
Abbreviated titleSYNT 2021
Internet address


Dive into the research topics of 'Almost-Symbolic Synthesis via Delta-2-Normalisation for Linear Temporal Logic'. Together they form a unique fingerprint.

Cite this