
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Jeremy Sproston, Susanna Donatelli, "Backward Bisimulation in Markov Chain Model Checking," IEEE Transactions on Software Engineering, vol. 32, no. 8, pp. 531546, August, 2006.  
BibTex  x  
@article{ 10.1109/TSE.2006.74, author = {Jeremy Sproston and Susanna Donatelli}, title = {Backward Bisimulation in Markov Chain Model Checking}, journal ={IEEE Transactions on Software Engineering}, volume = {32}, number = {8}, issn = {00985589}, year = {2006}, pages = {531546}, doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2006.74}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Backward Bisimulation in Markov Chain Model Checking IS  8 SN  00985589 SP531 EP546 EPD  531546 A1  Jeremy Sproston, A1  Susanna Donatelli, PY  2006 KW  Markov processes KW  model checking KW  temporal logic KW  verification. VL  32 JA  IEEE Transactions on Software Engineering ER   
[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. SangiovanniVincentelli, “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, “ModelChecking Continuous Time Markov Chains,” ACM Trans. Computational Logic, vol. 1, no. 1, pp. 162170 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. 115131, 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. 154, 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, “ModelChecking Algorithms for ContinuousTime Markov Chains,” IEEE Trans. Software Eng., vol. 29, no. 6, pp. 524541, June 2003.
[10] C. Baier, H. Hermanns, J.P. Katoen, and V. Wolf, “Comparative BranchingTime Semantics for Markov Chains,” Information and Computation, vol. 200, no. 2, pp. 149214, 2005.
[11] J.T. Bradley, N.J. Dingle, P.G. Harrison, and W.J. Knottenbelt, “Performance Queries on SemiMarkov Stochastic Petri Nets with an Extended Continuous Stochastic Logic,” Proc. 10th Int'l Workshop Petri Nets and Performance Models (PNPM '03), pp. 6271, 2003.
[12] P. Buchholz, “Exact and Ordinary Lumpability in Finite Markov Chains,” J. Applied Probability, vol. 31, pp. 5974, 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. 12, pp. 263287, 1999.
[15] G. Chiola, C. Dutheillet, G. Franceschinis, and S. Haddad, “Stochastic WellFormed Coloured Nets for Symmetric Modeling Applications,” IEEE Trans. Computers, vol. 42, no. 11, pp. 13431360, 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 TimeCritical 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. 410425, 2000.
[18] E.M. Clarke, E.A. Emerson, and A.P. Sistla, “Automatic Verification of FiniteState Concurrent Systems Using Temporal Logic Specifications,” ACM Trans. Programming Languages and Systems, vol. 8, no. 2, pp. 244263, 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. 857907, 1995.
[22] S. Derisavi, H. Hermanns, and W. Sanders, “Optimal StateSpace Lumping in Markov Chains,” Information Processing Letters, vol. 87, no. 6, pp. 309315, 2003.
[23] J. Desharnais and P. Panangaden, “Continuous Stochastic Logic Characterizes Bisimulation of ContinuousTime Markov Processes,” J. Logic and Algebraic Programming, vol. 56, nos. 12, pp.99115, 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. 910, pp. 901924, 1998.
[25] H. Hermanns, J.P. Katoen, J. MeyerKayser, and M. Siegle, “A Tool for ModelChecking Markov Chains,” Software Tools for Technology Transfer, vol. 4, no. 2, pp. 153172, 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. 512535, 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. 303327, 2003.
[29] G.J. Holzmann, “The Model Checker SPIN,” IEEE Trans. Software Eng., vol. 23, no. 5, pp. 279295, 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. 322323, 2004.
[32] P. Kanellakis and S. Smolka, “CCS Expressions, Finite State Processes, and Three Problems of Equivalence,” Information and Computation, vol. 86, pp. 4368, 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. 214233, 1995.
[35] A. Pnueli, “The Temporal Logic of Programs,” Proc. 18th Ann. Symp. Foundations of Computer Science (FOCS '77), pp. 4657, 1977.
[36] P.J. Schweitzer, “Aggregation Methods for Large Markov Chains,” Math. Computer Performance and Reliability, pp. 275302, 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. 220229, 2004.
[38] M. Vardi, “Automatic Verification of Probabilistic Concurrent FiniteState Programs,” Proc. 16th Ann. Symp. Foundations of Computer Science (FOCS '85), pp. 327338, 1985.