Abstract
Recently, there is an explosive development of fluid approa- ches to computer and distributed systems. These approaches are inherently stochastic and generate continuous state space models. Usually, the performance measures for these systems are defined using probabilities of reaching certain sets of the state space. These measures are well understood in the discrete context and many efficient model checking procedures have been developed for specifications involving them. The continuous case is far more complicated and new methods are necessary. In this paper we propose a general model checking strategy founded on advanced concepts and results of stochastic analysis. Due to the problem complexity, in this paper, we achieve the first necessary step of characterizing mathematically the problem. We construct upper bounds for the performance measures using Martin capacities. We introduce a concept of bisimulation that preserves the performance measures and a metric that characterizes the bisimulation.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Alur, R., Pappas, G.J. (eds.): HSCC 2004. LNCS, vol. 2993. Springer, Heidelberg (2004)
Bertsekas, D.P., Shreve, S.E.: Stochastic Optimal Control: The Discrete-Time Case. Athena Scientific (1996)
Bohacek, S., Hespanha, J., Lee, J., Obraczka, K.: Modeling Data Communication Networks Using Hybrid Systems. IEEE/ACM Trans. on Networking (2006)
Borkar, V.S.: Probability Theory. An Advance Course. Springer, Heidelberg (1995)
Bujorianu, M.L.: Extended Stochastic Hybrid Systems and their Reachability Problem. In: [1], pp. 234–249 (2004)
Bujorianu, M.L., Lygeros, J., Bujorianu, M.C.: Bisimulation for General Stochastic Hybrid Systems. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 198–214. Springer, Heidelberg (2005)
Bujorianu, M.L.: Capacities and Markov Processes. Lib. Math. 24, 201–210 (2004)
Bujorianu, M.L., Bujorianu, M.C.: Distributed Stochastic Hybrid Systems. In: Kucera, A. (ed.) Proceedings of IFAC 2005. Elsevier Press, Amsterdam (2005)
Bujorianu, M.L., Bujorianu, M.C., Blom, H.A.P.: Towards Model Checking Stochastic Hybrid Systems by Approximate Abstractions (Submitted)
Choquet, G.: Theory of Capacities. Annales de l’Institut Fourier, Grenoble 5, 131–291 (1953)
Chung, K.L.: Probabilistic Approach in Potential Theory to the Equilibrium Problem. Annales de L’Institut Fourier,Grenoble 23, 313–322 (1973)
Ciardo, G., Nicol, D., Trivedi, K.S.: Discrete-Event Simulation of Fluid Stochastic Petri Nets. In: Proc. 7th Int. Workshop on Petri Nets and Performance Models, pp. 217–225 (1997)
Davis, M.H.A.: Markov Models and Optimization. Chapman & Hall, London (1993)
Desharnais, J., Gupta, V., Jagadeesan, Panangaden, P.: Weak Bisimulation is Sound and Complete for PCTL. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 355–370. Springer, Heidelberg (2002)
Dempster, D.: Upper and Lower Probabilities Induced by a Multi-valued Mapping. Ann. Math. Statist. 38, 325–339 (1967)
Dubois, D., Prade, H.: Modelling Uncertainty and Inductive Inference: A Survey of Recent Non-Additive Probability Systems. Acta Psychologica 68, 53–78 (1988)
Fitzsimmons, P.J.: Markov Processes with Equal Capacities. J. Theor. Prob. 12, 271–292 (1999)
Horton, G., Kulkarni, V., Nicol, D., Trivedi, K.S.: Fluid Stochastic Petri Nets: Theory, Applications, and Solution. Eur. J. Oper. Res. 105(1), 184–201 (1998)
Huber, P.J.: Robust Statistics. Willey, New York (1980)
Hermanns, H., Katoen, J.-P.: Automated Compositional Markov Chain Generation for a Plain-old Telephone System. Science of Computer Programming 36(1), 97–127 (2000)
Hespanha, J.P.: Stochastic Hybrid Systems: Application to Communication Networks. In: [1], pp. 387–401 (2004)
Kang, W., Kelly, F.P., Lee, N.H., Williams, R.J.: Fluid and Brownian Approximations for an Internet congestion control model. In: Proceedings of the 43rd IEEE Conference on Decision and Control (2004)
Kelly, F.P.: Mathematical Modelling of the Internet. In: Engquist, B., Schmid, W. (eds.) Mathematics Unlimited - 2001 and Beyond, pp. 670–685. Springer, Heidelberg (2001)
Kulkarni, V., Trivedi, K.S.: FSPNs: Fluid Stochastic Petri Nets. In: Ajmone Marsan, M. (ed.) ICATPN 1993. LNCS, vol. 691, pp. 24–31. Springer, Heidelberg (1993)
Kwiatkowska, Norman, G., Parker, D., Sproston, J.: Performance Analysis of Probabilistic Timed Automata using Digital Clocks. In: Formal Methods in System Design. Springer, Heidelberg (to appear, 2006)
Kwiatkowska, M., Norman, G., Segal, R., Sproston, J.: Automatic Verification of Real Time Systems with Discrete Probability Distribution. Theoretical Computer Science 282, 101–150 (2002)
NWO Project Description AiSHA: Abstraction in Stochastic and Hybrid process Algebra, www.onderzoekinformatie.nl/en/oi/nod/onderzoek/OND1303139
Pola, G., Bujorianu, M.L., Lygeros, J., Di Benedetto, M.D.: Stochastic Hybrid Models: An Overview with applications to Air Traffic Management. In: Proccedings Analysis and Design of Hybrid Systems IFAC ADHS 2003, pp. 45–50 (2003)
Shafer, G.: A Mathematical Theory of Evidence. Princeton Univ. Press, Princeton (1976)
Schmeidler, D.: Subjective Probability and Expected Utility Without Additivity. Econometrica 57, 571–587 (1989)
Viertl, R.: Statistical Methods for Non-Precise Data. CRC Press, Boca Raton (1996)
Walley, P.: Statistical Reasoning with Imprecise Probabilities. Chapman & Hall, Boca Raton (1991)
Wolter, K.: Second Order Fluid Stochastic Petri Nets: an Extension of GSPNs for Approximate and Continuous Modeling. In: World Congress on System Simulation, pp. 328–332 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bujorianu, M.L., Bujorianu, M.C. (2006). Model Checking for a Class of Performance Properties of Fluid Stochastic Models. In: Horváth, A., Telek, M. (eds) Formal Methods and Stochastic Models for Performance Evaluation. EPEW 2006. Lecture Notes in Computer Science, vol 4054. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11777830_7
Download citation
DOI: https://doi.org/10.1007/11777830_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-35362-1
Online ISBN: 978-3-540-35365-2
eBook Packages: Computer ScienceComputer Science (R0)