Skip to main content
Top

2018 | OriginalPaper | Chapter

Bounded Synthesis of Reactive Programs

Authors : Carsten Gerstacker, Felix Klein, Bernd Finkbeiner

Published in: Automated Technology for Verification and Analysis

Publisher: Springer International Publishing

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

search-config
loading …

Abstract

Most algorithms for the synthesis of reactive systems focus on the construction of finite-state machines rather than actual programs. This often leads to badly structured, unreadable code. In this paper, we present a bounded synthesis approach that automatically constructs, from a given specification in linear-time temporal logic (LTL), a program in Madhusudan’s simple imperative language for reactive programs. We develop and compare two principal approaches for the reduction of the synthesis problem to a Boolean constraint satisfaction problem. The first reduction is based on a generalization of bounded synthesis to two-way alternating automata, the second reduction is based on a direct encoding of the program syntax in the constraint system. We report on preliminary experience with a prototype implementation, which indicates that the direct encoding outperforms the automata approach.

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 "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!

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!

Literature
1.
go back to reference Church, A.: Application of recursive arithmetic to the problem of circuit synthesis. J. Symb. Log. 28(4), 289–290 (1963)CrossRef Church, A.: Application of recursive arithmetic to the problem of circuit synthesis. J. Symb. Log. 28(4), 289–290 (1963)CrossRef
5.
go back to reference Faymonville, P., Finkbeiner, B., Tentrup, L.: BoSy: an experimentation framework for bounded synthesis. [20] 325–332 Faymonville, P., Finkbeiner, B., Tentrup, L.: BoSy: an experimentation framework for bounded synthesis. [20] 325–332
6.
go back to reference Bloem, R., Galler, S.J., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M., et al.: Interactive presentation: automatic hardware synthesis from specifications: a case study. In: Lauwereins, R., Madsen, J. (eds.) DATE, pp. 1188–1193. Nice, France, EDA Consortium, San Jose, CA, USA (2007) Bloem, R., Galler, S.J., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M., et al.: Interactive presentation: automatic hardware synthesis from specifications: a case study. In: Lauwereins, R., Madsen, J. (eds.) DATE, pp. 1188–1193. Nice, France, EDA Consortium, San Jose, CA, USA (2007)
7.
go back to reference Finkbeiner, B., Schewe, S.: Bounded synthesis. STTT 15(5–6), 519–539 (2013)CrossRef Finkbeiner, B., Schewe, S.: Bounded synthesis. STTT 15(5–6), 519–539 (2013)CrossRef
10.
go back to reference Alur, R., et al.: Syntax-guided synthesis. In: FMCAD, pp. 1–8. Portland, OR, USA, IEEE (2013) Alur, R., et al.: Syntax-guided synthesis. In: FMCAD, pp. 1–8. Portland, OR, USA, IEEE (2013)
11.
go back to reference Gulwani, S.: Automating string processing in spreadsheets using input-output examples. In: Ball, T., Sagiv, M. (eds.) POPL, pp. 317–330. Austin, TX, USA, ACM (2011) Gulwani, S.: Automating string processing in spreadsheets using input-output examples. In: Ball, T., Sagiv, M. (eds.) POPL, pp. 317–330. Austin, TX, USA, ACM (2011)
12.
go back to reference Osera, P., Zdancewic, S.: Type-and-example-directed program synthesis. In: Grove, D., Blackburn, S. (eds.) PLDI, pp. 619–630. Portland, OR, USA, ACM (2015) Osera, P., Zdancewic, S.: Type-and-example-directed program synthesis. In: Grove, D., Blackburn, S. (eds.) PLDI, pp. 619–630. Portland, OR, USA, ACM (2015)
13.
14.
go back to reference Vechev, M.T., Yahav, E., Yorsh, G.: Abstraction-guided synthesis of synchronization. STTT 15(5–6), 413–431 (2013)CrossRef Vechev, M.T., Yahav, E., Yorsh, G.: Abstraction-guided synthesis of synchronization. STTT 15(5–6), 413–431 (2013)CrossRef
15.
go back to reference Madhusudan, P.: Synthesizing reactive programs. In: Bezem, M., (ed.) CSL, Bergen, Norway. Volume 12 of LIPIcs, pp. 428–442. Schloss Dagstuhl (2011) Madhusudan, P.: Synthesizing reactive programs. In: Bezem, M., (ed.) CSL, Bergen, Norway. Volume 12 of LIPIcs, pp. 428–442. Schloss Dagstuhl (2011)
17.
go back to reference Gerstacker, C.: Bounded Synthesis of Reactive Programs, Bachelor’s Thesis (2017) Gerstacker, C.: Bounded Synthesis of Reactive Programs, Bachelor’s Thesis (2017)
18.
go back to reference Gerstacker, C., Klein, F., Finkbeiner, B.: Bounded synthesis of reactive programs. CoRR 1807.09047 (2018) Gerstacker, C., Klein, F., Finkbeiner, B.: Bounded synthesis of reactive programs. CoRR 1807.09047 (2018)
19.
go back to reference Khalimov, A., Bloem, R.: Bounded Synthesis for Streett, Rabin, and CTL\(^{*}\). [20] 333–352 Khalimov, A., Bloem, R.: Bounded Synthesis for Streett, Rabin, and CTL\(^{*}\). [20] 333–352
Metadata
Title
Bounded Synthesis of Reactive Programs
Authors
Carsten Gerstacker
Felix Klein
Bernd Finkbeiner
Copyright Year
2018
DOI
https://doi.org/10.1007/978-3-030-01090-4_26

Premium Partner