Bayesian Hybrid Automata: A Formal Model of Justified Belief in Interacting Hybrid Systems Subject to Imprecise Observation
How to Cite
Copyright (c) 2022 Paul Kröger and Martin Fränzle
This work is licensed under a Creative Commons Attribution 4.0 International License.
Hybrid discrete-continuous system dynamics arises when discrete actions, e.g. by a decision algorithm, meet continuous behaviour, e.g. due to physical processes and continuous control. A natural domain of such systems are emerging smart technologies which add elements of intelligence, co-operation, and adaptivity to physical entities, enabling them to interact with each other and with humans as systems of (human-)cyber-physical systems or (H)CPSes.
Various flavours of hybrid automata have been suggested as a means to formally analyse CPS dynamics. In a previous article, we demonstrated that all these variants of hybrid automata provide inaccurate, in the sense of either overly pessimistic or overly optimistic, verdicts for engineered systems operating under imprecise observation of their environment due to, e.g., measurement error. We suggested a revised formal model, called Bayesian hybrid automata, that is able to represent state tracking and estimation in hybrid systems and thereby enhances precision of verdicts obtained from the model in comparison to traditional model variants.
In this article, we present an extended definition of Bayesian hybrid automata which incorporates a new class of guard and invariant functions that allow to evaluate traditional guards and invariants over probability distributions. The resulting framework allows to model observers with knowledge about the control strategy of an observed agent but with imprecise estimates of the data on which the control decisions are based.
- Alessandro Abate, Joost-Pieter Katoen, John Lygeros, and Maria Prandini. Approximate model checking of stochastic hybrid systems. Eur. J. Control, 16(6):624-641, 2010. URL: https://doi.org/10.3166/ejc.16.624-641.
- Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger, and Pei-Hsin Ho. Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In Robert L. Grossman, Anil Nerode, Anders P. Ravn, and Hans Rischel, editors, Hybrid Systems, volume 736 of Lecture Notes in Computer Science, pages 209-229. Springer, 1992. URL: https://doi.org/10.1007/3-540-57318-6_30.
- David Barber. Bayesian Reasoning and Machine Learning. Cambride University Press, 2012. URL: https://doi.org/10.1017/CBO9780511804779.
- Karl Berntorp and Stefano Di Cairano. Particle filtering for automotive: A survey. In 22th International Conference on Information Fusion, pages 1-8, July 2019. URL: https://www.merl.com/publications/TR2019-069.
- L.M. Bujorianu and J. Lygeros. Toward a general theory of stochastic hybrid systems. In Stochastic Hybrid Systems: Theory and Safety Critical Applications, volume 337 of LNCIS, pages 3-30. Springer-Verlag, 2006. URL: https://doi.org/10.1007/11587392_1.
- C. Combastel. Merging Kalman filtering and zonotopic state bounding for robust fault detection under noisy environment. IFAC-PapersOnLine, 48(21):289-295, 2015. 9th IFAC Symposium on Fault Detection, Supervision and Safety for Technical Processes SAFEPROCESS 2015. URL: https://doi.org/10.1016/j.ifacol.2015.09.542.
- Christophe Coué, Cédric Pradalier, Christian Laugier, Thierry Fraichard, and Pierre Bessiere. Bayesian occupancy filtering for multitarget tracking: an automotive application. International Journal of Robotics Research, 25(1):19-30, January 2006. URL: https://doi.org/10.1177/0278364906061158.
- Werner Damm, Martin Fränzle, Andreas Lüdtke, Jochem W. Rieger, Alexander Trende, and Anirudh Unni. Integrating neurophysiological sensors and driver models for safe and performant automated vehicle control in mixed traffic. In 2019 IEEE Intelligent Vehicles Symposium, pages 82-89. IEEE, 2019. URL: https://ieeexplore.ieee.org/xpl/conhome/8792328/proceeding.
- M.H.A. Davis. Markov Models and Optimization. Chapman & Hall, London, 1993.
- J. Ding, A. Abate, and C. Tomlin. Optimal control of partially observable discrete time stochastic hybrid systems for safety specifications. In 2013 American Control Conference, pages 6231-6236, June 2013. URL: https://doi.org/10.1109/ACC.2013.6580815.
- Alexandre Donzé and Oded Maler. Robust satisfaction of temporal logic over real-valued signals. In Krishnendu Chatterjee and Thomas A. Henzinger, editors, Formal Modeling and Analysis of Timed Systems - 8th International Conference, FORMATS 2010, Klosterneuburg, Austria, September 8-10, 2010. Proceedings, volume 6246 of Lecture Notes in Computer Science, pages 92-106. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15297-9_9.
- Alberto Elfes. Using occupancy grids for mobile robot perception and navigation. Computer, 22(6):46-57, June 1989. URL: https://doi.org/10.1109/2.30720.
- Martin Fränzle, Mingshuai Chen, and Paul Kröger. In memory of Oded Maler: automatic reachability analysis of hybrid-state automata. SIGLOG News, 6(1):19-39, 2019. URL: https://doi.org/10.1145/3313909.3313913.
- Martin Fränzle, Ernst Moritz Hahn, Holger Hermanns, Nicolás Wolovick, and Lijun Zhang. Measurability and safety verification for stochastic hybrid systems. In Marco Caccamo, Emilio Frazzoli, and Radu Grosu, editors, Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, IL, USA, April 12-14, 2011, pages 43-52. ACM, 2011. URL: https://doi.org/10.1145/1967701.1967710.
- Martin Fränzle, Holger Hermanns, and Tino Teige. Stochastic satisfiability modulo theory: A novel technique for the analysis of probabilistic hybrid systems. In Magnus Egerstedt and Bud Mishra, editors, Hybrid Systems: Computation and Control, 11th International Workshop, HSCC 2008, St. Louis, MO, USA, April 22-24, 2008. Proceedings, volume 4981 of Lecture Notes in Computer Science, pages 172-186. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78929-1_13.
- Martin Fränzle and Paul Kröger. The demon, the gambler, and the engineer - reconciling hybrid-system theory with metrology. In Cliff Jones, Ji Wang, and Naijun Zhan, editors, Symposium on Real-Time and Hybrid Systems, volume 11180 of Theoretical Computer Science and General Issues, pages 165-185, Cham, 2018. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-01461-2_9.
- Martin Fränzle and Paul Kröger. Guess what I'm doing! Rendering formal verification methods ripe for the era of interacting intelligent systems. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation: Applications, pages 255-272, Cham, 2020. Springer International Publishing.
- Adrian Gambier. Multivariable adaptive state-space control: A survey. In 2004 5th Asian Control Conference (IEEE Cat. No.04EX904), volume 1, pages 185-191 Vol.1, July 2004.
- J. Hu, J. Lygeros, and S. Sastry. Towards a theory of stochastic hybrid systems. In Hybrid Systems: Computation and Control, volume 1790 of LNCS, pages 160-173. Springer-Verlag, 2000. URL: https://doi.org/10.1007/3-540-46430-1_16.
- Rudolph Emil Kálmán. A new approach to linear filtering and prediction problems. Transactions of the ASME-Journal of Basic Engineering, 82(Series D):35-45, 1960. URL: https://doi.org/10.1115/1.3662552.
- S. Kowalewski, M. Garavello, H. Guéguen, G. Herberich, R. Langerak, B. Piccoli, J. W. Polderman, and C. Weise. Hybrid automata, pages 57-86. Cambridge University Press, 2009. URL: https://doi.org/10.1017/CBO9780511807930.004.
- Helge Langseth, Thomas D. Nielsen, Rafael Rumí, and Antonio Salmerón. Inference in hybrid bayesian networks. Reliability Engineering & System Safety, 94(10):1499-1509, 2009. URL: https://doi.org/10.1016/j.ress.2009.02.027.
- Eugene Lavretsky. Robust and adaptive control methods for aerial vehicles. In Kimon P. Valavanis and George J. Vachtsevanos, editors, Handbook of Unmanned Aerial Vehicles, pages 675-710, Dordrecht, 2015. Springer Netherlands. URL: https://doi.org/10.1007/978-90-481-9707-1_50.
- R. P. S. Mahler. Multitarget Bayes filtering via first-order multitarget moments. IEEE Transactions on Aerospace and Electronic Systems, 39(4):1152-1178, October 2003. URL: https://doi.org/10.1109/TAES.2003.1261119.
- Michael Maschler, Eilon Solan, and Shmuel Zamir. Game Theory. Cambridge University Press, 2013. URL: https://doi.org/10.1017/cbo9780511794216.
- Kevin P. Murphy. Switching Kalman filters, 1998.
- Kumpati S. Narendra and Zhuo Han. Adaptive control using collective information obtained from multiple models. IFAC Proceedings Volumes, 44(1):362-367, 2011. 18th IFAC World Congress. URL: https://doi.org/10.3182/20110828-6-IT-1002.02237.
- Anil Nerode and Wolf Kohn. Models for hybrid systems: Automata, topologies, controllability, observability. In Robert L. Grossman, Anil Nerode, Anders P. Ravn, and Hans Rischel, editors, Hybrid Systems, volume 736 of Lecture Notes in Computer Science, pages 317-356. Springer, 1992. URL: https://doi.org/10.1007/3-540-57318-6_35.
- Simo Särkkä. Bayesian Filtering and Smoothing. Cambridge University Press, New York, NY, USA, 2013.
- C. Sherlock, A. Golightly, and C. S. Gillespie. Bayesian inference for hybrid discrete-continuous stochastic kinetic models. Inverse Problems, 30(11):114005, November 2014. URL: https://doi.org/10.1088/0266-5611/30/11/114005.
- Jeremy Sproston. Decidable model checking of probabilistic hybrid automata. In Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT 2000), volume 1926 of LNCS, pages 31-45. Springer, 2000. URL: https://doi.org/10.1007/3-540-45352-0_5.
- Håkan L. S. Younes and Reid G. Simmons. Probabilistic verification of discrete event systems using acceptance sampling. In Ed Brinksma and Kim Guldstrand Larsen, editors, Computer Aided Verification, 14th International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings, volume 2404 of Lecture Notes in Computer Science, pages 223-235. Springer, 2002. URL: https://doi.org/10.1007/3-540-45657-0_17.