Counterexamples for Timed Probabilistic Reachability

  • Husain Aljazzar
  • Holger Hermanns
  • Stefan Leue
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3829)


The inability to provide counterexamples for the violation of timed probabilistic reachability properties constrains the practical use of CSL model checking for continuous time Markov chains (CTMCs). Counterexamples are essential tools in determining the causes of property violations and are required during debugging. We propose the use of explicit state model checking to determine runs leading into property offending states. Since we are interested in finding paths that carry large amounts of probability mass we employ directed explicit state model checking technology to find such runs using a variety of heuristics guided search algorithms, such as Best First search and Z*. The estimates used in computing the heuristics rely on a uniformisation of the CTMC. We apply our approach to a probabilistic model of the SCSI-2 protocol.


Model Check Goal State Atomic Proposition Label Transition System Traversal Tree 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999) (third printing 2001)Google Scholar
  2. 2.
    Bianco, A., de Alfaro, L.: Model checking of probabalistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499–513. Springer, Heidelberg (1995)Google Scholar
  3. 3.
    Aziz, A., Sanwal, K., Singhal, V., Brayton, R.K.: Verifying continuous-time Markov chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 269–276. Springer, Heidelberg (1996)Google Scholar
  4. 4.
    de Alfaro, L.: Formal Verification of Probabilistic Systems. Ph.d. dissertation, Stanford University (1997)Google Scholar
  5. 5.
    Baier, C.: On algorithmic verification methods for probabilistic systems. Habilitation Thesis. Habilitation thesis, University of Mannheim (1998)Google Scholar
  6. 6.
    Baier, C., Katoen, J.P., Hermanns, H.: Approximate symbolic model checking of continuous-time Markov chains. In: International Conference on Concurrency Theory. LNCS, pp. 146–161. Springer, Heidelberg (1999)Google Scholar
  7. 7.
    Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model-checking Continuous-Time Markov Chains. ACM Transactions on Computational Logic 1, 162–170 (2000)CrossRefMathSciNetGoogle Scholar
  8. 8.
    Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.P.: Model checking continuous-time Markov chains by transient analysis. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 358–372. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  9. 9.
    Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Model-checking algorithms for continuous-time Markov chains. IEEE Transions on Software Engineering 29 (2003)Google Scholar
  10. 10.
    Garavel, H., Lang, F., Mateescu, R.: An overview of CADP 2001. European Association for Software Science and Technology (EASST) Newsletter 4 (2002)Google Scholar
  11. 11.
    Hermanns, H., Joubert, C.: A set of performance and dependability analysis components for CADP. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 425–430. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  12. 12.
    Edelkamp, S., Lafuente, A.L., Leue, S.: Directed explicit-state model checking in the validation of communication protocols. Software Tools for Technology Transfer 5, 247–267 (2004)CrossRefGoogle Scholar
  13. 13.
    Dijkstra, E.W.: A note on two problems in connexion with graphs. Numerische Mathematik 1, 269–271 (1959)zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    Pearl, J.: Heuristics – Intelligent Search Strategies for Computer Problem Solving. Addision-Wesley, Reading (1986)Google Scholar
  15. 15.
    (ANSI), A.N.S.I.: Small computer interface-2 – standard x3.131-1994 (1994)Google Scholar
  16. 16.
    Garavel, H., Hermanns, H.: On combining functional verification and performance evaluation using CADP. In: Proceedings of the International Symposium of Formal Methods Europe on Formal Methods - Getting IT Right. LNCS, pp. 410–429. Springer, Heidelberg (2002)Google Scholar
  17. 17.
    ISO/IEC: LOTOS – a formal description technique based on temporal ordering of observational behaviour (1989)Google Scholar
  18. 18.
    Garavel, H.: OPEN/CÆSAR: An open software architecture for verification, simulation, and testing. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 68–84. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  19. 19.
    Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addision-Wesley, Reading (2003)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Husain Aljazzar
    • 1
  • Holger Hermanns
    • 2
  • Stefan Leue
    • 1
  1. 1.Department of Computer and Information ScienceUniversity of KonstanzGermany
  2. 2.Department of Computer ScienceSaarland UniversityGermany

Personalised recommendations