Skip to main content
Top
Published in: Acta Informatica 1-2/2020

04-10-2019 | Original Article

A symbolic algorithm for lazy synthesis of eager strategies

Authors: Swen Jacobs, Mouhammad Sakr

Published in: Acta Informatica | Issue 1-2/2020

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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 classes of crafted benchmarks, the benchmark set of the Reactive Synthesis Competition (SYNTCOMP) 2017, as well as a set of randomly generated benchmarks. 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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Footnotes
1
This part is the light-weight backward search: unlike UPRE in the standard backward algorithm, preimage does not contain any quantifier alternation.
 
2
This is the only place where our algorithm uses image, and it is only included to keep the definitions and correctness argument simple - the algorithm also works if the model checker omits this last image computation step, see Sect. 5.
 
3
It may be a subsequence due to the merging of error levels from different iterations of the main loop.
 
Literature
2.
go back to reference Bloem, R., Könighofer, R., Seidl, M.: SAT-based synthesis methods for safety specs. In: VMCAI, LNCS, vol. 8318, pp. 1–20. Springer, Berlin (2014) Bloem, R., Könighofer, R., Seidl, M.: SAT-based synthesis methods for safety specs. In: VMCAI, LNCS, vol. 8318, pp. 1–20. Springer, Berlin (2014)
5.
go back to reference Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: CONCUR, LNCS, vol. 3653, pp. 66–80. Springer, Berlin (2005) Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: CONCUR, LNCS, vol. 3653, pp. 66–80. Springer, Berlin (2005)
6.
go back to reference Church, A.: Applications of recursive arithmetic to the problem of circuit synthesis. Summaries of the Summer Institute of Symbolic Logic I, pp. 3–50 (1957) Church, A.: Applications of recursive arithmetic to the problem of circuit synthesis. Summaries of the Summer Institute of Symbolic Logic I, pp. 3–50 (1957)
7.
go back to reference Clarke, J.B.E., Long, D.: Representing circuits more efficiently in symbolic model checking. In: 28th ACM/IEEE Design Automation Conference, pp. 403–407 (1991) Clarke, J.B.E., Long, D.: Representing circuits more efficiently in symbolic model checking. In: 28th ACM/IEEE Design Automation Conference, pp. 403–407 (1991)
8.
16.
go back to reference Jacobs, S., Basset, N., Bloem, R., Brenguier, R., Colange, M., Faymonville, P., Finkbeiner, B., Khalimov, A., Klein, F., Michaud, T., Pérez, G.A., Raskin, J., Sankur, O., Tentrup, L.: The 4th reactive synthesis competition (SYNTCOMP 2017): Benchmarks, participants & results. In: SYNT@CAV, EPTCS, vol. 260, pp. 116–143 (2017). https://doi.org/10.4204/EPTCS.260.10 CrossRef Jacobs, S., Basset, N., Bloem, R., Brenguier, R., Colange, M., Faymonville, P., Finkbeiner, B., Khalimov, A., Klein, F., Michaud, T., Pérez, G.A., Raskin, J., Sankur, O., Tentrup, L.: The 4th reactive synthesis competition (SYNTCOMP 2017): Benchmarks, participants & results. In: SYNT@CAV, EPTCS, vol. 260, pp. 116–143 (2017). https://​doi.​org/​10.​4204/​EPTCS.​260.​10 CrossRef
19.
go back to reference Kropf, T.: Introduction to Formal Hardware Verification. Springer, Berlin (2013)MATH Kropf, T.: Introduction to Formal Hardware Verification. Springer, Berlin (2013)MATH
27.
go back to reference Somenzi, F.: CUDD: CU decision diagram package, release 2.4.0. University of Colorado at Boulder (2009) Somenzi, F.: CUDD: CU decision diagram package, release 2.4.0. University of Colorado at Boulder (2009)
28.
go back to reference Touati, H.J., Savoj, H., Lin, B., Brayton, R.K., Sangiovanni-Vincentelli, A.: Implicit state enumeration of finite state machines using bdd’s. In: Computer-Aided Design, 1990. ICCAD-90. 1990 IEEE International Conference on Digest of Technical Papers, pp. 130–133. IEEE (1990) Touati, H.J., Savoj, H., Lin, B., Brayton, R.K., Sangiovanni-Vincentelli, A.: Implicit state enumeration of finite state machines using bdd’s. In: Computer-Aided Design, 1990. ICCAD-90. 1990 IEEE International Conference on Digest of Technical Papers, pp. 130–133. IEEE (1990)
Metadata
Title
A symbolic algorithm for lazy synthesis of eager strategies
Authors
Swen Jacobs
Mouhammad Sakr
Publication date
04-10-2019
Publisher
Springer Berlin Heidelberg
Published in
Acta Informatica / Issue 1-2/2020
Print ISSN: 0001-5903
Electronic ISSN: 1432-0525
DOI
https://doi.org/10.1007/s00236-019-00344-8

Other articles of this Issue 1-2/2020

Acta Informatica 1-2/2020 Go to the issue

Premium Partner