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
Acta Informatica
Erschienen in: Acta Informatica 3-4/2014

01.06.2014 | Original Article

Synthesizing robust systems

verfasst von: Roderick Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas A. Henzinger, Georg Hofferek, Barbara Jobstmann, Bettina Könighofer, Robert Könighofer

Erschienen in: Acta Informatica | Ausgabe 3-4/2014

Einloggen

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

search-config
loading …

Abstract

Systems should not only be correct but also robust in the sense that they behave reasonably in unexpected situations. This article addresses synthesis of robust reactive systems from temporal specifications. Existing methods allow arbitrary behavior if assumptions in the specification are violated. To overcome this, we define two robustness notions, combine them, and show how to enforce them in synthesis. The first notion applies to safety properties: If safety assumptions are violated temporarily, we require that the system recovers to normal operation with as few errors as possible. The second notion requires that, if liveness assumptions are violated, as many guarantees as possible should be fulfilled nevertheless. We present a synthesis procedure achieving this for the important class of GR(1) specifications, and establish complexity bounds. We also present an implementation of a special case of robustness, and show experimental results.
Vorheriger Artikel Efficient controller synthesis for a fragment of
Nächster Artikel Distributed synthesis for regular and contextfree specifications

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

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
Fußnoten
1
We assume that illegal signal valuations are “skipped”, i.e., the DBWs remain in the same state. The question in which state to continue after an error will be addressed in Sect. 5.1.1.
 
2
Note that the converse definition is more common. We use this definition as it allows for a smoother presentation of \(k\)-robustness.
 
3
We use LTL here, instead of DBWs, for space reasons. Building the corresponding DBWs is trivial.
 
4
While this is intuitively clear, refer to the proof of Lemma 14 in [13] for a formal argument.
 
5
A DBW encodes a liveness property if it is complete but not all states are accepting. A DBW encodes a safety property if all states are accepting but the transition function is incomplete. A DBW which features both can easily be split.
 
6
The reason is that conjunctions of Büchi conditions can easily be turned into Streett objectives, as will be shown later.
 
7
Cf. Definition 8.
 
