Abstract
We consider the problem of verifying reachability properties of stochastic real-time systems modeled as generalized semi-Markov processes (GSMPs). The standard simulation-based techniques for GSMPs are not adequate for solving verification problems, and existing symbolic techniques either require memoryless distributions for firing times, or approximate the problem using discrete time or bounded horizon. In this paper, we present a symbolic solution for the case where firing times are random variables over a rich class of distributions, but only one event is allowed to retain its firing time when a discrete change occurs. The solution allows us to compute the probability that such a GSMP satisfies a property of the form “can the system reach a target, while staying within a set of safe states”. We report on illustrative examples and their analysis using our procedure.
This research was supported by the US National Science Foundation via grants CCR-0410662 and CSR-EHS 0509143.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Alur, R., Bernadsky, M.: Bounded model checking for GSMP models of stochastic real-time systems. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 19–33. Springer, Heidelberg (2006)
Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking for probabilistic real-time systems. In: Leach Albert, J., Monien, B., Rodríguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol. 510, pp. 115–136. Springer, Heidelberg (1991)
Alur, R., Dill, D.L.: A theory of timed automata. TCS 126, 183–235 (1994)
Asmussen, S.: Applied Probability and Queues. Springer, Heidelberg (2006)
Aziz, A., et al.: Model-checking continuous-time Markov chains. ACM Trans. on Computational Logic 1(1), 162–170 (2000)
Choi, H., Kulkarni, V.G., Trivedi, K.: Markov regenerative stochastic Petri nets. Performance Evaluation 20, 337–357 (1994)
Cumani, A.: Esp — A package for the evaluation of stochastic Petri nets with phase-type distributed transition times. In: Proc. of Int. Workshop on Timed Petri Nets, Torino, Italy, no. 674, pp. 144–151. IEEE Computer Society Press, Los Alamitos (1985)
German, R.: Performance analysis of communication systems: Modeling with non-Markovian stochastic Petri nets. J. Wiley & Sons, Chichester (2000)
Glynn, P.W.: A GSMP formalism for discrete event systems. Proc. of the IEEE 77(1), 14–23 (1988)
Haverkort, B.: Performance of computer-communication systems: A model-based approach. Wiley & Sons, Chichester (1998)
Kwiatkowska, M.Z.: Model checking for probability and time: from theory to practice. In: Proc. of the 18th IEEE Symposium on Logic in CS, pp. 351–360. IEEE Computer Society Press, Los Alamitos (2003)
Lindemann, C., Thümmler, A.: Numerical Analysis of Generalized Semi-Markov Processes. Research Report No. 722, Dept. of CS, University of Dortmund (1999)
López, G., Hermanns, H., Katoen, J.-P.: Beyond Memoryless Distributions: Model Checking Semi-Markov Chains. In: de Luca, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol. 2165, pp. 57–70. Springer, Heidelberg (2001)
Shedler, G.S.: Regenerative stochastic simulation. Academic Press, London (1993)
Ye, H., Corless, R.: Solving linear integral equations in Maple. In: Proc. of the Int. Symposium on Symbolic and Algebraic Computation, pp. 95–102 (1992)
Zeilberger, D.: Holonomic Systems Approach To Special Functions. J. Computational and Applied Math. 32, 321–368 (1990)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Bernadsky, M., Alur, R. (2007). Symbolic Analysis for GSMP Models with One Stateful Clock. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds) Hybrid Systems: Computation and Control. HSCC 2007. Lecture Notes in Computer Science, vol 4416. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71493-4_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-71493-4_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71492-7
Online ISBN: 978-3-540-71493-4
eBook Packages: Computer ScienceComputer Science (R0)