An Antichain Algorithm for {LTL} Realizability

TitleAn Antichain Algorithm for {LTL} Realizability
Publication TypeMiscellaneous
Year of Publication2009
AuthorsFiliot, E, Jin N, Raskin J-F

In this paper, we study the structure of underlying automata based constructions for solving the LTL realizability and synthesis problem. We show how to reduce the LTL realizability problem to a game with an observer that checks that the game visits a bounded number of times accepting states of a universal co-Büchi word automaton. We show that such an observer can be made deterministic and that this deterministic observer has a nice structure which can be exploited by an incremental algorithm that manipulates antichains of game positions. We have implemented this new algorithm and our first results are very encouraging.