Abstract : 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.
https://hal.inria.fr/inria-00489952 Contributor : Emmanuel FiliotConnect in order to contact the contributor Submitted on : Monday, June 7, 2010 - 2:40:26 PM Last modification on : Tuesday, October 19, 2021 - 12:55:34 PM Long-term archiving on: : Friday, September 17, 2010 - 1:05:27 PM