An Antichain Algorithm for LTL Realizability

Emmanuel Filiot 1, * Naiyong Jin 1 Raskin Jean-François 1
* Auteur correspondant
1 ULB - Université Libre de Bruxelles [Bruxelles]
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.
Type de document :
Communication dans un congrès
Springer Berlin / Heidelberg. Computer Aided Verification, Jun 2009, Grenoble, France. Volume 5643, pp.263-277, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-02658-4_22〉
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/inria-00489952
Contributeur : Emmanuel Filiot <>
Soumis le : lundi 7 juin 2010 - 14:40:26
Dernière modification le : lundi 21 mars 2016 - 17:45:21
Document(s) archivé(s) le : vendredi 17 septembre 2010 - 13:05:27

Fichier

cav09-full.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

TDS-MACS

Citation

Emmanuel Filiot, Naiyong Jin, Raskin Jean-François. An Antichain Algorithm for LTL Realizability. Springer Berlin / Heidelberg. Computer Aided Verification, Jun 2009, Grenoble, France. Volume 5643, pp.263-277, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-02658-4_22〉. 〈inria-00489952〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

43

Téléchargements de fichiers

135

Contact


archive-ouverte@inria.fr