Skip to main content

2017 | OriginalPaper | Buchkapitel

Synthesis of Optimal Resilient Control Strategies

verfasst von : Christel Baier, Clemens Dubslaff, L’uboš Korenčiak, Antonín Kučera, Vojtěch Řehák

Erschienen in: Automated Technology for Verification and Analysis

Verlag: Springer International Publishing

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

search-config
loading …

Abstract

Repair mechanisms are important within resilient systems to maintain the system in an operational state after an error occurred. Usually, constraints on the repair mechanisms are imposed, e.g., concerning the time or resources required (such as energy consumption or other kinds of costs). For systems modeled by Markov decision processes (MDPs), we introduce the concept of resilient schedulers, which represent control strategies guaranteeing that these constraints are always met within some given probability. Assigning rewards to the operational states of the system, we then aim towards resilient schedulers which maximize the long-run average reward, i.e., the expected mean payoff. We present a pseudo-polynomial algorithm that decides whether a resilient scheduler exists and if so, yields an optimal resilient scheduler. We show also that already the decision problem asking whether there exists a resilient scheduler is PSPACE-hard.

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!

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!

Literatur
1.
Zurück zum Zitat Altman, E.: Constrained Markov Decision Processes. Chapman and Hall, Boca Raton (1999)MATH Altman, E.: Constrained Markov Decision Processes. Chapman and Hall, Boca Raton (1999)MATH
2.
Zurück zum Zitat Attoh-Okine, N.: Resilience Engineering: Models and Analysis. Resilience Engineering: Models and Analysis. Cambridge University Press, Cambridge (2016)CrossRef Attoh-Okine, N.: Resilience Engineering: Models and Analysis. Resilience Engineering: Models and Analysis. Cambridge University Press, Cambridge (2016)CrossRef
3.
Zurück zum Zitat Baier, C., Dubslaff, C., Klüppelholz, S., Leuschner, L.: Energy-utility analysis for resilient systems using probabilistic model checking. In: Ciardo, G., Kindler, E. (eds.) PETRI NETS 2014. LNCS, vol. 8489, pp. 20–39. Springer, Cham (2014). doi:10.1007/978-3-319-07734-5_2 CrossRef Baier, C., Dubslaff, C., Klüppelholz, S., Leuschner, L.: Energy-utility analysis for resilient systems using probabilistic model checking. In: Ciardo, G., Kindler, E. (eds.) PETRI NETS 2014. LNCS, vol. 8489, pp. 20–39. Springer, Cham (2014). doi:10.​1007/​978-3-319-07734-5_​2 CrossRef
4.
Zurück zum Zitat Baier, C., Dubslaff, C., Korenčiak, Ľ., Kučera, A., Řehák, V.: Synthesis of optimal resilient control strategies. CoRR, abs/1707.03223 (2017) Baier, C., Dubslaff, C., Korenčiak, Ľ., Kučera, A., Řehák, V.: Synthesis of optimal resilient control strategies. CoRR, abs/1707.03223 (2017)
5.
Zurück zum Zitat Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press (2008) Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press (2008)
6.
Zurück zum Zitat Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T.A., Hofferek, G., Jobstmann, B., Könighofer, B., Könighofer, R.: Synthesizing robust systems. Acta Inf. 51(3), 193–220 (2014)MathSciNetCrossRefMATH Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T.A., Hofferek, G., Jobstmann, B., Könighofer, B., Könighofer, R.: Synthesizing robust systems. Acta Inf. 51(3), 193–220 (2014)MathSciNetCrossRefMATH
7.
Zurück zum Zitat Brázdil, T., Brožek, V., Chatterjee, K., Forejt, V., Kučera, A.: Markov decision processes with multiple long-run average objectives. LMCS 10(1) (2014) Brázdil, T., Brožek, V., Chatterjee, K., Forejt, V., Kučera, A.: Markov decision processes with multiple long-run average objectives. LMCS 10(1) (2014)
8.
Zurück zum Zitat Camara, J., de Lemos, R.: Evaluation of resilience in self-adaptive systems using probabilistic model-checking. In: SEAMS, pp. 53–62 (2012) Camara, J., de Lemos, R.: Evaluation of resilience in self-adaptive systems using probabilistic model-checking. In: SEAMS, pp. 53–62 (2012)
9.
10.
Zurück zum Zitat Ehlers, R., Topcu, U.: Resilience to intermittent assumption violations in reactive synthesis. In: HSCC, pp. 203–212. ACM, New York (2014) Ehlers, R., Topcu, U.: Resilience to intermittent assumption violations in reactive synthesis. In: HSCC, pp. 203–212. ACM, New York (2014)
11.
Zurück zum Zitat Etessami, K., Kwiatkowska, M., Vardi, M.Y., Yannakakis, M.: Multi-objective model checking of Markov decision processes. LMCS 4(4) (2008) Etessami, K., Kwiatkowska, M., Vardi, M.Y., Yannakakis, M.: Multi-objective model checking of Markov decision processes. LMCS 4(4) (2008)
12.
Zurück zum Zitat Forejt, V., Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Quantitative multi-objective verification for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 112–127. Springer, Heidelberg (2011). doi:10.1007/978-3-642-19835-9_11 CrossRef Forejt, V., Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Quantitative multi-objective verification for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 112–127. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-19835-9_​11 CrossRef
13.
Zurück zum Zitat German, R.: Performance Analysis of Communication Systems with Non-Markovian Stochastic Petri Nets. Wiley, Hobokon (2000)MATH German, R.: Performance Analysis of Communication Systems with Non-Markovian Stochastic Petri Nets. Wiley, Hobokon (2000)MATH
14.
Zurück zum Zitat Girault, A., Rutten, É.: Automating the addition of fault tolerance with discrete controller synthesis. Form. Methods Syst. Des. 35(2), 190–225 (2009)CrossRefMATH Girault, A., Rutten, É.: Automating the addition of fault tolerance with discrete controller synthesis. Form. Methods Syst. Des. 35(2), 190–225 (2009)CrossRefMATH
15.
Zurück zum Zitat Haase, C., Kiefer, S.: The odds of staying on budget. In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 234–246. Springer, Heidelberg (2015). doi:10.1007/978-3-662-47666-6_19 CrossRef Haase, C., Kiefer, S.: The odds of staying on budget. In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 234–246. Springer, Heidelberg (2015). doi:10.​1007/​978-3-662-47666-6_​19 CrossRef
16.
Zurück zum Zitat Huang, C.H., Peled, D.A., Schewe, S., Wang, F.: A game-theoretic foundation for the maximum software resilience against dense errors. IEEE Trans. Software Eng. 42(7), 605–622 (2016)CrossRef Huang, C.H., Peled, D.A., Schewe, S., Wang, F.: A game-theoretic foundation for the maximum software resilience against dense errors. IEEE Trans. Software Eng. 42(7), 605–622 (2016)CrossRef
17.
Zurück zum Zitat Kallenberg, L.: Markov Decision Processes. Lect. Notes, University of Leiden (2011) Kallenberg, L.: Markov Decision Processes. Lect. Notes, University of Leiden (2011)
18.
Zurück zum Zitat Longo, F., Ghosh, R., Naik, V.K., Rindos, A.J., Trivedi, K.S.: An approach for resiliency quantification of large scale systems. SIGMETRICS 44(4), 37–48 (2017)CrossRef Longo, F., Ghosh, R., Naik, V.K., Rindos, A.J., Trivedi, K.S.: An approach for resiliency quantification of large scale systems. SIGMETRICS 44(4), 37–48 (2017)CrossRef
19.
Zurück zum Zitat Puterman, M.L.: Markov Decision Processes. Wiley (1994) Puterman, M.L.: Markov Decision Processes. Wiley (1994)
Metadaten
Titel
Synthesis of Optimal Resilient Control Strategies
verfasst von
Christel Baier
Clemens Dubslaff
L’uboš Korenčiak
Antonín Kučera
Vojtěch Řehák
Copyright-Jahr
2017
DOI
https://doi.org/10.1007/978-3-319-68167-2_27

Premium Partner