Abstract
This chapter constitutes a smooth introduction in the field of hybrid systems, discussing issues like modelling classes, analysis and verification, how randomness appears and which stochastic models can be used to capture it. The chapter starts with the presentation of models for deterministic hybrid systems considering two main approaches: the automata perspective and the dynamical system perspective. Then existing algorithmic (model checking) and deductive (theorem proving) techniques for hybrid systems are briefly discussed. The main body of this chapter is dedicated to the description of stochastic models that result by randomising different elements in the structure of classical hybrid systems. Classes of stochastic hybrid systems (like probabilistic hybrid automata, stochastic hybrid automata, switching diffusion processes, general stochastic hybrid automata) are briefly exposed and comparison criteria are underlined.
Basically, under standard assumptions all these models give rise to different classes of Markov processes (with regime changing) with quite good analytic properties. The jumping/switching structure is essential for establishing the main properties of these Markov processes.
Keywords
- Stochastic Hybrid Systems
- Hybrid Automata
- Switching Diffusion Process (SDP)
- Stochastic Hybrid Processes (SHP)
- Piecewise Deterministic Markov Processes (PDMP)
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Abate, A., Prandini, M., Lygeros, J., Sastry, S.: Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica 44(11), 2724–2734 (2008)
Abate, A., Katoen, J.-P., Prandini, M., Lygeros, J.: Approximate model checking of stochastic hybrid systems. Eur. J. Control 6, 624–641 (2010)
Alur, R., Henzinger, T.A., Ho, P.-H.: Automated symbolic verification of embedded systems. IEEE Trans. Softw. Eng. 22(3), 181–201 (1996)
Arnold, L.: Stochastic Differential Equations: Theory and Applications. Wiley-Interscience, New York (1974)
Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model checking continuous time Markov chains. ACM Trans. Comput. Log. 1(1), 162–170 (2000)
Baier, C., Katoen, J.-P., Hermanns, H.: Approximate symbolic model checking of continuous time Markov chains. In: Baeten, J.C.M., Mauw, S. (eds.) Concurrency Theory. Lecture Notes in Computer Science, vol. 1664, pp. 146–162. Springer, Berlin (1999)
Bensoussan, A., Menaldi, J.L.: Stochastic hybrid control. J. Math. Anal. Appl. 249, 261–288 (2000)
Biere, A., Cimatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 118–149 (2003)
Blom, H.A.P.: Stochastic hybrid processes with hybrid jumps. In: Analysis and Design of Hybrid System, pp. 319–324. IFAC Press, New York (2003)
Blom, H.A.P.: Bayesian estimation for decision—directed stochastic control. PhD Thesis, Delft University of Technology (1990)
Blom, H.A.P., Bakker, G.J., Krystul, J.: Probabilistic reachability analysis for large scale stochastic hybrid systems. In: Proc. of the 46th IEEE Conference on Decision and Control, pp. 3182–3189 (2007)
Borkar, V.S., Ghosh, M.K., Sahay, P.: Optimal control of a stochastic hybrid system with discounted cost. J. Optim. Theory Appl. 101(3), 557–580 (1999)
Boulton, R.J., Gottliebsen, H., Hardy, R., Kelsey, T., Martin, U.: Design verification for control engineering. In: Boiten, E.A., Derrick, J., Smith, G. (eds.) Conference on Integrated Formal Methods. Lecture Notes in Computer Science, vol. 2999, pp. 21–35. Springer, Berlin (2004)
Branicky, M.S.: Studies in hybrid systems: modeling, analysis and control. Sc.D. Thesis, MIT (June 1995)
Branicky, M.S., Borkar, V.S., Mitter, S.K.: A unified framework for hybrid control: model and optimal control theory. IEEE Trans. Autom. Control 43(1), 31–45 (1998)
Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35(8), 677–691 (1986)
Bujorianu, M.L., Lygeros, J.: Reachability questions in piecewise deterministic Markov processes. In: Maler, O., Pnueli, A. (eds.) Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, vol. 2623, pp. 126–140. Springer, Berlin (2003)
Chen, T., Han, T., Mereacre, A., Katoen, J.-P.: Model checking of continuous-time Markov chains against timed automata specifications. Log. Methods Comput. Sci. 7(1), 1–34 (2011)
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244–263 (1986)
Congdon, P.: Applied Bayesian Modelling. Wiley Series in Probability and Statistics (2003)
Dang, T., Maler, O.: Reachability analysis via face lifting. In: Sastry, S., Henzinger, T.A. (eds.) Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, vol. 1386, pp. 96–109. Springer, Berlin (1998)
Davis, M.H.A.: Markov Models and Optimization. Chapman & Hall, London (1993)
Davis, M.H.A.: Piecewise-deterministic Markov processes: a general class of non-diffusion stochastic models. J. R. Stat. Soc. B, 46(3), 353–388 (1984)
Ephraim, Y., Merhav, N.: Hidden Markov processes. IEEE Trans. Inf. Theory 48(6), 1518–1569 (2002) (Special Issue on Shannon Theory: perspectives, trends, and applications)
Ethier, S.N., Kurtz, T.G.: Markov Processes: Characterization and Convergence. Wiley, New York (1986)
Fränzle, M., Hermanns, H., Teige, T.: Stochastic satisfiability modulo theory: a novel technique for the analysis of probabilistic hybrid systems. In: Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, pp. 172–186. Springer, Berlin (2008)
Fränzle, M., Herde, C.: Efficient proof engines for bounded model checking of hybrid systems. In: Workshop on Formal Methods for Industrial Critical Systems (2004). Electron. Notes Theor. Comput. Sci. 133, 119–137 (2005)
Ghosh, M.K., Arapostathis, A., Marcus, S.I.: An optimal control problem arising in flexible manufacturing systems. In: Proc. of 30th IEEE Conf. on Decision and Control, pp. 1844–1849 (1991)
Ghosh, M.K., Arapostathis, A., Marcus, S.I.: Optimal control of switching diffusions with application to flexible manufacturing systems. SIAM J. Control Optim. 31(5), 1183–1204 (1993)
Ghosh, M.K., Arapostathis, A., Marcus, S.I.: Ergodic control of switching diffusions. SIAM J. Control Optim. 35(6), 1952–1988 (1997)
Havelund, K., Larsen, K.G., Skou, A.: Formal verification of a power controller using the real-time model checker UPAAL. In: Katoen, J.P. (ed.) Formal Methods for Real-Time and Probabilistic Systems. Lecture Notes in Computer Science, vol. 1601, pp. 277–298. Springer, Berlin (1999)
Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: A user guide to HYTECH. In: Brinksma, E., Cleaveland, R., Larsen, K.G., Maragaria, T., Steffen, B. (eds.) TACAS 95: Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 1019, pp. 41–71. Springer, Berlin (1995)
Henzinger, T.A.: The theory of hybrid automata. In: Proceedings 11th Logic in Computer Science, pp. 278–292. IEEE Comput. Soc., Los Alamitos (1996)
Hofbaur, M.W., Williams, B.C.: Mode estimation of probabilistic hybrid systems. In: Tomlin, C.J., Greenstreet, M.R. (eds.) Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, vol. 2289, pp. 253–266. Springer, Berlin (2002)
Hu, J., Lygeros, J., Sastry, S.: Towards a theory of stochastic hybrid systems. In: Lynch, N., Krogh, B. (eds.) Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, vol. 1790, pp. 160–173. Springer, Berlin (2000)
Jacod, J., Shiryayev, A.N.: Limit Theorems for Stochastic Processes. Springer, New York (1987)
Koutsoukos, X., Riley, D.: Computational methods for verification of stochastic hybrid systems. IEEE Trans. Syst. Man Cybern., Part A, Syst. Hum. 38(2), 385–396 (2008)
Krystul, J., Blom, H.A.P.: Sequential Monte Carlo simulation of rare event probability in stochastic hybrid systems. Preprint, 16th IFAC World Congress (2005)
Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: a hybrid approach. International. J. on Software Tools Technology Transfer 6, 128–142 (2004)
Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Verifying quantitative properties of continuous probabilistic timed automata. In: Palamidessi, C. (ed.) International Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 1877, pp. 123–137. Springer, Berlin (2000)
Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theor. Comput. Sci. 282, 101–150 (2002)
Kurzhanski, A.B., Varaiya, P.: Ellipsoidal techniques for reachability analysis. In: Lynch, N., Krogh, B. (eds.) Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, vol. 1790, pp. 202–214. Springer, Berlin (2000)
Kurzhanski, A.B., Varaiya, P.: Ellipsoidal techniques for hybrid dynamics: the reachability problem. In: Dayawansa, W.P., Lindquist, A., Zhou, Y. (eds.) New Directions and Applications in Control Theory. Lecture Notes in Control and Information Sciences, vol. 321, pp. 193–205. Springer, Berlin (2005)
Lafferriere, G., Pappas, G.J., Sastry, S.: Reachability analysis of hybrid systems using bisimulations. In: Proc. of the IEEE Conference on Decision and Control, pp. 1623–1628 (1998)
Lemmon, M., Stiver, J.A., Antsaklis, P.J.: Event identification and intelligent hybrid control. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) Hybrid Systems. Lecture Notes in Computer Science, vol. 736, pp. 268–296. Springer, Berlin (1993)
Limnios, N., Oprisan, G.: Semi-Markov Processes and Reliability. Birkhäuser, Boston (2001)
Lygeros, J., Johansson, K.H., Simić, S.N., Zhang, J., Sastry, S.: Dynamical properties of hybrid automata. IEEE Trans. Autom. Control 48, 2–17 (2003)
Lygeros, J.: Lecture notes on hybrid systems (2004)
Lygeros, J., Tomlin, C., Sastry, S.: Controllers for reachability specifications of hybrid systems. Automatica 35, 349–370 (1999)
Lygeros, J., Tomlin, C., Sastry, S.: A game theoretic approach to controller design for hybrid systems. Proc. IEEE 88, 949–969 (2000)
Mitchell, I., Tomlin, C.: Level set methods for computation in hybrid systems. In: Lynch, N., Krogh, B. (eds.) Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, vol. 1790, pp. 310–323. Springer, Berlin (2000)
Nerode, A., Kohn, W.: Models for hybrid systems: automata, topologies, controllability, observability. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, vol. 736, pp. 317–356. Springer, Berlin (1993)
Pola, G., Bujorianu, M.L., Lygeros, J., Di Benedetto, M.D.: Stochastic hybrid models: an overview with applications to air traffic management. In: Proc. of the Analysis and Design of Hybrid Systems, pp. 45–50. IFAC Elsevier, Amsterdam (2003)
Riley, D., Koutsoukos, X.: Simulation of stochastic hybrid systems using probabilistic boundary detection and adaptive time stepping. Simul. Model. Pract. Theory 18(9), 1397–1411 (2010)
Shtrichman, O.: Tuning SAT checkers for bounded model checking. In: Emerson, E.A., Sistla, A.P. (eds.) Computer Aided Verification. Lecture Notes in Computer Science, vol. 1855, pp. 480–494. Springer, Berlin (2000)
Sproston, J.: Analysing subclasses of probabilistic hybrid automata. In: Kwiatkowska, M.Z. (ed.) 2nd International Workshop on Probabilistic Methods in Verification (1999)
Varaiya, P.: Reach set computation using optimal control problems in multidimensional systems. In: Proc. of KIT Workshop on Verification of Hybrid Systems (1998)
Zhou, K., Doyle, J.C., Glover, K.: Robust and Optimal Control. Prentice Hall, Upper Saddle River (1996)
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag London Limited
About this chapter
Cite this chapter
Bujorianu, L.M. (2012). Hybrid Systems: Deterministic to Stochastic Perspectives. In: Stochastic Reachability Analysis of Hybrid Systems. Communications and Control Engineering. Springer, London. https://doi.org/10.1007/978-1-4471-2795-6_3
Download citation
DOI: https://doi.org/10.1007/978-1-4471-2795-6_3
Published:
Publisher Name: Springer, London
Print ISBN: 978-1-4471-2794-9
Online ISBN: 978-1-4471-2795-6
eBook Packages: EngineeringEngineering (R0)