Abstract
This paper presents a stochastic variant of Hennessy-Milner logic that is interpreted over (state-labeled) inhomogeneous continuous-time Markov chains (ICTMCs), i.e., Markov chains in which transition rates are functions over time t. For piecewise constant rate functions, the model-checking problem is shown to be reducible to finding the zeros of an exponential polynomial. Using Sturm sequences and Newton’s method, we obtain an approximative model-checking algorithm which is linear in the size of the ICTMC, logarithmic in the number of bits precision, and exponential in the nesting depth of the formula.
This research has taken place as part of the Research Training Group 1298 ALGOSYN funded by the German Research Council.
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 subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Aho, A.V., Hopcroft, J.E., Ullman, J.D.: Design and Analysis of Computer Algorithms. Addison-Wesley, Reading (1974)
Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking for real-time systems. In: Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pp. 414–425 (1990)
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
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.R., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. on Softw. Eng. 29(6), 524–541 (2003)
Buchholz, P.: Exact and ordinary lumpability in finite Markov chains. J. of Applied Probability 31, 59–75 (1994)
Clark, G., Gilmore, S., Hillston, J., Ribaudo, M.: Exploiting modal logic to express performance measures. In: Haverkort, B.R., Bohnenkamp, H.C., Smith, C.U. (eds.) TOOLS 2000. LNCS, vol. 1786, pp. 247–261. Springer, Heidelberg (2000)
Desharnais, J., Panangaden, P.: Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes. J. Log. Algebr. Program 56(1-2), 99–115 (2003)
Hamming, R.W.: Numerical Methods for Scientists and Engineers. McGraw-Hill, New York (1973)
Han, T., Katoen, J.-P., Mereacre, A.: Compositional modeling and minimization of time-inhomogeneous Markov chains. In: Hybrid Systems: Computation and Control. LNCS, vol. 4981, pp. 244–258. Springer, Heidelberg (2008)
Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137–161 (1985)
Henrici, P., Kenan, W.R.: Applied & Computational Complex Analysis: Power Series Integration Conformal Mapping Location of Zero. John Wiley & Sons, Chichester (1988)
Hermanns, H.: Interactive Markov Chains: The Quest for Quantified Quality. LNCS, vol. 2428. Springer, Heidelberg (2002)
Hillston, J.: A Compositional Approach to Performance Modeling. Cambridge University Press, Cambridge (1996)
Katoen, J.-P., Khattri, M., Zapreev, I.S.: A Markov reward model checker. In: Quantitative Evaluation of Systems (QEST), pp. 243–245. IEEE CS Press, Los Alamitos (2005)
Kwiatkowska, M.Z., Norman, G., Parker, D.A.: Probabilistic symbolic model checking using PRISM: a hybrid approach. J. on Software Tools for Technology Transfer 6(2), 128–142 (2004)
Laguerre, E.: Sur la théorie des équations numériques. J. Math. Pures Appl. 9, 99–146 (1883); (3e série)
Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1–28 (1991)
Parma, A., Segala, R.: Logical characterizations of bisimulations for discrete probabilistic systems. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423, pp. 287–301. Springer, Heidelberg (2007)
Reif, J.H.: An \(\mathcal{O}\left(n\log^3n\right)\) algorithm for the real root and symmetric tridiagonal eigenvalue problems. In: 34th Annual IEEE Conference on Foundations of Computer Science (FOCS 1993), pp. 626-635 (1993)
Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, MIT, Dept. of Electrical Eng. and Computer Sci. (1995)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Katoen, JP., Mereacre, A. (2008). Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains. In: Cassez, F., Jard, C. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2008. Lecture Notes in Computer Science, vol 5215. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85778-5_15
Download citation
DOI: https://doi.org/10.1007/978-3-540-85778-5_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85777-8
Online ISBN: 978-3-540-85778-5
eBook Packages: Computer ScienceComputer Science (R0)