This Article 
 Bibliographic References 
 Add to: 
Backward Bisimulation in Markov Chain Model Checking
August 2006 (vol. 32 no. 8)
pp. 531-546
Susanna Donatelli, IEEE Computer Society
Equivalence relations can be used to reduce the state space of a system model, thereby permitting more efficient analysis. We study backward stochastic bisimulation in the context of model checking continuous-time Markov chains against Continuous Stochastic Logic (Csl) properties. While there are simple Csl properties that are not preserved when reducing the state space of a continuous-time Markov chain using backward stochastic bisimulation, we show that the equivalence can nevertheless be used in the verification of a practically significant class of Csl properties. We consider an extension of these results to Markov reward models and Continuous Stochastic Reward Logic. Furthermore, we identify the logical properties for which the requirement on the equality of state-labeling sets (normally imposed on state equivalences in a model-checking context) can be omitted from the definition of the equivalence, resulting in a better state-space reduction.

[1] M.A. Marsan, G. Balbo, G. Conte, S. Donatelli, and G. Franceschinis, Modeling with Generalized Stochastic Petri Nets. John Wiley and Sons, 1995.
[2] A. Aziz, V. Singhal, F. Balarin, R.K. Brayton, and A.L. Sangiovanni-Vincentelli, “It Usually Works: The Temporal Logic of Stochastic Systems,” Proc. Seventh Int'l Conf. Computer Aided Verification (CAV '95), 1995.
[3] A. Aziz, K. Sanwal, V. Singhal, and R. Brayton, “Model-Checking Continuous Time Markov Chains,” ACM Trans. Computational Logic, vol. 1, no. 1, pp. 162-170 2000.
[4] P. Ballarini, “Towards Compositional CSL Model Checking,” PhD thesis, Dipartimento di Informatica, Univ. di Torino, 2004.
[5] M.C. Browne, E.M. Clarke, and O. Grumberg, “Characterizing Finite Kripke Structures in Propositional Temporal Logic,” Theoretical Computer Science, vol. 59, pp. 115-131, 1988.
[6] M. Bernardo and R. Gorrieri, “A Tutorial on EMPA: A Theory of Concurrent Processes with Nondeterminism, Priorities, Probabilities and Time,” Theoretical Computer Science, vol. 202, pp. 1-54, 1998.
[7] C. Baier, B. Haverkort, H. Hermanns, and J.-P. Katoen, “On the Logical Characterisation of Performability Properties,” Proc. 12th Int'l Colloquium on Automata, Languages and Programming (ICALP'00), 2000.
[8] C. Baier, B. Haverkort, H. Hermanns, and J.-P. Katoen, “Automated Performance and Dependability Evaluation Using Model Checking,” Performance Evaluation of Complex Systems: Techniques and Tools, 2002.
[9] C. Baier, B. Haverkort, H. Hermanns, and J.-P. Katoen, “Model-Checking Algorithms for Continuous-Time Markov Chains,” IEEE Trans. Software Eng., vol. 29, no. 6, pp. 524-541, June 2003.
[10] C. Baier, H. Hermanns, J.-P. Katoen, and V. Wolf, “Comparative Branching-Time Semantics for Markov Chains,” Information and Computation, vol. 200, no. 2, pp. 149-214, 2005.
[11] J.T. Bradley, N.J. Dingle, P.G. Harrison, and W.J. Knottenbelt, “Performance Queries on Semi-Markov Stochastic Petri Nets with an Extended Continuous Stochastic Logic,” Proc. 10th Int'l Workshop Petri Nets and Performance Models (PNPM '03), pp. 62-71, 2003.
[12] P. Buchholz, “Exact and Ordinary Lumpability in Finite Markov Chains,” J. Applied Probability, vol. 31, pp. 59-74, 1994.
[13] P. Buchholz, “On a Markovian Process Algebra,” Technical Report500, Fachbereich Informatik, Univ. of Dortmund, 1994.
[14] P. Buchholz, “Exact Performance Equivalence: An Equivalence Relation for Stochastic Automata,” Theoretical Computer Science, vol. 215, nos. 1-2, pp. 263-287, 1999.
[15] G. Chiola, C. Dutheillet, G. Franceschinis, and S. Haddad, “Stochastic Well-Formed Coloured Nets for Symmetric Modeling Applications,” IEEE Trans. Computers, vol. 42, no. 11, pp. 1343-1360, Nov. 1993.
[16] L. Capra, C. Dutheillet, G. Franceschinis, and J.-M. Ilié, “Exploiting Partial Symmetries for Markov Chain Aggregation,” Proc. First Int'l Workshop Models for Time-Critical Systems (MTCS 2000), 2000.
[17] A. Cimatti, E.M. Clarke, F. Giunchiglia, and M. Roveri, “NUSMV: A New Symbolic Model Checker,” Software Tools for Technology Transfer, vol. 2, no. 4, pp. 410-425, 2000.
[18] E.M. Clarke, E.A. Emerson, and A.P. Sistla, “Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications,” ACM Trans. Programming Languages and Systems, vol. 8, no. 2, pp. 244-263, 1986.
[19] E.M. Clarke, O. Grumberg, and D.A. Peled, Model Checking. MIT Press, 1999.
[20] T.H. Cormen, C.E. Leiserson, and R.L. Rivest, Introduction to Algorithms. MIT Press, 1990.
[21] C. Courcoubetis and M. Yannakakis, “The Complexity of Probabilistic Verification,” J. ACM, vol. 42, no. 4, pp. 857-907, 1995.
[22] S. Derisavi, H. Hermanns, and W. Sanders, “Optimal State-Space Lumping in Markov Chains,” Information Processing Letters, vol. 87, no. 6, pp. 309-315, 2003.
[23] J. Desharnais and P. Panangaden, “Continuous Stochastic Logic Characterizes Bisimulation of Continuous-Time Markov Processes,” J. Logic and Algebraic Programming, vol. 56, nos. 1-2, pp.99-115, 2003.
[24] H. Hermanns, U. Herzog, and V. Mertsiotakis, “Stochastic Process Algebras: Between LOTOS and Markov Chains,” Computer Networks and ISDN Systems, vol. 30, nos. 9-10, pp. 901-924, 1998.
[25] H. Hermanns, J.-P. Katoen, J. Meyer-Kayser, and M. Siegle, “A Tool for Model-Checking Markov Chains,” Software Tools for Technology Transfer, vol. 4, no. 2, pp. 153-172, 2003.
[26] J. Hillston, A Compositional Approach to Performance Modeling. Cambridge Univ. Press, 1996.
[27] H. Hansson and B. Jonsson, “A Logic for Reasoning about Time and Reliability,” Formal Aspects of Computing, vol. 6, no. 5, pp. 512-535, 1994.
[28] T.A. Henzinger, O. Kupferman, and S. Qadeer, “From Prehistoric to Postmodern Symbolic Model Checking,” Formal Methods in System Design, vol. 23, pp. 303-327, 2003.
[29] G.J. Holzmann, “The Model Checker SPIN,” IEEE Trans. Software Eng., vol. 23, no. 5, pp. 279-295, May 1997.
[30] R.A. Howard, Dynamic Probabilistic Systems, vols. I, II. John Wiley and Sons, 1971.
[31] M. Kwiatkowska, G. Norman, and D. Parker, “PRISM 2.0: A Tool for Probabilistic Model Checking,” Proc. First Int'l Conf. Quantitative Evaluation of Systems (QEST '04), pp. 322-323, 2004.
[32] P. Kanellakis and S. Smolka, “CCS Expressions, Finite State Processes, and Three Problems of Equivalence,” Information and Computation, vol. 86, pp. 43-68, 1990.
[33] J.G. Kemeny and J.L. Snell, Finite Markov Chains. Van Nostrand, 1960.
[34] N. Lynch and F.W. Vaandrager, “Forward and Backward Simulations Part I: Untimed Systems,” Information and Computation, vol. 121, no. 2, pp. 214-233, 1995.
[35] A. Pnueli, “The Temporal Logic of Programs,” Proc. 18th Ann. Symp. Foundations of Computer Science (FOCS '77), pp. 46-57, 1977.
[36] P.J. Schweitzer, “Aggregation Methods for Large Markov Chains,” Math. Computer Performance and Reliability, pp. 275-302, 1984.
[37] J. Sproston and S. Donatelli, “Backward Stochastic Bisimulation in CSL Model Checking,” Proc. First Int'l Conf. Quantitative Evaluation of Systems (QEST '04), pp. 220-229, 2004.
[38] M. Vardi, “Automatic Verification of Probabilistic Concurrent Finite-State Programs,” Proc. 16th Ann. Symp. Foundations of Computer Science (FOCS '85), pp. 327-338, 1985.

Index Terms:
Markov processes, model checking, temporal logic, verification.
Jeremy Sproston, Susanna Donatelli, "Backward Bisimulation in Markov Chain Model Checking," IEEE Transactions on Software Engineering, vol. 32, no. 8, pp. 531-546, Aug. 2006, doi:10.1109/TSE.2006.74
Usage of this product signifies your acceptance of the Terms of Use.