Antichains and compositional algorithms for LTL synthesis

In this paper, we present new monolithic and compositional algorithms to solve the LTL realizability problem. Those new algorithms are based on a reduction of the LTL realizability problem to a game whose winning condition is defined by a universal automaton on infinite words with a k-co-Buchi acceptance condition. This acceptance condition asks that runs visit at most k accepting states, so it implicitly defines a safety game. To obtain efficient algorithms from this construction, we need several additional ingredients. First, we study the structure of the underlying automata constructions, and we show that there exists a partial order that structures the state space of the underlying safety game. This partial order can be used to define an efficient antichain algorithm. Second, we show that the algorithm can be implemented in an incremental way by considering increasing values of k in the acceptance condition. Finally, we show that for large LTL formulas that are written as conjunctions of smaller formulas, we can solve the problem compositionally by first computing winning strategies for each conjunct that appears in the large formula. We report on the behavior of those algorithms on several benchmarks. We show that the compositional algorithms are able to handle LTL formulas that are several pages long.