Skip to Main content Skip to Navigation
Conference papers

An Antichain Algorithm for LTL Realizability

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.
Complete list of metadata

Cited literature [20 references]  Display  Hide  Download
Contributor : Emmanuel Filiot Connect 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


Files produced by the author(s)




Emmanuel Filiot, Naiyong Jin, Raskin Jean-François. An Antichain Algorithm for LTL Realizability. Computer Aided Verification, Jun 2009, Grenoble, France. pp.263-277, ⟨10.1007/978-3-642-02658-4_22⟩. ⟨inria-00489952⟩



Record views


Files downloads