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

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.