Bounded Model Checking for GSMP Models of Stochastic Real-Time Systems | Springer Nature Link

Bounded Model Checking for GSMP Models of Stochastic Real-Time Systems | Springer Nature Link
Advertisement
Bounded Model Checking for GSMP Models of Stochastic Real-Time Systems
Conference paper
pp 19–33
Cite this conference paper
Hybrid Systems: Computation and Control
(HSCC 2006)
Abstract
Model checking is a popular algorithmic verification technique for checking temporal requirements of mathematical models of systems. In this paper, we consider the problem of verifying bounded reachability properties of stochastic real-time systems modeled as generalized semi-Markov processes (GSMP). While GSMPs is a rich model for stochastic systems widely used in performance evaluation, existing model checking algorithms are applicable only to subclasses such as discrete-time or continuous-time Markov chains. The main contribution of the paper is an algorithm to compute the probability that a given GSMP satisfies a property of the form “can the system reach a target before time
within
discrete events, while staying within a set of safe states”. For this, we show that the probability density function for the remaining firing times of different events in a GSMP after
discrete events can be effectively partitioned into finitely many regions and represented by exponentials and polynomials. We report on illustrative examples and their analysis using our techniques.
This research was supported by the US National Science Foundation via grants CCR-0410662 and ITR/SY 0121431.
This is a preview of subscription content,
log in via an institution
to check access.
Access this chapter
Log in via an institution
Institutional subscriptions
Preview
Unable to display preview.
Download preview
PDF.
Unable to display preview.
Download preview
PDF.
Similar content being viewed by others
Model-Based Testing for General Stochastic Time
Chapter
Special Subclass of Generalized Semi-Markov Decision Processes with Discrete Time
Chapter
Imprecise Probabilistic Model Checking for Stochastic Multi-agent Systems
Article
Open access
12 June 2023
Explore related subjects
Discover the latest articles, books and news in related subjects, suggested using machine learning.
Markov Process
Stochastic Systems and Control
Stochastic Calculus
Stochastic Differential Equations
Stochastic Analysis
Stochastic Modelling in Statistics
Probabilistic Model Checking in Stochastic Systems
References
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)
Chapter
Google Scholar
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)
Article
MathSciNet
MATH
Google Scholar
Aziz, A., Sanwal, K., Singhal, V., Brayton, R.K.: Model-checking continuous-time markov chains. ACM Transactions on Computational Logic 1(1), 162–170 (2000)
Article
MathSciNet
MATH
Google Scholar
Biere, A., Cimatti, A., Clarke, E., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Proceedings of the 36th ACM/IEEE Design Automation Conference, pp. 317–320 (1999)
Google Scholar
Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press, Cambridge (2000)
Google Scholar
Clarke, E.M., Kurshan, R.P.: Computer-aided verification. IEEE Spectrum 33(6), 61–67 (1996)
Article
Google Scholar
Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. Journal of the ACM 42(4), 857–907 (1995)
Article
MathSciNet
MATH
Google Scholar
German, R.: Performance analysis of communication systems: Modeling with non-Markovian stochastic Petri nets. J. Wiley & Sons, Chichester (2000)
MATH
Google Scholar
Glynn, P.W.: A GSMP formalism for discrete event systems. Proceedings of the IEEE 77(1), 14–23 (1988)
Article
Google Scholar
Hansson, H., Jonsson, B.: A framework for reasoning about time and reliability. In: Proceedings of the Tenth IEEE Real-Time Systems Symposium, pp. 102–111 (1989)
Google Scholar
Haverkort, B.: Performance of computer-communication systems: A model-based approach. Wiley & Sons, Chichester (1998)
Book
Google Scholar
Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering 23(5), 279–295 (1997)
Article
Google Scholar
Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 200–204. Springer, Heidelberg (2002)
Google Scholar
Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Verifying quantitative properties of continuous probabilistic timed automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 123–137. Springer, Heidelberg (2000)
Chapter
Google Scholar
Kwiatkowska, M.Z.: Model checking for probability and time: from theory to pratice. In: Proceedings of the 18th IEEE Symposium on Logic in Computer Science, pp. 351–360 (2003)
Google Scholar
Kwiatkowska, M.Z., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: a hybrid approach. Software Tools for Technology Transfer 6(2), 128–142 (2004)
Article
MATH
Google Scholar
D’Argenio, P., Hermanns, H., Katoen, J.-P., Klaren, R.: Modest - a modeling and description language for stochastic timed systems. In: de Luca, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol. 2165, pp. 87–104. Springer, Heidelberg (2001)
Chapter
Google Scholar
Shedler, G.S.: Regenerative stochastic simulation. Academic Press, London (1993)
MATH
Google Scholar
Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: Proceedings of the 26th IEEE Symposium on Foundations of Computer Science, pp. 327–338 (1985)
Google Scholar
Younes, H., Simmons, R.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 223–235. Springer, Heidelberg (2002)
Chapter
Google Scholar
Download references
Author information
Authors and Affiliations
Department of Computer and Information Science, University of Pennsylvania, USA
Rajeev Alur & Mikhail Bernadsky
Authors
Rajeev Alur
View author publications
Search author on:
PubMed
Google Scholar
Mikhail Bernadsky
View author publications
Search author on:
PubMed
Google Scholar
Editor information
Editors and Affiliations
Center for Control, Dynamical Systems and Computation, University of California, 93106, Santa Barbara, CA, USA
João P. Hespanha
SRI International, 333 Ravenswood Ave, Menlo Park, CA, USA
Ashish Tiwari
Rights and permissions
Reprints and permissions
Copyright information
About this paper
Cite this paper
Alur, R., Bernadsky, M. (2006). Bounded Model Checking for GSMP Models of Stochastic Real-Time Systems.

In: Hespanha, J.P., Tiwari, A. (eds) Hybrid Systems: Computation and Control. HSCC 2006. Lecture Notes in Computer Science, vol 3927. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11730637_5
Download citation
.RIS
.ENW
.BIB
DOI
Publisher Name
Springer, Berlin, Heidelberg
Print ISBN
978-3-540-33170-4
Online ISBN
978-3-540-33171-1
eBook Packages
Computer Science
Computer Science (R0)
Springer Nature Proceedings Computer Science
Share this paper
Anyone you share the following link with will be able to read this content:
Sorry, a shareable link is not currently available for this article.
Provided by the Springer Nature SharedIt content-sharing initiative
Keywords
Model Check
Mass Point
Destination Location
Discrete Event System
Symbolic Model Check
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.
Publish with us
Policies and ethics
Access this chapter
Log in via an institution
Institutional subscriptions