Acacia+, a Tool for LTL Synthesis
| Autor: | Véronique Bruyère, Emmanuel Filiot, Jean-François Raskin, Aaron Bohy, Naiyong Jin |
|---|---|
| Přispěvatelé: | Université de Mons (UMons), Institute of Computer Science [Mons], University of Mons [Belgium] (UMONS), Département d'Informatique [Bruxelles] (ULB), Faculté des Sciences [Bruxelles] (ULB), Université libre de Bruxelles (ULB)-Université libre de Bruxelles (ULB), Université libre de Bruxelles (ULB), P. Madhusudan and Sanjit A. Seshia |
| Jazyk: | angličtina |
| Rok vydání: | 2012 |
| Předmět: |
Reduction (complexity)
Theoretical computer science Computer science TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Realizability Reactive synthesis 0202 electrical engineering electronic engineering information engineering 020207 software engineering 020201 artificial intelligence & image processing [INFO]Computer Science [cs] 02 engineering and technology Algorithm ComputingMilieux_MISCELLANEOUS |
| Zdroj: | Computer Aided Verification (CAV) Computer Aided Verification (CAV), 2012, Unknown, Unknown Region. pp.652-657, ⟨10.1007/978-3-642-31424-7_45⟩ Lecture Notes in Computer Science Computer Aided Verification ISBN: 9783642314230 CAV |
| DOI: | 10.1007/978-3-642-31424-7_45⟩ |
| Popis: | We present Acacia+, a tool for solving the LTL realizability and synthesis problems. We use recent approaches that reduce these problems to safety games, and can be solved efficiently by symbolic incremental algorithms based on antichains. The reduction to safety games offers very interesting properties in practice: the construction of compact solutions (when they exist) and a compositional approach for large conjunctions of LTL formulas. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|