Abstract
In this paper a hierarchical Markov model is proposed for the temporal analysis of periodic stochastic systems. For analyzing the system behavior, an interval linear temporal logic, ipLTL, is presented, which is an LTL with linear inequalities on the probability mass functions (pmfs) as an atomic proposition. We prove that the proposed model converges to a steady state which enables us to develop an algorithm to determine the bound of the system execution time and check the specification written in ipLTL. Some properties of the manufacturing systems are analyzed and verified to illustrate the efficiency of our methods.
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.
References
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)
Aziz, A., Singhal, V., Balarin, F., Brayton, R.K., Sangiovanni-Vincentelli, A.L.: It usually works: The temporal logic of stochastic systems. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 155–165. Springer, Heidelberg (1995)
Bianco, A., De Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499–513. Springer, Heidelberg (1995)
Kwon, Y., Agha, G.: Linear inequality ltl (iltl): A model checker for discrete time markov chains. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 194–208. Springer, Heidelberg (2004)
Kwon, Y., Agha, G.: Verifying the evolution of probability distributions governed by a dtmc. IEEE Transactions on Software Engineering 37(1), 126–141 (2011)
Papoulis, A., Pillai, S.U.: Probability, random variables, and stochastic processes. Tata McGraw-Hill Education (2002)
Delcher, A.L., Harmon, D., Kasif, S., White, O., Salzberg, S.L.: Improved microbial gene identification with glimmer. Nucleic Acids Research 27(23), 4636–4641 (1999)
Pinsky, M., Karlin, S.: An introduction to stochastic modeling. Academic press (2010)
Sinkhorn, R.: A relationship between arbitrary positive matrices and doubly stochastic matrices. The Annals of Mathematical Statistics 35(2), 876–879 (1964)
Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Proceedings of the Fifteenth IFIP WG6. 1 International Symposium on Protocol Specification, Testing and Verification. IFIP (1995)
Strang, G.: Introduction to linear algebra. SIAM (2003)
Lay, D.C.: Linear algebra and its applications. Univ. of Maryland-College Park (2003)
Büchi, J.R.: On a decision method in restricted second order arithmetic. In: The Collected Works of J. Richard Büchi, pp. 425–435. Springer (1990)
Luenberger, D.G.: Linear and nonlinear programming. Springer (2003)
Alur, R., Brayton, R.K., Henzinger, T.A., Qadeer, S., Rajamani, S.K.: Partial-order reduction in symbolic state space exploration. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 340–351. Springer, Heidelberg (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Zhang, L., Meng, Q., Luo, G. (2014). Model Checking (k, d)-Markov Chain with ipLTL. In: Buchmann, R., Kifor, C.V., Yu, J. (eds) Knowledge Science, Engineering and Management. KSEM 2014. Lecture Notes in Computer Science(), vol 8793. Springer, Cham. https://doi.org/10.1007/978-3-319-12096-6_25
Download citation
DOI: https://doi.org/10.1007/978-3-319-12096-6_25
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-12095-9
Online ISBN: 978-3-319-12096-6
eBook Packages: Computer ScienceComputer Science (R0)