Acacia+

Acacia+ is a tool for LTL realizability and synthesis, based on symbolic antichain techniques. Acacia+ is extended to synthesis from LTL specifications with secondary mean-payoff objectives. NEW! Acacia+ contains a new feature: the synthesis of the optimal strategy in a stochastic environment among a set of winning strategies in the worst-case.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 15 articles )

Showing results 1 to 15 of 15.
Sorted by year (citations)

  1. Luttenberger, Michael; Meyer, Philipp J.; Sickert, Salomon: Practical synthesis of reactive systems from LTL specifications via parity games (2020)
  2. Tabajara, Lucas M.; Vardi, Moshe Y.: LTLf synthesis under partial observability: from theory to practice (2020)
  3. Hecking-Harbusch, Jesko; Metzger, Niklas O.: Efficient trace encodings of bounded synthesis for asynchronous distributed systems (2019)
  4. Křetínský, Jan; Manta, Alexander; Meggendorfer, Tobias: Semantic labelling and learning for parity game solving in LTL synthesis (2019)
  5. Finkbeiner, Bernd; Gölz, Paul: Synthesis in distributed environments (2018)
  6. Hunter, Paul; Pérez, Guillermo A.; Raskin, Jean-François: Looking at mean payoff through foggy windows (2018)
  7. Majumdar, Rupak; Raskin, Jean-François: Symbolic model checking in non-Boolean domains (2018)
  8. Torfah, Hazem; Zimmermann, Martin: The complexity of counting models of linear-time temporal logic (2018)
  9. Bohy, Aaron; Bruyère, Véronique; Raskin, Jean-François; Bertrand, Nathalie: Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes (2017)
  10. Faymonville, Peter; Finkbeiner, Bernd; Rabe, Markus N.; Tentrup, Leander: Encodings of bounded synthesis (2017)
  11. Tomita, Takashi; Ueno, Atsushi; Shimakawa, Masaya; Hagihara, Shigeki; Yonezaki, Naoki: Safraless LTL synthesis considering maximal realizability (2017)
  12. Tentrup, Leander: Non-prenex QBF solving using abstraction (2016)
  13. Tentrup, Leander; Weinert, Alexander; Zimmermann, Martin: Approximating optimal bounds in prompt-LTL realizability in doubly-exponential time (2016)
  14. Bulychev, Peter; David, Alexandre; Larsen, Kim G.; Li, Guangyuan: Efficient controller synthesis for a fragment of (\mathrmMTL_0,\infty) (2014)
  15. Bohy, Aaron; Bruyère, Véronique; Filiot, Emmanuel; Jin, Naiyong; Raskin, Jean-François: Acacia+, a tool for LTL synthesis (2012) ioport