Randomization Helps in LTL Model Checking

  • Luboš Brim
  • Ivana Černá
  • Martin Nečesal
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2165)


We present and analyze a new probabilistic methodfor automata basedL TL model checking of non-probabilistic systems with intention to reduce memory requirements. The main idea of our approach is to use randomness to decide which of the needed information (visited states) should be storedd uring a computation and which could beomitted. We propose two strategies of probabilistic storing of states. The algorithm never errs, i.e. it always delivers correct results. On the other hand the computation time can increase. The methodhas been embedded into the SPIN model checker and a series of experiments has been performed. The results confirm that randomization can help to increase the applicability of model checkers in practice.


Model Check Reduction Strategy Linear Temporal Logic Kripke Structure Dynamic Strategy 
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.
    C. Baier and M. Kwiatkowska. Model Checking for a Probabilistic Branching Time Logic with Fairness. DISTCOMP: Distributed Computing, 11, 1998.Google Scholar
  2. 2.
    A. Bianco and L. De Alfaro. Model Checking of Probabilistic and Nondeterministic Systems. In P. S. Thiagarajan, editor, Foundations of Software Technology and Theoretical Computer Science (FSTTCS), volume 1026 of LNCS, pages 499–513. Springer-Verlag, 1995.Google Scholar
  3. 3.
    C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis. Memory-Efficient Algorithms for the Verification of Temporal Properties. Formal Methods in System Design, 1:275–288, 1992.CrossRefGoogle Scholar
  4. 4.
    C. Courcoubetis and M. Yannakakis. The Complexity of Probabilistic Verification. Journal of the ACM, 42(4):857–907, July 1995.zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    P. Godefroid, G. J. Holzmann, and D. Pirottin. State-Space Caching Revisited. Formal Methods in System Design: An International Journal, 7(3):227–241, November 1995.CrossRefGoogle Scholar
  6. 6.
    G. J. Holzmann. An Analysis of Bitstate Hashing. Formal Methods in System Design: An International Journal, 13(3):289–307, Nov. 1998.CrossRefMathSciNetGoogle Scholar
  7. 7.
    G.J. Holzmann, D. Peled, and M. Yannakakis. On NestedDepth First Search. In The SPIN Verification System, pages 23–32. American Mathematical Society, 1996. Proc. of the Second SPIN Workshop.Google Scholar
  8. 8.
    M. Narasimha, R. Cleaveland, and P. Iyer. Probabilistic Temporal Logics via the Modal Mu-Calculus. In W. Thomas, editor, Proceedings of the Second International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), volume 1578 of LNCS, pages 288–305. Springer-Verlag, 1999.CrossRefGoogle Scholar
  9. 9.
    U. Stern and D.L. Dill. Combining State Space Caching and Hash Compaction. In B. Straube and J. Schoenherr, editors, 4. GI/ITG/GME Workshop zur Methoden des Entwurfs und der Verifikation Digitaler Systeme, pages 81–90. Shaker Verlag, Aachen, 1996.Google Scholar
  10. 10.
    R. Tarjan. Depth First Search and Linear Graph Algorithms. SIAM journal on computing, pages 146–160, Januar 1972.Google Scholar
  11. 11.
    M. Vardi. Probabilistic Linear-Time Model Checking: An Overview of the Automata-Theoretic Approach. In J.-P. Katoen, editor, International AMAST Workshop on Formal Methods for Real-Time and Probabilistic Systems (ARTS), volume 1601 of LNCS, pages 265–276. Springer-Verlag, 1999.CrossRefGoogle Scholar
  12. 12.
    W. Visser. Using OBDD Encodings for Space Efficient State Storage during On-the-fly Model Checking. Proceedings of the 1st SPIN Workshop, Montreal, Canada, 1995.Google Scholar
  13. 13.
    A. K. Wisspeintner, F. Huber, and J. Philipps. Model Checking and Random Competition — A Study Using the Model Checking Framework MIC. 10. GI/ITG Fachgespräch “Formale Beschreibungstechniken für verteilte Systeme”, pages 91–100, June 2000.Google Scholar
  14. 14.
    P. Wolper and D. Leroy. Reliable Hashing Without Collision Detection. In C. Courcoubetis, editor, Proc. 5th International Computer Aided Veri.cation Conference (CAV’93), volume 697 of LNCS, pages 59–70. Springer-Verlag, 1993.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Luboš Brim
    • 1
  • Ivana Černá
    • 1
  • Martin Nečesal
    • 1
  1. 1.Department of Computer Science, Faculty of InformaticsMasaryk University BrnoCzech Republic

Personalised recommendations