Abstract
In this paper, we discuss how to check Probablistic Computation Tree Logic (PCTL) logic operators over infinite state Discrete Time Markov Chains (DTMC). Probabilistic model checking has been largely applied over finite state space Markov models. Recently infinite state models have been considered when underlying infinite Markov models have special structures. We propose to consider finite state models providing bounds on transient and the stationary distributions in the sense of the \(\preceq_{st}\) stochastic order to check infinite state models. The operators of the PCTL logic are then checked by considering these finite bounding models.
This work is supported by French research project CheckBound, ANR06-SETIN-002.
This is a preview of subscription content, log in via an institution to check access.
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
Abu-Amsha, O., Vincent, J.-M.: An algorithm to bound functionals of Markov chains with large state space. In: 4th INFORMS Conference on Telecommunications, Boca Raton, Florida (1998)
D’Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reduction and Refinement Strategies for Probabilistic Analysis. In: Process Algebra and Probabilistic Methods Performance Modeling and Verification, Springer, Heidelberg (2001)
Andova, S., Hermanns, H., Katoen, J.P.: Discrete-time rewards model Checked. In: Formal Modelling and Analysis of timed Systems (FORMATS 2003), France (2003)
Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model Checking Continuous Time Markov Chains. ACM Trans. on Comp. Logic 1(1), 162–170 (2000)
Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Model-Checking Algorithms for Continuous-Time Markov Chains. IEEE Trans. Software Eng. 29(6), 524–541 (2003)
Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Automated performance and dependability evaluation using Model Checking. In: Calzarossa, M.C., Tucci, S. (eds.) Performance 2002. LNCS, vol. 2459, pp. 261–289. Springer, Heidelberg (2002)
Ben Mamoun, M., Pekergin, N., Younès, S.: Model Checking Continuous-Time Markov Chains by Closed-Form Bounding Distributions. In: QEST, International Conference on the Quantitative Evaluation of Systems, Riverside, pp. 189–198 (2006)
Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, Springer, Heidelberg (1995)
Doisy, M.: A coupling technique for stochastic comparison of functions of Markov processes. Journal of applied Mathematics Decision Sciences 4(1), 39–64 (2000)
Doisy, M.: Comparaison de processus Markoviens, PhD thesis, Université de Pau et des pays de de l’Adour (1992)
Fourneau, J.M., Pekergin, N.: An algorithmic approach to stochastic bounds. In: Calzarossa, M.C., Tucci, S. (eds.) Performance 2002. LNCS, vol. 2459, pp. 64–88. Springer, Heidelberg (2002)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Form. Asp. of Comp. 6, 512–535 (1994)
Hermanns, H., Katoen, J.P., Meyer-Kayser, J., Siegle, M.: A tool for model-checking Markov chains. International Journal on Software Tools for Technology Transfer 4(2), 153–172 (2003)
Heyman, P.D.: Approximating the stationary distribution of an infinite stochastic matrix. Jour. of Applied Probability 28(1), 96–108 (1991)
Katoen, J.-P., Kwiatkowska, M., Norman, G., Parker, D.: Faster and Symbolic CTMC Model Checking. In: de Luca, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol. 2165, pp. 23–38. Springer, Heidelberg (2001)
Kwiatkowska, M., Norman, G., Parker, D.: Prism: Probabilistic symbolic model checker. In: Proceedings of PAPM/PROBMIV 2001 Tools Session (2001)
Muller, A., Stoyan, D.: Comparison Methods for Stochastic Models and Risks. Wiley, New York (2002)
Pekergin, N., Younès, S.: Stochastic Model Checking with Stochastic Comparison. In: Bravetti, M., Kloul, L., Zavattaro, G. (eds.) EPEW/WS-EM 2005. LNCS, vol. 3670, pp. 109–123. Springer, Heidelberg (2005)
Remke, A., Haverkort, B.R., Cloth, L.: Model Checking Infinite-State Markov chains. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, Springer, Heidelberg (2005)
Remke, A., Haverkort, B.R.: CSL model checking algorithms for infinite-state structured Markov chains. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, Springer, Heidelberg (2007)
Seneta, E.: Non-negative Matrices and Markov chains, Springer series in statistics, 3rd edn., USA (2006)
Taleb, H.: Bornes stochastiques pour l’évaluation des réseaux informatiques, PhD thesis, Université Paris 6 (1996)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ben Mamoun, M., Pekergin, N. (2008). Model Checking of Infinite State Space Markov Chains by Stochastic Bounds. In: Al-Begain, K., Heindl, A., Telek, M. (eds) Analytical and Stochastic Modeling Techniques and Applications. ASMTA 2008. Lecture Notes in Computer Science, vol 5055. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68982-9_19
Download citation
DOI: https://doi.org/10.1007/978-3-540-68982-9_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68980-5
Online ISBN: 978-3-540-68982-9
eBook Packages: Computer ScienceComputer Science (R0)