An Antichain Algorithm for LTL Realizability - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2009

An Antichain Algorithm for LTL Realizability

Résumé

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.
Fichier principal
Vignette du fichier
cav09-full.pdf (204.64 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00489952 , version 1 (07-06-2010)

Identifiants

Citer

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⟩

Collections

TDS-MACS
64 Consultations
365 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More