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. © 2012 Springer-Verlag.
CITATION STYLE
Bohy, A., Bruyère, V., Filiot, E., Jin, N., & Raskin, J. F. (2012). Acacia+, a tool for LTL synthesis. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7358 LNCS, pp. 652–657). https://doi.org/10.1007/978-3-642-31424-7_45
Mendeley helps you to discover research relevant for your work.