Subscribe

Issue No.01 - January/February (2011 vol.37)

pp: 126-141

YoungMin Kwon , Microsoft Corporation, Redmond

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2010.80

ABSTRACT

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.

INDEX TERMS

Probabilistic model checking, linear temporal logic, Discrete Time Markov Chain, pharmacokinetics.

CITATION

YoungMin Kwon, "Verifying the Evolution of Probability Distributions Governed by a DTMC",

*IEEE Transactions on Software Engineering*, vol.37, no. 1, pp. 126-141, January/February 2011, doi:10.1109/TSE.2010.80REFERENCES

- [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. |