Abstract
Checking that a given finite state program satisfies a linear temporal logic property suffers from a severe space and time explosion. One way to cope with this is to reduce the state graph used for model checking. We present an algorithm for constructing a state graph that is a projection of the program's state graph. The algorithm maintains the transitions and states that affect the truth of the property to be checked. The algorithm works in conjunction with a partial order reduction algorithm. We show a substantial reduction in memory over current partial order reduction methods, both in the precomputation stage, and in the result presented to a model checker, with a price of a single additional traversal of the graph obtained with partial order reduction. As part of our space-saving methods, we present a new way to exploit Holzmann's Bit Hash Table, which assists us in solving the revisiting problem.
Supported by the Technion V.P.R. Fund-Promotion of Sponsored Research
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
D. Dolev, M. Klawe and M. Rodeh. An O(nlogn) unidirectional distributed algorithm for extrema finding in a circle. Journal of Algorithms, volume 3, pages 245–260, 1992.
P. Godefroid, G.J Holzman and D. Pirottin. State space caching revisited. In Proc. 4th International Conference on Computer Aided Verification, LNCS 697, pages 178–191, Canada, June 1992.
P.Godefroid and P.Wolper. A partial order approach to model checking. In Proc. 6th Symposium on Logic in Computer Science, pages 406–415, Amsterdam, July 91.
G.J. Holzmann. An improved protocol peachability analysis technique. Software-Practice and Experience, Vol 18(2), pages 137–161,February 1988.
G.J. Holzmann and D. Peled. An improvement in formal verification. In Proceedings FORTE 1994 Conference, Switzerland, October 1994.
S. Katz and D. Peled. Conditional independence using collapses. Theoretical Computer Science, volume 101, pages 337–359, 1992.
L. Lamport, What good is temporal logic? in: Proc. IFIP 9th World Congress, Paris, France (1983) 657–668.
D. Peled. Combining partial order reductions with on-the-fly model checking. In Proc. 6th International Conference on Computer Aided Verification, LNCS 818, pages 377–390, California, USA, June 1994.
A. Valmari. A stubborn attack on state explosion. Formal methods in System Design 1, pages 297–322, 1992.
M. Vardi and P.Wolper. An automata-theoretic approach to automatic program verification. In Proc. 1st Symposium on Logic in Computer Science, pages 322–331, Cambridge, June 1986.
Author information
Authors and Affiliations
Corresponding author
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Miller, H., Katz, S. (1996). Saving space by fully exploiting invisible transitions. In: Alur, R., Henzinger, T.A. (eds) Computer Aided Verification. CAV 1996. Lecture Notes in Computer Science, vol 1102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61474-5_81
Download citation
DOI: https://doi.org/10.1007/3-540-61474-5_81
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61474-6
Online ISBN: 978-3-540-68599-9
eBook Packages: Springer Book Archive