Skip to main content

2016 | OriginalPaper | Buchkapitel

Decision-Theoretic Monitoring of Cyber-Physical Systems

verfasst von : Andrey Yavolovsky, Miloš Žefran, A. Prasad Sistla

Erschienen in: Runtime Verification

Verlag: Springer International Publishing

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

search-config
loading …

Abstract

Runtime monitoring has been proposed as an alternative to formal verification for safety critical systems. This paper introduces a decision-theoretic view of runtime monitoring. We formulate the monitoring problem as a Partially Observable Markov Decision Process (POMDP). Furthermore, we adopt a Partially Observable Monte-Carlo Planning (POMCP) to compute an approximate optimal policy of the monitoring POMDP. We show how to construct the POMCP for the monitoring problem and demonstrate experimentally that it can be effectively applied even when some of the state-space variables are continuous, the case where many other POMDP solvers fail. Experimental results on a mobile robot system show the effectiveness of the proposed POMDP-monitor.

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!

Fußnoten
1
Since we are only considering discrete outputs, the probability function becomes a probability distribution in z.
 
Literatur
1.
Zurück zum Zitat Agate, R., Seward, D.: Autonomous safety decision-making in intelligent robotic systems in the uncertain environments. In: Annual Meeting of the North American Fuzzy Information Processing Society, NAFIPS 2008, pp. 1–6. IEEE (2008) Agate, R., Seward, D.: Autonomous safety decision-making in intelligent robotic systems in the uncertain environments. In: Annual Meeting of the North American Fuzzy Information Processing Society, NAFIPS 2008, pp. 1–6. IEEE (2008)
2.
Zurück zum Zitat Auer, P., Cesa-Bianchi, N., Fischer, P.: Finite-time analysis of the multiarmed bandit problem. Mach. Learn. 47(2–3), 235–256 (2002)CrossRefMATH Auer, P., Cesa-Bianchi, N., Fischer, P.: Finite-time analysis of the multiarmed bandit problem. Mach. Learn. 47(2–3), 235–256 (2002)CrossRefMATH
3.
Zurück zum Zitat Bai, H., Hsu, D., Lee, W.S., Ngo, V.A.: Monte Carlo value iteration for continuous-state POMDPs. In: Hsu, D., Isler, V., Latombe, J.-C., Lin, M.C. (eds.) Algorithmic Foundations of Robotics IX. Springer Tracts in Advanced Robotics, vol. 68, pp. 175–191. Springer, Heidelberg (2011). doi:10.1007/978-3-642-17452-0_11 CrossRef Bai, H., Hsu, D., Lee, W.S., Ngo, V.A.: Monte Carlo value iteration for continuous-state POMDPs. In: Hsu, D., Isler, V., Latombe, J.-C., Lin, M.C. (eds.) Algorithmic Foundations of Robotics IX. Springer Tracts in Advanced Robotics, vol. 68, pp. 175–191. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-17452-0_​11 CrossRef
4.
Zurück zum Zitat Blom, H., Bloem, E.: Particle filtering for stochastic hybrid systems. In: 43rd IEEE Conference on Decision and Control, CDC, vol. 3 (2004) Blom, H., Bloem, E.: Particle filtering for stochastic hybrid systems. In: 43rd IEEE Conference on Decision and Control, CDC, vol. 3 (2004)
5.
Zurück zum Zitat Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT press, Cambridge (1999) Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT press, Cambridge (1999)
6.
Zurück zum Zitat Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94–124 (1998)MathSciNetCrossRefMATH Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94–124 (1998)MathSciNetCrossRefMATH
7.
Zurück zum Zitat Hofbaur, M.W., Williams, B.C.: Mode estimation of probabilistic hybrid systems. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol. 2289, pp. 253–266. Springer, Heidelberg (2002). doi:10.1007/3-540-45873-5_21 CrossRef Hofbaur, M.W., Williams, B.C.: Mode estimation of probabilistic hybrid systems. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol. 2289, pp. 253–266. Springer, Heidelberg (2002). doi:10.​1007/​3-540-45873-5_​21 CrossRef
8.
Zurück zum Zitat Radu, V.: Application. In: Radu, V. (ed.) Stochastic Modeling of Thermal Fatigue Crack Growth. Applied Condition Monitoring, vol. 1, pp. 63–70. Springer, Switzerland (2015) Radu, V.: Application. In: Radu, V. (ed.) Stochastic Modeling of Thermal Fatigue Crack Growth. Applied Condition Monitoring, vol. 1, pp. 63–70. Springer, Switzerland (2015)
9.
Zurück zum Zitat Kanade, A., Alur, R., Ivančić, F., Ramesh, S., Sankaranarayanan, S., Shashidhar, K.C.: Generating and analyzing symbolic traces of simulink/stateflow models. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 430–445. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02658-4_33 CrossRef Kanade, A., Alur, R., Ivančić, F., Ramesh, S., Sankaranarayanan, S., Shashidhar, K.C.: Generating and analyzing symbolic traces of simulink/stateflow models. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 430–445. Springer, Heidelberg (2009). doi:10.​1007/​978-3-642-02658-4_​33 CrossRef
10.
Zurück zum Zitat Koutsoukos, X., Kurien, J., Zhao, F.: Estimation of distributed hybrid systems using particle filtering methods. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 298–313. Springer, Heidelberg (2003). doi:10.1007/3-540-36580-X_23 CrossRef Koutsoukos, X., Kurien, J., Zhao, F.: Estimation of distributed hybrid systems using particle filtering methods. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 298–313. Springer, Heidelberg (2003). doi:10.​1007/​3-540-36580-X_​23 CrossRef
11.
Zurück zum Zitat Kumar, R., Garg, V.: Control of stochastic discrete event systems modeled by probabilistic languages. IEEE Trans. Autom. Control 46(4), 593–606 (2001)MathSciNetCrossRefMATH Kumar, R., Garg, V.: Control of stochastic discrete event systems modeled by probabilistic languages. IEEE Trans. Autom. Control 46(4), 593–606 (2001)MathSciNetCrossRefMATH
12.
Zurück zum Zitat Lerner, U., Moses, B., Scott, M., McIlraith, S., Koller, D.: Monitoring a complex physical system using a hybrid dynamic bayes net. In: Proceedings of the 18th Annual Conference on Uncertainty in AI (UAI), pp. 301–310 (2002) Lerner, U., Moses, B., Scott, M., McIlraith, S., Koller, D.: Monitoring a complex physical system using a hybrid dynamic bayes net. In: Proceedings of the 18th Annual Conference on Uncertainty in AI (UAI), pp. 301–310 (2002)
13.
Zurück zum Zitat Pantelic, V., Postma, S., Lawford, M.: Probabilistic supervisory control of probabilistic discrete event systems. IEEE Trans. Autom. Control 54(8), 2013–2018 (2009)MathSciNetCrossRef Pantelic, V., Postma, S., Lawford, M.: Probabilistic supervisory control of probabilistic discrete event systems. IEEE Trans. Autom. Control 54(8), 2013–2018 (2009)MathSciNetCrossRef
14.
15.
Zurück zum Zitat Tabuada, P.: Verification and Control of Hybrid Systems: A Symbolic Approach. Springer Science & Business Media, New York (2009) Tabuada, P.: Verification and Control of Hybrid Systems: A Symbolic Approach. Springer Science & Business Media, New York (2009)
16.
Zurück zum Zitat Quigley, M., Conley, K., Gerkey, B., Faust, J., Foote, T., Leibs, J., Wheeler, R., Ng, A.Y.: ROS: an open-source Robot Operating System. In: ICRA Workshop on Open Source Software 3 (2009) Quigley, M., Conley, K., Gerkey, B., Faust, J., Foote, T., Leibs, J., Wheeler, R., Ng, A.Y.: ROS: an open-source Robot Operating System. In: ICRA Workshop on Open Source Software 3 (2009)
17.
Zurück zum Zitat Russell, S., Norvig, P., Intelligence, A.: A Modern Approach. Prentice Hall, Englewood (2009) Russell, S., Norvig, P., Intelligence, A.: A Modern Approach. Prentice Hall, Englewood (2009)
18.
Zurück zum Zitat Seward, D., Pace, C., Agate, R.: Safe and effective navigation of autonomous robots in hazardous environments. Auton. Robot. 22(3), 223–242 (2007)CrossRef Seward, D., Pace, C., Agate, R.: Safe and effective navigation of autonomous robots in hazardous environments. Auton. Robot. 22(3), 223–242 (2007)CrossRef
19.
Zurück zum Zitat Silver, D., Veness, J.: Monte-Carlo planning in large POMDPs. In: Advances in Neural Information Processing Systems, pp. 2164–2172 (2010) Silver, D., Veness, J.: Monte-Carlo planning in large POMDPs. In: Advances in Neural Information Processing Systems, pp. 2164–2172 (2010)
20.
Zurück zum Zitat Sistla, A.P., Žefran, M., Feng, Y.: Runtime monitoring of stochastic cyber-physical systems with hybrid state. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 276–293. Springer, Heidelberg (2012). doi:10.1007/978-3-642-29860-8_21 CrossRef Sistla, A.P., Žefran, M., Feng, Y.: Runtime monitoring of stochastic cyber-physical systems with hybrid state. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 276–293. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-29860-8_​21 CrossRef
21.
Zurück zum Zitat Sistla, A.P., Žefran, M., Feng, Y.: Monitorability of stochastic dynamical systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 720–736. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_58 CrossRef Sistla, A.P., Žefran, M., Feng, Y.: Monitorability of stochastic dynamical systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 720–736. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-22110-1_​58 CrossRef
22.
Zurück zum Zitat Sistla, A.P., Žefran, M., Feng, Y., Ben, Y.: Timely monitoring of partially observable stochastic systems. In: Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, pp. 61–70. ACM (2014) Sistla, A.P., Žefran, M., Feng, Y., Ben, Y.: Timely monitoring of partially observable stochastic systems. In: Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, pp. 61–70. ACM (2014)
23.
Zurück zum Zitat Stoller, S.D., Bartocci, E., Seyster, J., Grosu, R., Havelund, K., Smolka, S.A., Zadok, E.: Runtime verification with state estimation. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 193–207. Springer, Heidelberg (2012). doi:10.1007/978-3-642-29860-8_15 CrossRef Stoller, S.D., Bartocci, E., Seyster, J., Grosu, R., Havelund, K., Smolka, S.A., Zadok, E.: Runtime verification with state estimation. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 193–207. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-29860-8_​15 CrossRef
24.
Zurück zum Zitat Verma, V., Gordon, G., Simmons, R., Thrun, S.: Real-time fault diagnosis. IEEE Robot. Autom. Mag. 11(2), 56–66 (2004)CrossRef Verma, V., Gordon, G., Simmons, R., Thrun, S.: Real-time fault diagnosis. IEEE Robot. Autom. Mag. 11(2), 56–66 (2004)CrossRef
25.
Zurück zum Zitat Yoo, T., Lafortune, S.: Polynomial-time verification of diagnosability of partially observed discrete-event systems. IEEE Trans. Autom. Control 47(9), 1491–1495 (2002)MathSciNetCrossRef Yoo, T., Lafortune, S.: Polynomial-time verification of diagnosability of partially observed discrete-event systems. IEEE Trans. Autom. Control 47(9), 1491–1495 (2002)MathSciNetCrossRef
Metadaten
Titel
Decision-Theoretic Monitoring of Cyber-Physical Systems
verfasst von
Andrey Yavolovsky
Miloš Žefran
A. Prasad Sistla
Copyright-Jahr
2016
DOI
https://doi.org/10.1007/978-3-319-46982-9_25

Premium Partner