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.
|Publication status||Published - 19 Jul 2021|
|Event||10th Workshop on Synthesis - Online|
Duration: 19 Jul 2021 → 19 Jul 2021
Conference number: 10
|Workshop||10th Workshop on Synthesis|
|Abbreviated title||SYNT 2021|
|Period||19/07/21 → 19/07/21|