Advertisement

A Symbolic Algorithm for Lazy Synthesis of Eager Strategies

  • Swen Jacobs
  • Mouhammad SakrEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11138)

Abstract

We present an algorithm for solving two-player safety games that combines a mixed forward/backward search strategy with a symbolic representation of the state space. By combining forward and backward exploration, our algorithm can synthesize strategies that are eager in the sense that they try to prevent progress towards the error states as soon as possible, whereas standard backwards algorithms often produce permissive solutions that only react when absolutely necessary. We provide experimental results for two new sets of benchmarks, as well as the benchmark set of the Reactive Synthesis Competition (SYNTCOMP) 2017. The results show that our algorithm in many cases produces more eager strategies than a standard backwards algorithm, and solves a number of benchmarks that are intractable for existing tools. Finally, we observe a connection between our algorithm and a recently proposed algorithm for the synthesis of controllers that are robust against disturbances, pointing to possible future applications.

Notes

Acknowledgments

We thank Bernd Finkbeiner and Martin Zimmermann for fruitful discussions. This work was supported by the German Research Foundation (DFG) under the project ASDPS (JA 2357/2-1).

References

  1. 1.
    Church, A.: Applications of recursive arithmetic to the problem of circuit synthesis. Summ. Summer Inst. Symb. Logic I, 3–50 (1957)Google Scholar
  2. 2.
    Büchi, J., Landweber, L.: Solving sequential conditions by finite-state strategies. Trans. Am. Math. Soc. 138, 295–311 (1969)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179–190. ACM Press (1989)Google Scholar
  4. 4.
    Filiot, E., Jin, N., Raskin, J.F.: Antichains and compositional algorithms for LTL synthesis. Form. Methods Syst. Des. 39(3), 261–296 (2011)CrossRefGoogle Scholar
  5. 5.
    Ehlers, R.: Symbolic bounded synthesis. Form. Methods Syst. Des. 40(2), 232–262 (2012)CrossRefGoogle Scholar
  6. 6.
    Sohail, S., Somenzi, F.: Safety first: a two-stage algorithm for the synthesis of reactive systems. STTT 15(5–6), 433–454 (2013)CrossRefGoogle Scholar
  7. 7.
    Finkbeiner, B., Schewe, S.: Bounded synthesis. STTT 15(5–6), 519–539 (2013)CrossRefGoogle Scholar
  8. 8.
    Bloem, R., Könighofer, R., Seidl, M.: SAT-based synthesis methods for safety specs. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 1–20. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-642-54013-4_1CrossRefGoogle Scholar
  9. 9.
    Legg, A., Narodytska, N., Ryzhyk, L.: A SAT-based counterexample guided method for unbounded synthesis. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 364–382. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-41540-6_20CrossRefGoogle Scholar
  10. 10.
    Jacobs, S., et al.: The first reactive synthesis competition (SYNTCOMP 2014). STTT 19(3), 367–390 (2017)CrossRefGoogle Scholar
  11. 11.
    Dallal, E., Neider, D., Tabuada, P.: Synthesis of safety controllers robust to unmodeled intermittent disturbances. In: CDC, pp. 7425–7430. IEEE (2016)Google Scholar
  12. 12.
    Jacobs, S., et al.: The 4th reactive synthesis competition (SYNTCOMP 2017): benchmarks, participants & results. In: SYNT@CAV. Volume 260 of EPTCS, pp. 116–143. (2017)CrossRefGoogle Scholar
  13. 13.
    Liu, X., Smolka, S.A.: Simple linear-time algorithms for minimal fixed points. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 53–66. Springer, Heidelberg (1998).  https://doi.org/10.1007/BFb0055040CrossRefGoogle Scholar
  14. 14.
    Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 66–80. Springer, Heidelberg (2005).  https://doi.org/10.1007/11539452_9CrossRefGoogle Scholar
  15. 15.
    Finkbeiner, B., Jacobs, S.: Lazy synthesis. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 219–234. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-27940-9_15CrossRefGoogle Scholar
  16. 16.
    Kropf, T.: Introduction to Formal Hardware Verification. Springer Science & Business Media, Berlin (2013)zbMATHGoogle Scholar
  17. 17.
    Somenzi, F.: CUDD: CU decision diagram package, release 2.4.0. University of Colorado at Boulder (2009)Google Scholar
  18. 18.
    Neider, D., Weinert, A., Zimmermann, M.: Synthesizing optimally resilient controllers. In: CSL (2018, to appear)Google Scholar
  19. 19.
    Ehlers, R., Topcu, U.: Resilience to intermittent assumption violations in reactive synthesis. In: HSCC, pp. 203–212. ACM (2014)Google Scholar
  20. 20.
    Huang, C., Peled, D.A., Schewe, S., Wang, F.: A game-theoretic foundation for the maximum software resilience against dense errors. IEEE Trans. Softw. Eng. 42(7), 605–622 (2016)CrossRefGoogle Scholar
  21. 21.
    Raman, V., Donzé, A., Sadigh, D., Murray, R.M., Seshia, S.A.: Reactive synthesis from signal temporal logic specifications. In: HSCC, pp. 239–248. ACM (2015)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.CISPA and Saarland UniversitySaarbruckenGermany

Personalised recommendations