References

  1. S. B. Akers (1978): Binary Decision Diagrams. IEEE Trans. Comput. 27(6), pp. 509–516, doi:10.1109/TC.1978.1675141.
  2. Rajeev Alur, Salar Moarref & Ufuk Topcu (2013): Counter-Strategy Guided Refinement of GR(1) Temporal Logic Specifications, doi:10.1109/FMCAD.2013.6679387.
  3. Rajeev Alur, Salar Moarref & Ufuk Topcu (2015): Pattern-Based Refinement of Assume-Guarantee Specifications in Reactive Synthesis. In: Christel Baier & Cesare Tinelli: Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 501–516, doi:10.1007/978-3-662-46681-0_49.
  4. Ilan Beer, Shoham Ben-David, Cindy Eisner & Yoav Rodeh (2001): Efficient Detection of Vacuity in Temporal Model Checking. Formal Methods in System Design 18(2), pp. 141–163, doi:10.1023/A:1008779610539.
  5. Shoham Ben-David, Fady Copty, Dana Fisman & Sitvanit Ruah (2015): Vacuity in practice: temporal antecedent failure. Formal Methods in System Design 46(1), pp. 81–104, doi:10.1007/s10703-014-0221-0.
  6. Roderick Bloem, Hana Chockler, Masoud Ebrahimi & Ofer Strichman (2017): Synthesizing Non-Vacuous Systems. In: Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings, pp. 55–72, doi:10.1007/978-3-319-52234-0_4.
  7. Roderick Bloem, Stefan Galler, Nir Piterman, Amir Pnueli & Martin Weiglhofer (2007): Automatic hardware synthesis from specifications: A case study. In: In Design, Automation and Test in Europe (DATE, doi:10.1109/DATE.2007.364456.
  8. Roderick Bloem, Hans-Jürgen Gamauf, Georg Hofferek, Bettina Könighofer & Robert Könighofer (2012): Synthesizing Robust Systems with RATSY 84, doi:10.4204/EPTCS.84.4.
  9. Aaron Bohy, Véronique Bruyère, Emmanuel Filiot, Naiyong Jin & Jean-François Raskin (2012): Acacia+, a Tool for LTL Synthesis. In: P. Madhusudan & Sanjit A. Seshia: Computer Aided Verification. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 652–657, doi:10.1007/978-3-642-31424-7_45.
  10. Tomáš Brázdil, Krishnendu Chatterjee, Martin Chmelík, Andreas Fellner & Jan Křetínský (2015): Counterexample Explanation by Learning Small Strategies in Markov Decision Processes, pp. 158–177. Springer International Publishing, Cham, doi:10.1007/978-3-319-21690-4_10.
  11. Tomas Brazdil, Krishnendu Chatterjee, Jan Kretinsky & Viktor Toman (2018): Strategy Representation by Decision Trees in Reactive Synthesis. In: TACAS. Springer, doi:10.1016/S0304-3975(98)00009-7.
  12. J. Richard Buchi & Lawrence H. Landweber (1990): Solving Sequential Conditions by Finite-State Strategies, pp. 525–541. Springer New York, New York, NY, doi:10.1007/978-1-4613-8928-6_29.
  13. Krishnendu Chatterjee & Thomas A. Henzinger (2007): Assume-Guarantee Synthesis. In: Orna Grumberg & Michael Huth: Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 261–275, doi:10.1007/978-3-540-71209-1_21.
  14. Krishnendu Chatterjee, Thomas A. Henzinger & Barbara Jobstmann (2008): Environment Assumptions for Synthesis. In: Franck van Breugel & Marsha Chechik: CONCUR 2008 - Concurrency Theory. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 147–161, doi:10.1007/978-3-540-85361-9_14.
  15. Krishnendu Chatterjee, Thomas A. Henzinger, Barbara Jobstmann & Arjun Radhakrishna (2010): Gist: A Solver for Probabilistic Games. In: Tayssir Touili, Byron Cook & Paul Jackson: Computer Aided Verification. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 665–669, doi:10.1007/978-3-642-14295-6_57.
  16. Chih-Hong Cheng, Yassine Hamza & Harald Ruess (2016): Structural Synthesis for GXW Specifications. In: International Conference on Computer Aided Verification. Springer, pp. 95–117, doi:10.1007/978-3-319-89960-2_21.
  17. Chih-Hong Cheng, Chung-Hao Huang, Harald Ruess & Stefan Stattelmann (2014): G4LTL-ST: Automatic generation of PLC programs. In: International Conference on Computer Aided Verification. Springer, pp. 541–549, doi:10.1007/978-3-319-08867-9_36.
  18. Chih-Hong Cheng, Edward A Lee & Harald Ruess (2017): autoCode4: Structural Controller Synthesis. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, pp. 398–404, doi:10.1007/978-3-662-54577-5_23.
  19. Hana Chockler, Joseph Y. Halpern & Orna Kupferman (2008): What Causes a System to Satisfy a Specification?. ACM Trans. Comput. Logic 9(3), pp. 20:1–20:26, doi:10.1145/1352582.1352588.
  20. Hana Chockler, Orna Kupferman & Moshe Y. Vardi (2003): Coverage Metrics for Formal Verification. In: Daniel Geist & Enrico Tronci: Correct Hardware Design and Verification Methods. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 111–125, doi:10.1007/978-3-540-39724-3_11.
  21. A. Cimatti, M. Roveri, V. Schuppan & A. Tchaltsev (2008): Diagnostic Information for Realizability. In: Francesco Logozzo, Doron A. Peled & Lenore D. Zuck: Verification, Model Checking, and Abstract Interpretation. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 52–67, doi:10.1007/978-3-540-78163-9_9.
  22. Rüdiger Ehlers (2011): Unbeast: Symbolic Bounded Synthesis. In: Parosh Aziz Abdulla & K. Rustan M. Leino: Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 272–275, doi:10.1007/978-3-642-19835-9_25.
  23. Rüdiger Ehlers & Vasumathi Raman (2016): Slugs: Extensible GR(1) Synthesis. In: Swarat Chaudhuri & Azadeh Farzan: Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II, Lecture Notes in Computer Science 9780. Springer, pp. 333–339, doi:10.1007/978-3-319-41540-6_18.
  24. Peter Faymonville, Bernd Finkbeiner & Leander Tentrup (2017): BoSy: An Experimentation Framework for Bounded Synthesis. In: Proceedings of CAV, LNCS 10427. Springer, pp. 325–332, doi:10.1007/978-3-319-63390-9_17.
  25. Bernd Finkbeiner & Felix Klein (2016): Bounded Cycle Synthesis. Lecture Notes in Computer Science 9779. Springer Berlin Heidelberg, doi:10.1007/978-3-319-41528-4.
  26. Bernd Finkbeiner & Felix Klein (2017): Reactive Synthesis: Towards Output-Sensitive Algorithms. In: Alexander Pretschner, Doron Peled & Thomas Hutzelmann: Dependable Software Systems Engineering, NATO Science for Peace and Security Series, D: Information and Communication Security 50. IOS Press, pp. 25–43, doi:10.3233/978-1-61499-810-5-25.
  27. Bernd Finkbeiner & Sven Schewe (2013): Bounded synthesis. International Journal on Software Tools for Technology Transfer 15(5-6), pp. 519–539, doi:10.1007/s10009-012-0228-z.
  28. Bernd Finkbeiner & Leander Tentrup (2015): Detecting Unrealizability of Distributed Fault-tolerant Systems. Logical Methods in Computer Science 11(3), doi:10.2168/LMCS-11(3:12)2015.
  29. Bernd Finkbeiner & Hazem Torfah (2016): Synthesizing Skeletons for Reactive Systems, pp. 271–286. Springer International Publishing, Cham, doi:10.1007/978-3-319-46520-3_18.
  30. M. Fujita, Y. Matsunaga & T. Kakuda (1991): On variable ordering of binary decision diagrams for the application of multi-level logic synthesis. In: Proceedings of the European Conference on Design Automation., pp. 50–54, doi:10.1109/EDAC.1991.206358.
  31. Yuichi Fukaya & Noriaki Yoshiura (2015): Extracting Environmental Constraints in Reactive System Specifications. In: Osvaldo Gervasi, Beniamino Murgante, Sanjay Misra, Marina L. Gavrilova, Ana Maria Alves Coutinho Rocha, Carmelo Torre, David Taniar & Bernady O. Apduhan: Computational Science and Its Applications – ICCSA 2015. Springer International Publishing, Cham, pp. 671–685, doi:10.1007/978-3-319-21410-8_51.
  32. Yatin Hoskote, Timothy Kam, Pei-Hsin Ho & Xudong Zhao (1999): Coverage Estimation for Symbolic Model Checking. In: Proceedings of the 36th Annual ACM/IEEE Design Automation Conference, DAC '99. ACM, New York, NY, USA, pp. 300–305, doi:10.1145/309847.309936.
  33. Swen Jacobs, Nicolas Basset, Roderick Bloem, Romain Brenguier, Maximilien Colange, Peter Faymonville, Bernd Finkbeiner, Ayrat Khalimov, Felix Klein, Thibaud Michaud, Guillermo A. Perez, Jean-Francois Raskin, Ocan Sankur & Leander Tentrup (2017): The 4th Reactive Synthesis Competition (SYNTCOMP 2017): Benchmarks, Participants and Results. In: SYNT 2017, EPTCS 260, pp. 116–143, doi:10.4204/EPTCS.260.10.
  34. Barbara Jobstmann, Stefan Galler, Martin Weiglhofer & Roderick Bloem (2007): Anzu: A Tool for Property Synthesis. In: Werner Damm & Holger Hermanns: Computer Aided Verification. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 258–262, doi:10.1007/978-3-540-73368-3_29.
  35. Robert Könighofer, Georg Hofferek & Roderick Bloem (2011): Debugging Unrealizable Specifications with Model-Based Diagnosis, pp. 29–45. Springer Berlin Heidelberg, Berlin, Heidelberg, doi:10.1007/978-3-642-19583-9_8.
  36. R. K√∂nighofer, G. Hofferek & R. Bloem (2009): Debugging formal specifications using simple counterstrategies. In: 2009 Formal Methods in Computer-Aided Design, pp. 152–159, doi:10.1109/FMCAD.2009.5351127.
  37. Wolfgang Lenders & Christel Baier (2005): Genetic Algorithms for the Variable Ordering Problem of Binary Decision Diagrams. In: Alden H. Wright, Michael D. Vose, Kenneth A. De Jong & Lothar M. Schmitt: Foundations of Genetic Algorithms. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 1–20, doi:10.1007/11513575_1.
  38. W. Li, L. Dworkin & S. A. Seshia (2011): Mining assumptions for synthesis. In: Ninth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMPCODE2011), pp. 43–50, doi:10.1109/MEMCOD.2011.5970509.
  39. Constantine Lignos, Vasumathi Raman, Cameron Finucane, Mitchell P. Marcus & Hadas Kress-Gazit (2015): Provably correct reactive control from natural language. Auton. Robots 38(1), pp. 89–105, doi:10.1007/s10514-014-9418-8.
  40. P. Nilsson & N. Ozay (2014): Incremental synthesis of switching protocols via abstraction refinement. In: 53rd IEEE Conference on Decision and Control, pp. 6246–6253, doi:10.1109/CDC.2014.7040368.
  41. Hans-Jörg Peter & Robert Mattmüller (2009): Component-based Abstraction Refinement for Timed Controller Synthesis. In: Theodore Baker: Proceedings of the 30th IEEE Real-Time Systems Symposium (RTSS 2009), December 1 - December 4, 2009, Washington, D.C., USA. IEEE Computer Society, Los Alamitos, CA, USA, pp. 364–374, doi:10.1109/RTSS.2009.14.
  42. A. Pnueli & R. Rosner (1990): Distributed Reactive Systems Are Hard to Synthesize. In: Proceedings of the 31st Annual Symposium on Foundations of Computer Science, SFCS '90. IEEE Computer Society, Washington, DC, USA, pp. 746–757 vol.2, doi:10.1109/FSCS.1990.89597.
  43. V. Raman & H. Kress-Gazit (2013): Explaining Impossible High-Level Robot Behaviors. IEEE Transactions on Robotics 29(1), pp. 94–104, doi:10.1109/TRO.2012.2214558.
  44. G. Reissig, A. Weber & M. Rungger (2017): Feedback Refinement Relations for the Synthesis of Symbolic Controllers. IEEE Transactions on Automatic Control 62(4), pp. 1781–1796, doi:10.1109/TAC.2016.2593947.
  45. Viktor Schuppan (2012): Towards a notion of unsatisfiable and unrealizable cores for LTL. Science of Computer Programming 77(7), pp. 908 Р939, doi:10.1016/j.scico.2010.11.004. Available at http://www.sciencedirect.com/science/article/pii/S0167642310002030. (1) FOCLASA’09 (2) FSEN’09.
  46. Kai Weng Wong, Rüdiger Ehlers & Hadas Kress-Gazit (2014): Correct High-level Robot Behavior in Environments with Unexpected Events. In: Robotics: Science and Systems X, University of California, Berkeley, USA, July 12-16, 2014, doi:10.15607/RSS.2014.X.012. Available at http://www.roboticsproceedings.org/rss10/p12.html.
  47. Kai Weng Wong & H. Kress-Gazit (2015): Let's talk: Autonomous conflict resolution for robots carrying out individual high-level tasks in a shared workspace. In: 2015 IEEE International Conference on Robotics and Automation (ICRA), pp. 339–345, doi:10.1109/ICRA.2015.7139021.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org