Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
International Journal on Software Tools for Technology Transfer
Erschienen in: International Journal on Software Tools for Technology Transfer 3/2017

09.04.2016 | Regular Paper

The first reactive synthesis competition (SYNTCOMP 2014)

verfasst von: Swen Jacobs, Roderick Bloem, Romain Brenguier, Rüdiger Ehlers, Timotheus Hell, Robert Könighofer, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup, Adam Walker

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 3/2017

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

We introduce the reactive synthesis competition (SYNTCOMP), a long-term effort intended to stimulate and guide advances in the design and application of synthesis procedures for reactive systems. The first iteration of SYNTCOMP is based on the controller synthesis problem for finite-state systems and safety specifications. We provide an overview of this problem and existing approaches to solve it, and report on the design and results of the first SYNTCOMP. This includes the definition of the benchmark format, the collection of benchmarks, the rules of the competition, and the five synthesis tools that participated. We present and analyze the results of the competition and draw conclusions on the state of the art. Finally, we give an outlook on future directions of SYNTCOMP.
Vorheriger Artikel Fully automated runtime enforcement of component-based systems with formal and sound recovery

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Fußnoten
1
See also: the Hardware Model Checking Competition, http://​fmv.​jku.​at/​hwmcc/​. Accessed February 2016.
 
2
For simplicity, we assume that https://static-content.springer.com/image/art%3A10.1007%2Fs10009-016-0416-3/MediaObjects/10009_2016_416_IEq21_HTML.gif is a latch. If https://static-content.springer.com/image/art%3A10.1007%2Fs10009-016-0416-3/MediaObjects/10009_2016_416_IEq22_HTML.gif is not a latch in the given monitor circuit, then it can be described as a formula \(f(L,X_u,X_c)\). In this case we can obtain a problem in the described form by extending the circuit with a new latch that takes \(f(L,X_u,X_c)\) as an input and provides output https://static-content.springer.com/image/art%3A10.1007%2Fs10009-016-0416-3/MediaObjects/10009_2016_416_IEq25_HTML.gif .
 
4
http://​fmv.​jku.​at/​aiger/​. Accessed February 2016.
 
5
http://​fmv.​jku.​at/​hwmcc/​. Accessed February 2016.
 
6
The reason for disallowing original AND-gates is that we want the controller to work only based on the state of the given circuit (i.e., values of latches), and the uncontrollable inputs. Original AND-gates can be duplicated in the controller if necessary.
 
7
Numbers regarding realizability are to the best of our knowledge. The realizability status has not been verified for all benchmark instances.
 
12
http://​fmv.​jku.​at/​aiger/​. Accessed February 2016.
 
16
We conjecture that this version is more challenging because it is based on a large LTL specification, which is translated to a single, very big Büchi automaton in the first step of the ltl2aig routine. This results in a circuit that is much more complex than the ones from Sect. 4.3.
 
18
In particular, non-trivial parallelization is difficult for BDD-based tools, since none of the existing parallel BDD packages supports all features needed for the optimizations mentioned in Sect. 2.3.
 
19
The quality ranking was devised for the second SYNTCOMP and was applied to the results of the first competition only after the presentation of results at SYNT and CAV 2014.
 
20
This rule only had to be used in one instance, where a benchmark was solved by only one tool, and was reported to be realizable although unrealizable was the expected outcome. In our analysis it turned out that the tool was correct, and the initial classification as unrealizable was wrong.
 
22
http://​fmv.​jku.​at/​aiger/​. Accessed February 2016.
 
25
Analysis of results and subsequent inspection of the source code by the tool author showed that due to a bug the parallel version did not work as intended, and instead used two threads with identical strategy. As can be seen in the results section, this lead to a decreased performance overall.
 
26
http://​termite2.​org. Accessed February 2016.
 
29
As mentioned in Sect. 6.1, AbsSynthe was supposed to compete in different configurations, but due to a miscommunication was always started in the same configuration. The results presented here for the relative ranking differ from those presented at CAV 2014 in that only one of the three identical configurations of AbsSynthe is counted in the sequential tracks.
 
30
This benchmark was found to be realizable by the tool, although it was classified as unrealizable by the benchmark authors. Our analysis confirmed it to be realizable.
 