Literatur
1.
2.
Alur, R., Kanade, A., Weiss, G.: Ranking automata and games for prioritized requirements. In: Gupta and Malik [32], pp. 240–253
3.
Anderson, T., Knight, J.C.: A framework for software fault tolerance in real-time systems. IEEE Trans. Softw. Eng. 9(3), 355–364 (1983)CrossRefMathSciNet
4.
Arora, A., Gouda, M.G.: Closure and convergence: a foundation of fault-tolerant computing. IEEE Trans. Softw. Eng. 19(11), 1015–1027 (1993)CrossRef
5.
Attie, P.C., Arora, A., Emerson, A.E.: Synthesis of fault-tolerant concurrent programs. ACM Trans. Program. Lang. Syst. 26(1), 125–185 (2004)CrossRef
6.
Avizienis, A., Laprie, J.-C., Randell, B., Landwehr, C.E.: Basic concepts and taxonomy of dependable and secure computing. IEEE Trans. Dependable Secur. Comput. 1(1), 11–33 (2004)CrossRef
7.
Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T.A., Jobstmann, B.: Robustness in the presence of liveness. In: Touili et al. (eds) [49], pp. 410–424
8.
Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Bouajjani and Maler [14], pp. 140–156
9.
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: Touili et al. [49], pp. 425–429
10.
Bloem, R., Galler, S.J., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Interactive presentation: automatic hardware synthesis from specifications: a case study. In: Lauwereins, R., Madsen, J. (eds.) 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., Gamauf, H.-J., Hofferek, G., Könighofer, B., Könighofer, R.: Synthesizing robust systems with RATSY. In: Peled, D., Schewe, S. (eds.) SYNT, Volume 84 of EPTCS, pp. 47–53 (2012)
13.
Bloem, R., Greimel, K., Henzinger, T.A., Jobstmann, B.: Synthesizing robust systems. In: FMCAD, pp. 85–92. IEEE (2009)
14.
Bouajjani, A., Maler, O. (eds): Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26–July 2, 2009. In: Proceedings, Volume 5643 of Lecture Notes in Computer Science. Springer, Berlin (2009)
15.
Chatterjee, K., Doyen, L. (2010) Energy parity games. In: Abramsky, S., Gavoille, C., Kirchner, C., Friedhelm Meyer auf der Heide, Spirakis, P.G. (eds) ICALP (2), Volume 6199 of Lecture Notes in Computer Science, pp. 599–610. Springer, Berlin
16.
Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Environment assumptions for synthesis. In: van Breugel, F., Chechik, M. (eds.) CONCUR, Volume 5201 of Lecture Notes in Computer Science, pp. 147–161. Springer, Berlin (2008)
17.
Chatterjee, K., Henzinger, T.A., Jurdzinski, M.: Mean-payoff parity games. In: LICS, pp. 178–187. IEEE Computer Society (2005)
18.
Chaudhuri, S., Gulwani, S., Lublinerman, R.: Continuity and robustness of programs. Commun. ACM 55(8), 107–115 (2012)CrossRef
19.
Cheng, C.-H., Rueß, H., Knoll, A., Buckl, C.: Synthesis of fault-tolerant embedded systems using games: from theory to practice. In: Jhala, R., Schmidt, D.A. (eds.) VMCAI, Volume 6538 of Lecture Notes in Computer Science, pp. 118–133. Springer, Berlin (2011)
20.
Church, A.: Logic, arithmetic, and automata. In: Proceedings of the International Congress of Mathematicians (Stockholm, 1962), pp. 23–35. Institut Mittag-Leffler, Djursholm (1963)
21.
Cury, J.E.R., Krogh, B.H.: Robustness of supervisors for discrete-event systems. Autom. Control IEEE Trans. 44(2), 376–379 (1999)CrossRefMATHMathSciNet
22.
Dijkstra, E.W.: Self-stabilizing systems in spite of distributed control. Commun. ACM 17(11), 643–644 (1974)CrossRefMATH
23.
Doyen, L., Henzinger, T.A., Legay, A., Nickovic, D.: Robustness of sequential circuits. In: Gomes, L., Khomenko, V., Fernandes, J.M. (eds.) ACSD, pp. 77–84. IEEE Computer Society (2010)
24.
D’Souza, D., Gopinathan, M.: Conflict-tolerant features. In: Gupta and Malik [32], pp. 227–239
25.
Ebnenasir, A., Kulkarni, S.S., Arora, A.: Ftsyn: a framework for automatic synthesis of fault-tolerance. STTT 10(5), 455–471 (2008)CrossRef
26.
Eisner, C.: Using symbolic model checking to verify the railway stations of hoorn-kersenboogerd and heerhugowaard. In: Pierre, L., Kropf, Th (eds.) CHARME, volume 1703 of Lecture Notes in Computer Science, pp. 97–109. Springer, Berlin (1999)
27.
Faella, M.: Games you cannot win. In: Workshop on Games and Automata for Synthesis and Validation (2007)
28.
Fey, G., Drechsler, R.: A basis for formal robustness checking. In: ISQED, pp. 784–789. IEEE Computer Society (2008)
29.
Filiot, E., Jin, N., Raskin, J.-F.: An antichain algorithm for LTL realizability. In: Bouajjani and Maler [14], pp. 263–277
30.
Gärtner, F.C.: Fundamentals of fault-tolerant distributed computing in asynchronous environments. ACM Comput. Surv. 31(1), 1–26 (1999)CrossRef
31.
Girault, A., Rutten, É.: Automating the addition of fault tolerance with discrete controller synthesis. Formal Methods Syst. Des. 35(2), 190–225 (2009)CrossRefMATH
32.
Gupta, A., Malik, S. (eds): Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7–14, 2008. Proceedings, Volume 5123 of Lecture Notes in Computer Science. Springer, Berlin (2008)
33.
Gurevich, Y., Harrington, L.: Trees, automata, and games. In: STOC’82, pp. 60–65. ACM Press (1982)
34.
Henzinger, T.: Two challenges in embedded systems design: predictability and robustness. Philos. Trans. R. Soc. 366, 3727–3736 (2008)
35.
Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: FMCAD, pp. 117–124. IEEE Computer Society (2006)
36.
Jobstmann, B., Galler, S.J., Weiglhofer, M., Bloem, R.: Anzu: a tool for property synthesis. In: Damm, W., Hermanns, H. (eds.) CAV, Volume 4590 of Lecture Notes in Computer Science, pp. 258–262. Springer, Berlin (2007)
37.
Kulkarni, S.S., Ebnenasir, A.: Complexity issues in automated synthesis of failsafe fault-tolerance. IEEE Trans. Dependable Secur. Comput. 2(3), 201–215 (2005)CrossRef
38.
Majumdar, R., Render, E., Tabuada, P.: Robust discrete synthesis against unspecified disturbances. In: Caccamo, M., Frazzoli, E., Grosu, R. (eds.) HSCC, pp. 211–220. ACM, UK (2011)
39.
Morgenstern, A., Schneider, K.: Exploiting the temporal logic hierarchy and the non-confluence property for efficient LTL synthesis. In: Montanari, A., Napoli, M., Parente, M. (eds) GANDALF, Vvolume 25 of EPTCS, pp. 89–102 (2010)
40.
Navarro, G.: A guided tour to approximate string matching. ACM Comput. Surv. 33(1), 31–88 (2001)CrossRef
41.
Piterman, N., Pnueli, A.: Faster solutions of rabin and streett games. In: LICS, pp. 275–284. IEEE Computer Society (2006)
42.
Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive(1) designs. In: Emerson, A.E., Namjoshi, K.S. (eds.) VMCAI, Volume 3855 of Lecture Notes in Computer Science, pp. 364–380. Springer, Berlin (2006)
43.
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179–190. ACM Press (1989)
44.
Ramadge, P.J.G., Wonham, W.M.: The control of discrete event systems. Proc. IEEE 77(1), 81–98 (1989)CrossRef
45.
Rinard, M.C.: Acceptability-oriented computing. In: Crocker, R., Steele Jr, G.L. (eds.) OOPSLA Companion, pp. 221–239. ACM (2003)
46.
Schewe, S., Finkbeiner, B.: Bounded synthesis. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA, Volume 4762 of Lecture Notes in Computer Science, pp. 474–488. Springer, Berlin (2007)
47.
Shivakumar, P., Kistler, M., Keckler, S.W., Burger, D., Alvisi, L.: Modeling the effect of technology trends on the soft error rate of combinational logic. In: DSN, pp. 389–398. IEEE Computer Society (2002)
48.
Thomas, W.: Languages, automata, and logic. In: Handbook of Formal Languages, Volume 3, Chapter 7, pp. 389–455. Springer, Berlin (1997)
49.
Touili, T., Cook, B., Jackson, P. (eds.): Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15–19, 2010. In: Proceedings, Volume 6174 of Lecture Notes in Computer Science. Springer, Berlin (2010)
50.
Metadaten
Titel
Synthesizing robust systems
verfasst von
Roderick Bloem
Krishnendu Chatterjee
Karin Greimel
Thomas A. Henzinger
Georg Hofferek
Barbara Jobstmann
Bettina Könighofer
Robert Könighofer
Publikationsdatum
01.06.2014
Verlag
Springer Berlin Heidelberg
Erschienen in
Acta Informatica / Ausgabe 3-4/2014
Print ISSN: 0001-5903
Elektronische ISSN: 1432-0525
DOI
https://doi.org/10.1007/s00236-013-0191-5

Weitere Artikel der Ausgabe 3-4/2014

Acta Informatica 3-4/2014 Zur Ausgabe

Original Article

Efficient controller synthesis for a fragment of

Editorial

Editorial: special issue on synthesis

Original Article

Distributed synthesis for regular and contextfree specifications

Original Article

Strategy synthesis for multi-dimensional quantitative objectives

Premium Partner

    Bildnachweise