Model checking meets performance evaluation

ABSTRACT

Markov chains are one of the most popular models for the evaluation of performance and dependability of information processing systems. To obtain performance measures, typically long-run or transient state probabilities of Markov chains are determined. Sometimes the Markov chain at hand is equipped with rewards and computations involve determining long-run or instantaneous reward probabilities.This note summarises a technique to determine performance and dependability guarantees of Markov chains. Given a precise description of the desired guarantee, all states in the Markov chain are determined that surely meet the guarantee. This is done in a fully automated way. Guarantees are described using logics. The use of logics yields an expressive framework that allows to express well-known measures, but also (new) intricate and complex performance guarantees. The power of this technique is that no matter how complex the logical guarantee, it is automatically checked which states in the Markov chain satisfy it. Neither manual manipulations of Markov chains (or their high-level descriptions) are needed, nor the knowledge of any numerical technique to analyze them efficiently. This applies to any (time-homogeneous) Markov chain of any structure specified in any high-level formalism.

REFERENCES

• 1: S. Andova, H. Hermanns and J.-P. Katoen. Discrete-time rewards model-checked. Formal Methods for Timed Systems, LNCS 2791: 88--104, 2003.
• 2: Adnan Aziz , Kumud Sanwal , Vigyan Singhal , Robert Brayton, Model-checking continuous-time Markov chains, ACM Transactions on Computational Logic (TOCL), v.1 n.1, p.162-170, July 2000 [doi>10.1145/343369.343402]
• 3: Christel Baier , Lucia Cloth , Boudewijn Haverkort , Matthias Kuntz , Markus Siegle, Model Checking Action- and State-Labelled Markov Chains, Proceedings of the 2004 International Conference on Dependable Systems and Networks (DSN'04), p.701, June 28-July 01, 2004
• 4: Christel Baier , Bettina Engelen , Mila Majster-Cederbaum, Deciding bisimilarity and similarity for probabilistic processes, Journal of Computer and System Sciences, v.60 n.1, p.187-231, Feb. 2000 [doi>10.1006/jcss.1999.1683]
• 5: Christel Baier , Boudewijn R. Haverkort , Holger Hermanns , Joost-Pieter Katoen, On the Logical Characterisation of Performability Properties, Proceedings of the 27th International Colloquium on Automata, Languages and Programming, p.780-792, July 09-15, 2000
• 6: C. Baier, B. R. Haverkort, H. Hermanns, and J.-P. Katoen. Model-checking algorithms for continuous-time Markov chains. IEEE Trans. on Softw. Eng.,29(6): 524--541, 2003.
• 7: C. Baier, B. R. Haverkort, H. Hermanns, and J.-P. Katoen. Efficient computation of maximal timed reachability probabilities in uniform continuous-time Markov decision processes. Tools and Algorithms for the Construction and Analysis of Systems, LNCS 2988: 61--76, 2004.
• 8: Christel Baier , Holger Hermanns , Joost-Pieter Katoen, Probabilistic weak simulation is decidable in polynomial time, Information Processing Letters, v.89 n.3, p.123-130, 14 February 2004 [doi>10.1016/j.ipl.2003.10.001]
• 9: C. Baier, H. Hermanns, J.-P. Katoen and V. Wolf. Comparative branching-time semantics for Markov chains. Concurrency Theory, LNCS 2761, pp. 492--508, 2003.
• 10: Christel Baier , Joost-Pieter Katoen , Holger Hermanns, Approximate Symbolic Model Checking of Continuous-Time Markov Chains, Proceedings of the 10th International Conference on Concurrency Theory, p.146-161, August 24-27, 1999
• 11: Christel Baier , Marta Kwiatkowska, Model checking for a probabilistic branching time logic with fairness, Distributed Computing, v.11 n.3, p.125-155, August 1998 [doi>10.1007/s004460050046]
• 12: P. Buchholz, J.-P. Katoen, P. Kemper, and C. Tepper. Model-checking large structured Markov chains. J. of Logic and Alg. Progr.,56:69--97, 2003.
• 13: G. Ciardo, A. S. Miner. SMART. Stochastic model checking analyzer for reliability and timing. http://www.cs.ucr.edu/~ciardo/SMART/
• 14: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 15: L. Cloth, J.-P. Katoen, M. Khattri and R. Pulungan. Model-checking Markov reward models with impulse rewards. accepted for IEEE Dependable Systems and Networks, 2005.
• 16: D. D'Aprile, S. Donatelli and J. Sproston. CSL model checking for the GreatSPN tool. Int. Symp. on Computer and Information Sciences, LNCS 3280: 543--552, 2004.
• 17: Salem Derisavi , Holger Hermanns , William H. Sanders, Optimal state-space lumping in Markov chains, Information Processing Letters, v.87 n.6, p.309-315, 30 September 2003 [doi>10.1016/S0020-0190(03)00343-0]
• 18: J. Desharnais and P. Panangaden. Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes. J. of Logic and Alg. Progr.,56(1--2): 99--115, 2003.
• 19: H. A. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Form. Asp. of Comp.6(5), (1994) 512--535.
• 20: Boudewijn R. Haverkort , Lucia Cloth , Holger Hermanns , Joost-Pieter Katoen, Model Checking Performability Properties, Proceedings of the 2002 International Conference on Dependable Systems and Networks, p.103-112, June 23-26, 2002
• 21: H. Hermanns, J.-P. Katoen, J. Meyer-Kayser and M. Siegle. A tool for model checking Markov chains. J. on Software Tools for Technology Transfer,4(2):153--172, 2003.
• 22: Gabriel G. Infante López , Holger Hermanns , Joost-Pieter Katoen, Beyond Memoryless Distributions: Model Checking Semi-Markov Chains, Proceedings of the Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification, p.57-70, September 12-14, 2001
• 23: Marta Kwiatkowska , Gethin Norman , David Parker, Probabilistic symbolic model checking with PRISM: a hybrid approach, International Journal on Software Tools for Technology Transfer (STTT), v.6 n.2, p.128-142, August 2004 [doi>10.1007/s10009-004-0140-2]
• 24: Marta Kwiatkowska , Gethin Norman , David Parker, Probabilistic model checking in practice: case studies with PRISM, ACM SIGMETRICS Performance Evaluation Review, v.32 n.4, p.16-21, March 2005 [doi>10.1145/1059816.1059820]
• 25: Kim G. Larsen , Arne Skou, Bisimulation through probabilistic testing, Information and Computation, v.94 n.1, p.1-28, Sept. 1991 [doi>10.1016/0890-5401(91)90030-6]
• 26: K. Sen, M. Viswanathan and G. Agha. Statistical model checking of black-box probabilistic systems. Computer-Aided Verification, LNCS 3114: 202--215, 2004.
• 27: A. Remke, L. Cloth and B. R. Haverkort. Model-checking infinite-state Markov chains. Tools and Algorithms for the Construction and Analysis of Systems, LNCS 3440: 237--252, 2005.
• 28: Håkan L. S. Younes , Reid G. Simmons, Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling, Proceedings of the 14th International Conference on Computer Aided Verification, p.223-235, July 27-31, 2002

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

Additional Classification:
  G. Mathematics of Computing
  G.3 PROBABILITY AND STATISTICS
      Subjects: Markov processes

  H. Information Systems
  H.1 MODELS AND PRINCIPLES
      H.1.1 Systems and Information Theory
          Subjects: Value of information

General Terms:
Algorithms, Measurement, Theory