References

  1. Rajeev Alur, Salar Moarref & Ufuk Topcu (2013): Counter-strategy guided refinement of GR(1) temporal logic specifications. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013. IEEE, pp. 26–33. Available at http://dx.doi.org/10.1109/FMCAD.2013.6679387.
  2. Roderick Bloem, Swen Jacobs & Ayrat Khalimov (2014): Parameterized Synthesis Case Study: AMBA AHB. In: Krishnendu Chatterjee, Rüdiger Ehlers & Susmit Jha: Proceedings 3rd Workshop on Synthesis, SYNT 2014, Vienna, Austria, July 23-24, 2014., EPTCS 157, pp. 68–83. Available at http://dx.doi.org/10.4204/EPTCS.157.9.
  3. 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. Available at http://dx.doi.org/10.1016/j.jcss.2011.08.007.
  4. Nicolás D'Ippolito, Víctor A. Braberman, Nir Piterman & Sebastián Uchitel (2013): Synthesizing nonanomalous event-based controllers for liveness goals. ACM Trans. Softw. Eng. Methodol. 22(1), pp. 9. Available at http://doi.acm.org/10.1145/2430536.2430543.
  5. Matthew B. Dwyer, George S. Avrunin & James C. Corbett (1999): Patterns in Property Specifications for Finite-State Verification. In: ICSE. ACM, pp. 411–420. Available at http://doi.acm.org/10.1145/302405.302672.
  6. Rüdiger Ehlers & Ufuk Topcu (2014): Resilience to intermittent assumption violations in reactive synthesis. In: Martin Fränzle & John Lygeros: 17th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC'14, Berlin, Germany, April 15-17, 2014. ACM, pp. 203–212. Available at http://doi.acm.org/10.1145/2562059.2562128.
  7. Yashdeep Godhal, Krishnendu Chatterjee & Thomas A. Henzinger (2013): Synthesis of AMBA AHB from formal specification: a case study. STTT 15(5-6), pp. 585–601. Available at http://dx.doi.org/10.1007/s10009-011-0207-9.
  8. Uri Klein & Amir Pnueli (2010): Revisiting Synthesis of GR(1) Specifications. In: Sharon Barner, Ian G. Harris, Daniel Kroening & Orna Raz: Hardware and Software: Verification and Testing - 6th International Haifa Verification Conference, HVC 2010, Haifa, Israel, October 4-7, 2010. Revised Selected Papers, Lecture Notes in Computer Science 6504. Springer, pp. 161–181. Available at http://dx.doi.org/10.1007/978-3-642-19583-9_16.
  9. Robert Könighofer, Georg Hofferek & Roderick Bloem (2013): Debugging formal specifications: a practical approach using model-based diagnosis and counterstrategies. STTT 15(5-6), pp. 563–583. Available at http://dx.doi.org/10.1007/s10009-011-0221-y.
  10. Hadas Kress-Gazit, Georgios E. Fainekos & George J. Pappas (2007): Where's Waldo? Sensor-Based Temporal Logic Motion Planning. In: 2007 IEEE International Conference on Robotics and Automation, ICRA 2007, 10-14 April 2007, Roma, Italy. IEEE, pp. 3116–3121. Available at http://dx.doi.org/10.1109/ROBOT.2007.363946.
  11. Hadas Kress-Gazit, Georgios E. Fainekos & George J. Pappas (2009): Temporal-Logic-Based Reactive Mission and Motion Planning. IEEE Trans. Robotics 25(6), pp. 1370–1381. Available at http://dx.doi.org/10.1109/TRO.2009.2030225.
  12. Shahar Maoz & Jan Oliver Ringert (2015): GR(1) Synthesis for LTL Specification Patterns. In: ESEC/FSE. ACM, pp. 96–106. Available at http://dx.doi.org/10.1145/2786805.2786824. http://smlab.cs.tau.ac.il/syntech/patterns/.
  13. Shahar Maoz & Yaniv Sa'ar (2011): AspectLTL: an aspect language for LTL specifications. In: Paulo Borba & Shigeru Chiba: AOSD. ACM, pp. 19–30. Available at http://doi.acm.org/10.1145/1960275.1960280.
  14. Shahar Maoz & Yaniv Sa'ar (2012): Assume-Guarantee Scenarios: Semantics and Synthesis. In: MODELS, LNCS 7590. Springer, pp. 335–351. Available at http://dx.doi.org/10.1007/978-3-642-33666-9_22.
  15. Shahar Maoz & Yaniv Sa'ar (2013): Counter play-out: executing unrealizable scenario-based specifications. In: ICSE. IEEE / ACM, pp. 242–251. Available at http://dl.acm.org/citation.cfm?id=2486821.
  16. Shahar Maoz & Yaniv Sa'ar (2013): Two-Way Traceability and Conflict Debugging for AspectLTL Programs. T. Aspect-Oriented Software Development 10, pp. 39–72. Available at http://dx.doi.org/10.1007/978-3-642-36964-3_2.
  17. Nir Piterman, Amir Pnueli & Yaniv Sa'ar (2006): Synthesis of Reactive(1) Designs. In: VMCAI, LNCS 3855. Springer, pp. 364–380. Available at http://dx.doi.org/10.1007/11609773_24.
  18. Amir Pnueli & Roni Rosner (1989): On the Synthesis of a Reactive Module. In: POPL. ACM Press, pp. 179–190. Available at http://doi.acm.org/10.1145/75277.75293.
  19. Amir Pnueli, Yaniv Sa'ar & Lenore D. Zuck (2010): JTLV: A Framework for Developing Verification Algorithms. In: CAV, LNCS 6174. Springer, pp. 171–174. Available at http://dx.doi.org/10.1007/978-3-642-14295-6_18.
  20. Vasumathi Raman, Nir Piterman & Hadas Kress-Gazit (2013): Provably correct continuous control for high-level robot behaviors with actions of arbitrary execution durations. In: 2013 IEEE International Conference on Robotics and Automation, Karlsruhe, Germany, May 6-10, 2013. IEEE, pp. 4075–4081. Available at http://dx.doi.org/10.1109/ICRA.2013.6631152.
  21. Jan Oliver Ringert, Bernhard Rumpe & Andreas Wortmann (2014): Architecture and Behavior Modeling of Cyber-Physical Systems with MontiArcAutomaton. Aachener Informatik-Berichte, Software Engineering 20. Shaker Verlag.
  22. SYNTECH forklift website. http://smlab.cs.tau.ac.il/syntech/forklift/.
  23. SYNTECH GR(1) patterns website. http://smlab.cs.tau.ac.il/syntech/patterns/.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org