An Antichain Algorithm for {LTL} Realizability

TitleAn Antichain Algorithm for {LTL} Realizability
Publication TypeMiscellaneous
Year of Publication2009
AuthorsFiliot, E, Jin N, Raskin J-F
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.

URLHAL: http://hal.archives-ouvertes.fr/inria-00489952/en/; http://hal.archives-ouvertes.fr/docs/00/48/99/52/PDF/cav09-full.pdf