31
Due to a bug, the parallel version of Realizer performed worse than the sequential version, as mentioned in Sect. 6.
 
Literatur
1.
Alur, R., Bodík, R., Dallal, E., Fisman, D., Garg, P., Juniwal, G., Kress-Gazit, H., Madhusudan, P., Martin, M.M.K., Raghothaman, M., Saha, S., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: Dependable Software Systems Engineering, NATO Science for Peace and Security Series, D: Information and Communication Security, vol. 40, pp. 1–25. IOS Press (2015)
2.
Alur, R., Madhusudan, P., Nam, W.: Symbolic computational techniques for solving games. STTT 7(2), 118–128 (2005)CrossRefMATH
3.
Aziz, A., Tasiran, S., Brayton, R.K.: BDD variable ordering for interacting finite state machines. In: DAC, pp. 283–288 (1994)
4.
Balint, A., Diepold, D., Gall, D., Gerber, S., Kapler, G., Retz, R.: EDACC - an advanced platform for the experiment design, administration and analysis of empirical algorithms. In: LION 5. Selected Papers, LNCS, vol. 6683, pp. 586–599. Springer, (2011)
5.
Barrett, C.W., de Moura, L.M., Stump, A.: Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005). J. Autom. Reason. 35(4), 373–390 (2005)CrossRefMATH
6.
Beyer, D.: Competition on software verification - (SV-COMP). In: TACAS, LNCS, vol. 7214, pp. 504–524. Springer (2012)
7.
Beyer, D., Löwe, S., Wendler, P.: Benchmarking and resource measurement. In: SPIN 2015, LNCS, vol. 9232, pp. 160–178. Springer (2015)
8.
Bloem, R., Cimatti, A., Greimel, K., Hofferek, G., Könighofer, R., Roveri, M., Schuppan, V., Seeber, R.: RATSY - A new requirements analysis tool with synthesis. In: CAV, LNCS, vol. 6174, pp. 425–429. Springer (2010)
9.
Bloem, R., Egly, U., Klampfl, P., Könighofer, R., Lonsing, F.: SAT-based methods for circuit synthesis. In: FMCAD’14, pp. 31–34. IEEE (2014)
10.
Bloem, R., Galler, S.J., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Automatic hardware synthesis from specifications: a case study. In: DATE, pp. 1188–1193. ACM (2007)
11.
Bloem, R., Galler, S.J., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Specify, compile, run: hardware from PSL. Electr. Notes Theor. Comput. Sci. 190(4), 3–16 (2007)CrossRef
12.
Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive(1) designs. J. Comput. Syst. Sci. 78(3), 911–938 (2012)MathSciNetCrossRefMATH
13.
Bloem, R., Könighofer, R., Seidl, M.: SAT-based synthesis methods for safety specs. In: VMCAI, LNCS, vol. 8318, pp. 1–20. Springer (2014)
14.
Bohy, A., Bruyère, V., Filiot, E., Jin, N., Raskin, J.-F.: Acacia+, a tool for LTL synthesis. In: CAV, LNCS, vol. 7358, pp. 652–657. Springer (2012)
15.
Bradley, A.R.: SAT-based model checking without unrolling. In: VMCAI, LNCS, vol. 6538, pp. 70–87. Springer (2011)
16.
Brayton, R.K., Hachtel, G.D., Sangiovanni-Vincentelli, A.L., Somenzi, F., Aziz, A., Cheng, S., Edwards, S.A., Khatri, S.P., Kukimoto, Y., Pardo, A., Qadeer, S., Ranjan, R.K., Sarwary, S., Shiple, T.R., Swamy, G., Villa, T.: VIS: a system for verification and synthesis. In: CAV, LNCS, vol. 1102, pp. 428–432. Springer (1996)
17.
Brayton, R.K., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: CAV, LNCS, vol. 6174, pp. 24–40. Springer (2010)
18.
Brenguier, R., Pérez, G.A., Raskin, J.-F., Sankur, O.: AbsSynthe: abstract synthesis from succinct safety specifications. In: SYNT, EPTCS, vol. 157, pp. 100–116. Open Publishing Association (2014)
19.
Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35(8), 677–691 (1986)CrossRefMATH
20.
Büchi, J., Landweber, L.: Solving sequential conditions by finite-state strategies. Trans. Am. Math. Soc. 138, 295–311 (1969)CrossRefMATH
21.
Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic model checking with partitioned transistion relations. In: VLSI, pp. 49–58 (1991)
22.
Chiang, T., Jiang. J.R.: Property-directed synthesis of reactive systems from safety specifications. In: ICCAD, pp. 794–801. ACM (2015)
23.
Church, A.: Logic, arithmetic and automata. In: Proceedings of the International Congress of Mathematicians, pp. 23–35 (1962)
24.
Coudert, O., Madre, J.C.: A unified framework for the formal verification of sequential circuits. In: ICCAD, pp. 126–129 (1990)
25.
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238–252. ACM (1977)
26.
de Alfaro, L., Roy, P.: Solving games via three-valued abstraction refinement. In: CONCUR, LNCS, vol. 4703, pp. 74–89. Springer (2007)
27.
Ehlers, R.: Experimental aspects of synthesis. In: iWIGP, EPTCS, vol. 50, pp. 1–16 (2011)
28.
Ehlers, R.: Unbeast: symbolic bounded synthesis. In: TACAS, LNCS, vol. 6605, pp. 272–275. Springer (2011)
29.
Ehlers, R.: Symbolic bounded synthesis. Formal Methods Syst. Des. 40(2), 232–262 (2012)CrossRefMATH
30.
Ehlers, R., Könighofer, R., Hofferek, G.: Symbolically synthesizing small circuits. In: FMCAD’12, pp. 91–100. IEEE (2012)
31.
Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2(3), 241–266 (1982)CrossRefMATH
32.
Filiot, E., Jin, N., Raskin, J.: Exploiting structure in LTL synthesis. STTT 15(5–6), 541–561 (2013)CrossRef
33.
Filiot, E., Jin, N., Raskin, J.-F.: Antichains and compositional algorithms for LTL synthesis. Formal Methods Syst. Des. 39(3), 261–296 (2011)CrossRefMATH
34.
Finkbeiner, B., Jacobs, S.: Lazy synthesis. In: VMCAI, LNCS, vol. 7148, pp. 219–234. Springer (2012)
35.
36.
Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: CAV, LNCS, vol. 1254, pp. 72–83. Springer (1997)
37.
Henzinger, T.A., Jhala, R., Majumdar, R.: Counterexample-guided control. In: ICALP, LNCS, vol. 2719, pp. 886–902, Springer (2003)
38.
Hong, Y., Beerel, P.A., Burch, J.R., McMillan, K.L.: Sibling-substitution-based BDD minimization using don’t cares. IEEE Trans. CAD of Integr. Circuits Syst. 19(1), 44–55 (2000)CrossRef
39.
40.
Jacobs, S., Bloem, R., Brenguier, R., Ehlers, R., Hell, T., Könighofer, R., Pérez, G.A., Raskin, J., Ryzhyk, L., Sankur, O., Seidl, M., Tentrup, L., Walker, A.: The first reactive synthesis competition (SYNTCOMP 2014). CoRR (2015). arXiv:​1506.​08726. Accessed Feb 2016
41.
Jacobs, S., Bloem, R., Brenguier, R., Könighofer, R., Pérez, G.A., Raskin, J.-F., Ryzhyk, L., Sankur, O., Seidl, M., Tentrup, L., Walker, A.: The second reactive synthesis competition (SYNTCOMP 2015). In: SYNT, EPTCS, vol. 202, pp. 27–57. Open Publishing Association (2016)
42.
43.
Järvisalo, M., Berre, D.L., Roussel, O., Simon, L.: The international SAT solver competitions. AI Mag 33(1), 89–94 (2012)
44.
Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: FMCAD, pp. 117–124. IEEE Computer Society (2006)
45.
Jobstmann, B., Galler, S.J., Weiglhofer, M., Bloem, R.: Anzu: A tool for property synthesis. In: CAV, LNCS, vol. 4590, pp. 258–262. Springer (2006)
46.
Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: FOCS, pp. 531–542. IEEE Computer Society (2005)
47.
Kurshan, R.P.: Automata-theoretic verification of coordinating processes. In: Analysis and Optimization of Systems: Discrete Event Systems, pp. 16–28. Springer (1994)
48.
Lecoutre, C., Roussel, O., van Dongen, M.R.C.: Promoting robust black-box solvers through competitions. Constraints 15(3), 317–326 (2010)CrossRefMATH
49.
Mishchenko, A., Chatterjee, S., Brayton, R.K.: Dag-aware AIG rewriting a fresh look at combinational logic synthesis. In: DAC, pp. 532–535. ACM (2006)
50.
Mishchenko, A., Chatterjee, S., Jiang, R., Brayton, R.: FRAIGs: A unifying representation for logic synthesis and verification. Technical report, EECS Department, U. C. Berkeley (2005)
51.
Morgenstern, A., Gesell, M., Schneider, K.: Solving games using incremental induction. In: IFM’13, LNCS 7940, pp. 177–191. Springer (2013)
52.
Niemetz, A., Preiner, M., Lonsing, F., Seidl, M., Biere, A.: Resolution-based certificate extraction for QBF. In: SAT’12, LNCS 7317, pp. 430–435. Springer (2012)
53.
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179–190. ACM Press (1989)
54.
Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Trans. Am. Math. Soc. 141, 1–35 (1969)MATH
55.
Ranjan, R.K., Aziz, A., Brayton, R.K., Plessier, B., Pixley, C.: Efficient bdd algorithms for fsm synthesis and verification. In: International Workshop on Logic Synthesis (1995)
56.
Roussel, O.: Controlling a solver execution with the runsolver tool. JSAT 7(4), 139–144 (2011)MathSciNetMATH
57.
Rudell, R.: Dynamic variable ordering for ordered binary decision diagrams. In: ICCAD, pp. 42–47. IEEE Computer Society (1993)
58.
Seidl, M., Könighofer, R.: Partial witnesses from preprocessed quantified boolean formulas. In: DATE’14, pp. 1–6. IEEE (2014)
59.
Sohail, S., Somenzi, F.: Safety first: a two-stage algorithm for the synthesis of reactive systems. STTT 15(5–6), 433–454 (2013)CrossRef
60.
Somenzi, F.: Binary decision diagrams. In: Calculational System Design, vol. 173, pp. 303. IOS Press (1999)
61.
Sutcliffe, G., Suttner, C.B.: Evaluating general purpose automated theorem proving systems. Artif. Intell. 131(1–2), 39–54 (2001)MathSciNetCrossRefMATH
62.
63.
Thomas, W.: On the synthesis of strategies in infinite games. In: STACS, pp. 1–13 (1995)
64.
van Dijk, T., Laarman, A., van de Pol, J.: Multi-core BDD operations for symbolic reachability. Electron. Notes Theor. Comput. Sci. 296, 127–143 (2013)CrossRef
65.
van Dijk, T., van de Pol, J.: Sylvan: Multi-core decision diagrams. In: TACAS 2015, LNCS, vol. 9035, pp. 677–691 Springer (2015)
Metadaten
Titel
The first reactive synthesis competition (SYNTCOMP 2014)
verfasst von
Swen Jacobs
Roderick Bloem
Romain Brenguier
Rüdiger Ehlers
Timotheus Hell
Robert Könighofer
Guillermo A. Pérez
Jean-François Raskin
Leonid Ryzhyk
Ocan Sankur
Martina Seidl
Leander Tentrup
Adam Walker
Publikationsdatum
09.04.2016
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 3/2017
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-016-0416-3

Weitere Artikel der Ausgabe 3/2017

International Journal on Software Tools for Technology Transfer 3/2017 Zur Ausgabe

Introduction

Model-based testing as a service

Regular Paper

Fully automated runtime enforcement of component-based systems with formal and sound recovery

MBTCloud

Practical experiences in the usage of MIDAS in the logistics domain

MBTCloud

Combining usage-based and model-based testing for service-oriented architectures in the industrial practice

MBTCloud

Automation and intelligent scheduling of distributed system functional testing

Premium Partner

    Bildnachweise