Abstract | ||
---|---|---|
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. |
Year | DOI | Venue |
---|---|---|
2012 | 10.1007/978-3-642-31424-7_45 | CAV |
Keywords | Field | DocType |
ltl realizability,ltl synthesis,symbolic incremental algorithm,recent approach,safety game,large conjunction,compositional approach,interesting property,compact solution,ltl formula,synthesis problem | Computer science,Algorithm,Theoretical computer science,Realizability | Conference |
Citations | PageRank | References |
55 | 1.90 | 16 |
Authors | ||
5 |
Name | Order | Citations | PageRank |
---|---|---|---|
Aaron Bohy | 1 | 74 | 3.21 |
Véronique Bruyère | 2 | 429 | 43.59 |
Emmanuel Filiot | 3 | 217 | 24.98 |
Naiyong Jin | 4 | 95 | 8.40 |
Jean-François Raskin | 5 | 1735 | 100.15 |