Practical Synthesis of Reactive Systems from LTL Specifications via Parity Games
share
The synthesis - the automatic construction - of reactive systems from linear temporal logic (LTL) specifications has recently seen a revival of the classic automata-theoretic approach based on parity-tree-automata, which outperformed other synthesis approaches in the last synthesis competition (Syntcomp2018). We describe a complete synthesis procedure that is based on the translation of LTL to deterministic parity automata and the emptiness check of the corresponding tree automata. The described approach is (1) structured, meaning that the states used in the construction have a structure, which is also (partly) preserved in the synthesis result, performs a (2) forward exploration and thus often only constructs a small subset of the reachable states, and is (3) incremental in the sense that it reuses results from previous unsuccessful solution attempts. We further explore the impact of different guiding heuristics that determine where to expand the on-the-fly built arena and present several mechanisms for extracting an implementation (Mealy machine or circuit). Furthermore, several data structures used in the implementation can be encoded symbolically reducing time and memory consumption. We compare the proposed techniques on the Syntcomp2017 benchmark set.
READ FULL TEXT