Antichains and Compositional Algorithms for LTL synthesis

Emmanuel Filiot
ULB
Friday, 18 February, 2011 - 16:00
Room: A2.122

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-Büchi acceptance condition. This acceptance condition asks that runs visit at most k accepting states, so it implicitl
y 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 u
sed 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. Fin
ally, 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 app
ears 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.

Based on a joint work with Naiyong Jin and Jean-François Raskin.