References

  1. Promela Manual Pages (Promela LTL). Available at http://spinroot.com/spin/Man/ltl.html.
  2. Synthesis Format Conversion Tool. Available at https://github.com/reactive-systems/syfco.
  3. ARM Ltd. (1999): AMBA specification (rev. 2). Available at http://www.arm.com.
  4. Roderick Bloem, Barbara Jobstmann, Nir Piterman, Amir Pnueli & Yaniv Sa'ar (2012): Synthesis of Reactive(1) Designs. J. Comput. Syst. Sci. 78(3), pp. 911–938, doi:10.1016/j.jcss.2011.08.007.
  5. J.R. Büchi & L.H. Landweber (1969): Solving sequential conditions by finite-state strategies. Trans. Amer. Math. Soc. 138, pp. 295–311, doi:10.2307/1994916.
  6. Alonzo Church (1962): Logic, arithmetic and automata. In: Proceedings of the international congress of mathematicians, pp. 23–35, doi:10.2307/2270398.
  7. Rüdiger Ehlers (2010): Unbeast - Symbolic Bounded Synthesis. Available at https://react.cs.uni-saarland.de/tools/unbeast.
  8. Rüdiger Ehlers (2011): Experimental Aspects of Synthesis. In: iWIGP, EPTCS 50, pp. 1–16, doi:10.4204/EPTCS.50.1.
  9. Rüdiger Ehlers (2012): Symbolic bounded synthesis. Formal Methods in System Design 40(2), pp. 232–262, doi:10.1007/s10703-011-0137-x.
  10. Rüdiger Ehlers & Vasumathi Raman (2016): Slugs: Extensible GR(1) Synthesis. In: CAV (2), Lecture Notes in Computer Science 9780. Springer, pp. 333–339, doi:10.1007/978-3-319-41540-6_18.
  11. Rüdiger Ehlers, Vasumathi Raman & Cameron Finucane (2013): slugs - SmalL bUt Complete GROne Synthesizer. Available at https://github.com/VerifiableRobotics/slugs.
  12. Cindy Eisner & Dana Fisman (2006): A Practical Introduction to PSL. Series on Integrated Circuits and Systems. Springer-Verlag, doi:10.1007/978-0-387-36123-9.
  13. Emmanuel Filiot, Naiyong Jin & Jean-François Raskin (2011): Antichains and compositional algorithms for LTL synthesis. Formal Methods in System Design 39(3), pp. 261–296, doi:10.1007/s10703-011-0115-3.
  14. Emmanuel Filiot, Naiyong Jin & Jean-François Raskin (2013): Exploiting structure in LTL synthesis. STTT 15(5-6), pp. 541–561, doi:10.1007/s10009-012-0222-5.
  15. Bernd Finkbeiner & Swen Jacobs (2012): Lazy Synthesis. In: VMCAI, LNCS 7148. Springer, pp. 219–234, doi:10.1007/978-3-642-27940-9_15.
  16. Bernd Finkbeiner & Sven Schewe (2013): Bounded synthesis. STTT 15(5-6), pp. 519–539, doi:10.1007/s10009-012-0228-z.
  17. Swen Jacobs (2014): Extended AIGER Format for Synthesis. CoRR abs/1405.5793. Available at http://arxiv.org/abs/1405.5793.
  18. Swen Jacobs & Roderick Bloem (2016): The Reactive Synthesis Competition: SYNTCOMP 2016 and Beyond. In: SYNT, THISVOLUME5.
  19. Swen Jacobs, Roderick Bloem, Romain Brenguier, Rüdiger Ehlers, Timotheus Hell, Robert Könighofer, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup & Adam Walker (2016): The First Reactive Synthesis Competition (SYNTCOMP 2014). STTT, doi:10.1007/s10009-016-0416-3. Published online first, journal issue to appear.
  20. Swen Jacobs, Roderick Bloem, Romain Brenguier, Ayrat Khalimov, Felix Klein, Robert Könighofer, Jens Kreber, Alexander Legg, Nina Narodytska, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup & Adam Walker (2016): The 3rd Reactive Synthesis Competition (SYNTCOMP 2016): Benchmarks, Participants & Results. In: SYNT, THISVOLUME13.
  21. Swen Jacobs, Roderick Bloem, Romain Brenguier, Robert Könighofer, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup & Adam Walker (2015): The Second Reactive Synthesis Competition (SYNTCOMP 2015). In: SYNT 2015, EPTCS 202, pp. 27–57, doi:10.4204/EPTCS.202.4.
  22. Swen Jacobs & Felix Klein (2016): A High-Level LTL Synthesis Format: TLSF v1.0. CoRR abs/1601.05228. Available at http://arxiv.org/abs/1601.05228.
  23. Barbara Jobstmann (2007): Applications and Optimizations for LTL Synthesis. Graz University of Technology.
  24. Uri Klein & Amir Pnueli (2010): Revisiting Synthesis of GR(1) Specifications. In: HVC 2010. Revised Selected Papers, LNCS 6504. Springer, pp. 161–181, doi:10.1007/978-3-642-19583-9_16.
  25. Andreas Morgenstern & Klaus Schneider (2011): A LTL Fragment for GR(1)-Synthesis. In: iWIGP, EPTCS 50, pp. 33–45, doi:10.4204/EPTCS.50.3.
  26. Amir Pnueli & Roni Rosner (1989): On the Synthesis of a Reactive Module. In: POPL. ACM Press, pp. 179–190, doi:10.1145/75277.75293.
  27. Michael O. Rabin (1969): Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc. 141, pp. 1–35, doi:10.1090/S0002-9947-1969-0246760-1.
  28. Sebastian Schirmer (2015): A Specification Format for Reactive Synthesis. Bachelor Thesis. Saarland University, Computer Science.
  29. Saqib Sohail & Fabio Somenzi (2013): Safety first: a two-stage algorithm for the synthesis of reactive systems. STTT 15(5-6), pp. 433–454, doi:10.1007/s10009-012-0224-3.
  30. Fabio Somenzi & Roderick Bloem (2000): Efficient Büchi Automata from LTL Formulae. In: CAV, LNCS 1855. Springer, pp. 248–263, doi:10.1007/10722167_21.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org