References

  1. Synthesis Format Conversion Tool. Available at https://github.com/reactive-systems/syfco.
  2. Rajeev Alur & Salvatore La Torre (2004): Deterministic generators and games for LTL fragments. ACM Trans. Comput. Log. 5(1), pp. 1–25, doi:10.1145/963927.963928.
  3. Adrian Balint, Daniel Diepold, Daniel Gall, Simon Gerber, Gregor Kapler & Robert Retz (2011): EDACC - An Advanced Platform for the Experiment Design, Administration and Analysis of Empirical Algorithms. In: LION 5. Selected Papers, LNCS 6683. Springer, pp. 586–599, doi:10.1007/978-3-642-25566-3_46.
  4. Clark Barrett, Morgan Deters, Leonardo Mendonça de Moura, Albert Oliveras & Aaron Stump (2013): 6 Years of SMT-COMP. J. Autom. Reasoning 50(3), pp. 243–277, doi:10.1007/s10817-012-9246-5.
  5. Armin Biere: AIGER Format and Toolbox. Available at http://fmv.jku.at/aiger/.
  6. R. Bloem, B. Jobstmann, N. Piterman, A. Pnueli & Y. 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.
  7. R. Bloem, R. Könighofer & M. Seidl (2014): SAT-Based Synthesis Methods for Safety Specs. In: VMCAI, LNCS 8318. Springer, pp. 1–20, doi:10.1007/978-3-642-54013-4_1.
  8. Roderick Bloem, Krishnendu Chatterjee, Thomas A. Henzinger & Barbara Jobstmann (2009): Better Quality in Synthesis through Quantitative Objectives. In: CAV, LNCS 5643. Springer, pp. 140–156, doi:10.1007/978-3-642-02658-4_14.
  9. Roderick Bloem, Krishnendu Chatterjee, Swen Jacobs & Robert Könighofer (2015): Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information. In: TACAS, LNCS 9035. Springer, pp. 517–532, doi:10.1007/978-3-662-46681-0_50.
  10. Roderick Bloem, Uwe Egly, Patrick Klampfl, Robert Könighofer, Florian Lonsing & Martina Seidl (2016): Satisfiability-Based Methods for Reactive Synthesis from Safety Specifications. CoRR abs/1604.06204. Available at http://arxiv.org/abs/1604.06204.
  11. Romain Brenguier, Guillermo A. Pérez, Jean-François Raskin & Ocan Sankur (2014): AbsSynthe: abstract synthesis from succinct safety specifications. In: SYNT, EPTCS 157, pp. 100–116, doi:10.4204/EPTCS.157.11.
  12. Romain Brenguier, Guillermo A. Pérez, Jean-François Raskin & Ocan Sankur (2016): Compositional Algorithms for Succinct Safety Games. In: SYNT, EPTCS 202, pp. 98–111, doi:10.4204/EPTCS.202.7.
  13. 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.
  14. Gianpiero Cabodi, Carmelo Loiacono, Marco Palena, Paolo Pasini, Denis Patti, Stefano Quer, Danilo Vendraminetto, Armin Biere, Keijo Heljanko & Jason Baumgartner (2016): Hardware Model Checking Competition 2014: An Analysis and Comparison of Solvers and Benchmarks. Journal on Satisfiability, Boolean Modeling and Computation 9, pp. 135–172.
  15. Pavol Cerný, Krishnendu Chatterjee, Thomas A. Henzinger, Arjun Radhakrishna & Rohit Singh (2011): Quantitative Synthesis for Concurrent Programs. In: CAV, Lecture Notes in Computer Science 6806. Springer, pp. 243–259, doi:10.1007/978-3-642-22110-1_20.
  16. Pavol Cerný & Thomas A. Henzinger (2011): From boolean to quantitative synthesis. In: EMSOFT. ACM, pp. 149–154, doi:10.1145/2038642.2038666.
  17. Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann & Rohit Singh (2011): QUASY: Quantitative Synthesis Tool. In: TACAS, Lecture Notes in Computer Science 6605. Springer, pp. 267–271, doi:10.1007/978-3-642-19835-9_24.
  18. Yushan Chen, Xu Chu Ding, Alin Stefanescu & Calin Belta (2012): Formal Approach to the Deployment of Distributed Robotic Teams. IEEE Transactions on Robotics 28(1), pp. 158–171, doi:10.1109/TRO.2011.2163434.
  19. Ting-Wei Chiang & Jie-Hong R. Jiang (2015): Property-Directed Synthesis of Reactive Systems from Safety Specifications. In: ICCAD. IEEE, pp. 794–801, doi:10.1109/ICCAD.2015.7372652.
  20. Sandeep Chinchali, Scott C. Livingston, Ufuk Topcu, Joel W. Burdick & Richard M. Murray (2012): Towards formal synthesis of reactive controllers for dexterous robotic manipulation. In: ICRA. IEEE, pp. 5183–5189, doi:10.1109/ICRA.2012.6225257.
  21. Alonzo Church (1962): Logic, arithmetic and automata. In: Proceedings of the international congress of mathematicians, pp. 23–35.
  22. Niklas Eén, Alexander Legg, Nina Narodytska & Leonid Ryzhyk (2015): SAT-Based Strategy Extraction in Reachability Games. In: AAAI. AAAI Press, pp. 3738–3745. Available at http://www.aaai.org/ocs/index.php/AAAI/AAAI15/paper/view/9683.
  23. Rüdiger Ehlers (2011): Unbeast: Symbolic Bounded Synthesis. In: TACAS, LNCS 6605. Springer, pp. 272–275, doi:10.1007/978-3-642-19835-9_25.
  24. Rüdiger Ehlers (2012): Symbolic bounded synthesis. Formal Methods in System Design 40(2), pp. 232–262, doi:10.1007/s10703-011-0137-x.
  25. 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.
  26. Emmanuel Filiot: Acacia+. Available at http://lit2.ulb.ac.be/acaciaplus/.
  27. 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.
  28. 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.
  29. Bernd Finkbeiner (2016): Synthesis of Reactive Systems. In: Dependable Software Systems Engineering, NATO Science for Peace and Security Series - D: Information and Communication Security 45. IOS Press, pp. 72–98, doi:10.3233/978-1-61499-627-9-72.
  30. Bernd Finkbeiner & Swen Jacobs (2012): Lazy Synthesis. In: VMCAI, LNCS 7148. Springer, pp. 219–234, doi:10.1007/978-3-642-27940-9_15.
  31. Bernd Finkbeiner & Sven Schewe (2013): Bounded synthesis. STTT 15(5-6), pp. 519–539, doi:10.1007/s10009-012-0228-z.
  32. Swen Jacobs (2014): Extended AIGER Format for Synthesis. CoRR abs/1405.5793. Available at http://arxiv.org/abs/1405.5793.
  33. 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..
  34. 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, this volume of EPTCS. Open Publishing Association.
  35. 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 (2016): The Second Reactive Synthesis Competition (SYNTCOMP 2015). In: SYNT, EPTCS 202. Open Publishing Association, pp. 27–57, doi:10.4204/EPTCS.202.4.
  36. Swen Jacobs, Felix Klein & Sebastian Schirmer (2016): A High-Level LTL Synthesis Format: TLSF v1.1. In: SYNT, this volume of EPTCS. Open Publishing Association.
  37. Matti Järvisalo, Daniel Le Berre, Olivier Roussel & Laurent Simon (2012): The International SAT Solver Competitions. AI Magazine 33(1).
  38. Barbara Jobstmann & Roderick Bloem (2006): Optimizations for LTL Synthesis. In: FMCAD. IEEE Computer Society, pp. 117–124, doi:10.1109/FMCAD.2006.22.
  39. Ayrat Khalimov (2016): Specification Format for Reactive Synthesis Problems. In: SYNT, EPTCS 202, pp. 112–119, doi:10.4204/EPTCS.202.8.
  40. Hadas Kress-Gazit, Georgios E. Fainekos & George J. Pappas (2009): Temporal-Logic-Based Reactive Mission and Motion Planning. IEEE Transactions on Robotics 25(6), pp. 1370–1381, doi:10.1109/TRO.2009.2030225.
  41. Alexander Legg, Nina Narodytska & Leonid Ryzhyk (2016): A SAT-Based Counterexample Guided Method for Unbounded Synthesis. In: CAV (2), LNCS 9780. Springer, pp. 364–382, doi:10.1007/978-3-319-41540-6_20.
  42. Jun Liu, Necmiye Ozay, Ufuk Topcu & Richard M. Murray (2013): Synthesis of Reactive Switching Protocols From Temporal Logic Specifications. IEEE Trans. Automat. Contr. 58(7), pp. 1771–1785, doi:10.1109/TAC.2013.2246095.
  43. P. Madhusudan & P. S. Thiagarajan (2001): Distributed Controller Synthesis for Local Specifications. In: ICALP, LNCS 2076. Springer, pp. 396–407, doi:10.1007/3-540-48224-5_33.
  44. P. Madhusudan & P. S. Thiagarajan (2002): A Decidable Class of Asynchronous Distributed Controllers. In: CONCUR, LNCS 2421. Springer, pp. 145–160, doi:10.1007/3-540-45694-5_11.
  45. 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.
  46. Nina Narodytska, Alexander Legg, Fahiem Bacchus, Leonid Ryzhyk & Adam Walker (2014): Solving Games without Controllable Predecessor. In: CAV, LNCS 8559. Springer, pp. 533–540, doi:10.1007/978-3-319-08867-9_35.
  47. A Pnueli, E Asarin, O Maler & J Sifakis (1998): Controller synthesis for timed automata. In: Proc. System Structure and Control. Elsevier.
  48. Amir Pnueli (1977): The Temporal Logic of Programs. In: FOCS. IEEE Computer Society, pp. 46–57, doi:10.1109/SFCS.1977.32.
  49. Amir Pnueli & Roni Rosner (1989): On the Synthesis of a Reactive Module. In: POPL. ACM Press, pp. 179–190, doi:10.1145/75277.75293.
  50. Amir Pnueli & Roni Rosner (1990): Distributed Reactive Systems Are Hard to Synthesize. In: Foundations of Computer Science (FOCS'90). IEEE Computer Society, pp. 746–757, doi:10.1109/FSCS.1990.89597.
  51. Michael O. Rabin (1972): Automata on Infinite Objects and Church's Problem. Amer. Math. Soc. 13.
  52. Leonid Ryzhyk, Adam Walker, John Keys, Alexander Legg, Arun Raghunath, Michael Stumm & Mona Vij (2014): User-Guided Device Driver Synthesis. In: OSDI. USENIX Association, pp. 661–676. Available at https://www.usenix.org/conference/osdi14/technical-sessions/presentation/ryzhyk.
  53. 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.
  54. Aaron Stump, Geoff Sutcliffe & Cesare Tinelli (2014): StarExec: A Cross-Community Infrastructure for Logic Solving. In: IJCAR, LNCS 8562. Springer, pp. 367–373, doi:10.1007/978-3-319-08587-6_28.
  55. Geoff Sutcliffe & Christian B. Suttner (2006): The state of CASC. AI Commun. 19(1), pp. 35–48.
  56. Leander Tentrup (2016): Solving QBF by Abstraction. CoRR abs/1604.06752. Available at http://arxiv.org/abs/1604.06752.
  57. Wolfgang Thomas (1995): On the Synthesis of Strategies in Infinite Games. In: STACS, pp. 1–13, doi:10.1007/3-540-59042-0_57.
  58. Adam Walker & Leonid Ryzhyk (2014): Predicate abstraction for reactive synthesis. In: FMCAD. IEEE, pp. 219–226, doi:10.1109/FMCAD.2014.6987617.
  59. Martin Zimmermann (2013): Optimal bounds in parametric LTL games. Theor. Comput. Sci. 493, pp. 30–45, doi:10.1016/j.tcs.2012.07.039.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org