Abstract
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.
This work has been partially supported by the Grant Agency of Czech Republic grants No. 201/00/1023 and 201/00/0400.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
C. Baier and M. Kwiatkowska. Model Checking for a Probabilistic Branching Time Logic with Fairness. DISTCOMP: Distributed Computing, 11, 1998.
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.
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.
C. Courcoubetis and M. Yannakakis. The Complexity of Probabilistic Verification. Journal of the ACM, 42(4):857–907, July 1995.
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.
G. J. Holzmann. An Analysis of Bitstate Hashing. Formal Methods in System Design: An International Journal, 13(3):289–307, Nov. 1998.
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.
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.
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.
R. Tarjan. Depth First Search and Linear Graph Algorithms. SIAM journal on computing, pages 146–160, Januar 1972.
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.
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.
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.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brim, L., Černá, I., Nečesal, M. (2001). Randomization Helps in LTL Model Checking. In: de Alfaro, L., Gilmore, S. (eds) Process Algebra and Probabilistic Methods. Performance Modelling and Verification. PAPM-PROBMIV 2001. Lecture Notes in Computer Science, vol 2165. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44804-7_7
Download citation
DOI: https://doi.org/10.1007/3-540-44804-7_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42556-4
Online ISBN: 978-3-540-44804-4
eBook Packages: Springer Book Archive