This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Verifying the Evolution of Probability Distributions Governed by a DTMC
January/February 2011 (vol. 37 no. 1)
pp. 126-141
YoungMin Kwon, Microsoft Corporation, Redmond
Gul Agha, University of Illinois at Urbana-Champaign, Urbana
We propose a new probabilistic temporal logic, iLTL, which captures properties of systems whose state can be represented by probability mass functions (pmfs). Using iLTL, we can specify reachability to a state (i.e., a pmf), as well as properties representing the aggregate (expected) behavior of a system. We then consider a class of systems whose transitions are governed by a Markov Chain—in this case, the set of states a system may be in is specified by the transitions of pmfs from all potential initial states to the final state. We then provide a model checking algorithm to check iLTL properties of such systems. Unlike existing model checking techniques, which either compute the portions of the computational paths that satisfy a specification or evaluate properties along a single path of pmf transitions, our model checking technique enables us to do a complete analysis on the expected behaviors of large-scale systems. Desirable system parameters may also be found as a counterexample of a negated goal. Finally, we illustrate the usefulness of iLTL model checking by means of two examples: assessing software reliability and ensuring the results of administering a drug.

[1] iLTLChecker: http://osl.cs.uiuc.edu/~ykwon4/cgiiLTL.html , 2010.
[2] A. Aziz, K. Sanwal, V. Singhal, and R. Brayton, "Verifying Continuous Time Markov Chains," Proc. Eighth Int'l Conf. Computer Aided Verification, pp. 269-276, 1996.
[3] A. Aziz, V. Singhal, and F. Balarin, "It Usually Works: The Temporal Logic of Stochastic Systems," Proc. Seventh Int'l Conf. Computer Aided Verification, pp. 155-165, 1995.
[4] C. Baier, J. Katoen, and H. Hermanns, "Approximate Symbolic Model Checking of Continuous-Time Markov Chains," Proc. 10th Int'l Conf. Concurrency Theory, pp. 146-162, 1999.
[5] B.A. Berg, Markov Chain Monte Carlo Simulation and Their Statistical Analysis. World Scientific Publishing Company, 2004.
[6] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu, "Symbolic Model Checking Without BDDs," Proc. Fifth Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 193-207, 1999.
[7] J. Büchi, "On a Decision Method in Restricted Second Order Arithmetic," Proc. Int'l Conf. Logic, Methodology and Philosophy of Science, pp. 1-11, 1960.
[8] P. Bucholz, "Exact and Ordinary Lumpability in Finite Markov Chains," J. Applied Probability, vol. 31, pp. 59-74, 1994.
[9] M. Calder, A. Duguid, S. Gilmore, and J. Hillston, "Stronger Computational Modelling of Signalling Pathways Using Both Continuous and Discrete-State Methods," Computational Methods in Systems Biology, pp. 63-77, Springer-Verlag, 2006.
[10] G. Ciardo, R.A. Marie, B. Sericola, and K.S. Trivedi, "Performability Analysis Using Semi-Markov Reward Process," IEEE Trans. Computers, vol. 39, no. 10, pp. 1251-1264, Oct. 1990.
[11] G. Ciardo and A.S. Miner, "A Data Structure for the Efficient Kronecker Solution of GSPNs," Proc. Int'l Workshop Petri Nets and Performance Models, pp. 22-31, 1999.
[12] E. Clarke and E. Emerson, "Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic," Proc. Workshop Logic of Programs, 1981.
[13] E. Clarke, E. Emerson, and A. Sistla, "Automatic Verification of Finite-State Concurrent Systems Using Temporal Logics Specification: A Practical Approach," Proc. 10th Int'l ACM Symp. Principles of Programming Languages, pp. 117-126, 1983.
[14] E. Clarke, O. Grumberg, and D. Peled, Model Checking. MIT Press, 2000.
[15] R. Grosu, E. Bartocci, F. Corradini, E. Entcheva, S. Smolka, and A. Wasilewska, "Learning and Detecting Emergent Behavior in Networks of Cardiac Myocytes," Hybrid Systems: Computation and Control, pp. 229-243, Springer-Verlag, 2008.
[16] H. Hansson and B. Jonsson, "A Logic for Reasoning about Time and Reliability," Formal Aspects of Computing, vol. 6, pp. 512-535, 1994.
[17] G.J. Holzmann, "The Model Checker Spin," IEEE Trans. Software Eng., vol. 23, no. 5, pp. 279-295, May 1997.
[18] G. Hughes and M. Creswell, Introduction to Modal Logic. Methuen, 1997.
[19] J.G. Kemeny and J.L. Snell, Finite Markov Chains. Springer-Verlag, 1976.
[20] M. Kwiatkowska, G. Norman, and D. Parker, "Prism 2.0: A Tool for Probabilistic Model Checking," Proc. Int'l Conf. Quantitative Evaluation of Systems, pp. 322-323, 2004.
[21] Y. Kwon and G. Agha, "Linear Inequality LTL (iLTL): A Model Checker for Discrete Time Markov Chains," Proc. Int'l Conf. Formal Eng. Methods, pp. 194-208, 2004.
[22] Y. Kwon and G. Agha, "iLTLChecker: A Probabilistic Model Checker for Multiple DTMCs," Proc. Int'l Conf. Quantitative Evaluation of Systems, 2005.
[23] Y. Kwon and G. Agha, "Scalable Modeling and Performance Evaluation of Wireless Sensor Networks," Proc. IEEE Real-Time and Embedded Technology and Applications Symp., 2006.
[24] Y. Kwon and G. Agha, "A Markov Reward Model for Software Reliability," Proc. Next Generation Software Workshop at the IEEE Int'l Parallel and Distributed Processing Symp., pp. 1-6, 2007.
[25] Y. Kwon and G. Agha, "LTLC: Linear Temporal Logic for Control," Hybrid Systems: Computation and Control, pp. 316-329, Springer-Verlag, 2008.
[26] V.V. Lam, P. Buchholz, and W.H. Sanders, "A Structured Path-Based Approach for Computing Transient Rewards for Large CTMCs," Proc. Int'l Conf. Quantitative Evaluation of Systems, pp. 136-145, 2004.
[27] O. Lichtenstein and A. Pnueli, "Checking That Finite State Concurrent Programs Satisfy Their Linear Specification," Proc. 12th ACM Symp. Principles of Programming Languages, pp. 97-107, 1985.
[28] D.G. Luenberger, Linear and Nonlinear Programming, second ed., Addison Wesley, 1989.
[29] J. Martyna, "Performance Modeling of Mobile Sensor Networks," Ad-Hoc, Mobile, and Wireless Networks, pp. 262-272, Springer-Verlag, 2007.
[30] A.S. Miner and G. Ciardo, "Efficient Reachability Set Generation and Storage Using Decision Diagrams," Proc. Int'l Conf. Application and Theory of Petri Nets, pp. 6-25, 1999.
[31] A. Papoulis, Probability, Random Variables, and Stochastic Processes, third ed. McGraw-Hill, 1991.
[32] H. Pham, Software Reliability. Springer, 2000.
[33] J. Rajgopal and M. Mazumdar, "Modular Operational Test Plans for Inference on Software Reliability Based on a Markov Model," IEEE Trans. Software Eng., vol. 28, no. 4, pp. 358-363, Apr. 2002.
[34] D.M. Roberts and N.A. Buckley, "Pharmacokinetic Considerations in Clinical Toxicology," Clinical Pharmacokinetics, vol. 46, pp. 897-939, 2007.
[35] L. Shargel and A.B.C. Yu, Applied Biopharmaceutics and Pharmacokinetics. Appleton-Century-Crofts, 1985.
[36] H. Start and J.W. Woods, Probability and Random Processes with Applications to Signal Processing, third ed., Prentice-Hall, 2002.
[37] G. Strang, Linear Algebra and Its Applications, third ed., Harcourt Brace Jova novich, 1988.
[38] A.S. Tanenbaum, Computer Networks, fourth ed., Prentice Hall, 2003.
[39] S.M. Yacoub, B. Cukic, and H.H. Ammar, "Scenario-Based Reliability Analysis of Component-Based Software," Proc. 10th Int'l Symp. Software Reliability Eng., pp. 22-31, 1999.

Index Terms:
Probabilistic model checking, linear temporal logic, Discrete Time Markov Chain, pharmacokinetics.
Citation:
YoungMin Kwon, Gul Agha, "Verifying the Evolution of Probability Distributions Governed by a DTMC," IEEE Transactions on Software Engineering, vol. 37, no. 1, pp. 126-141, Jan.-Feb. 2011, doi:10.1109/TSE.2010.80
Usage of this product signifies your acceptance of the Terms of Use.