Abstract
Checking that a given finite state program satisfies a linear temporal logic property suffers from the state explosion problem. Often the resulting lack of available memory is more significant than any time limitations. 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. Especially in conjunction with known partial order reduction algorithms, we show a substantial reduction in memory over using partial order methods alone, both in the precomputation stage, and in the result presented to a model checker. The price of the space reduction is 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.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
D. Dolev, M. Klawe, and M. Rodeh, “An O(n log n) unidirectional distributed algorithm for extrema finding in a circle,” Journal of Algorithms, Vol. 3, pp. 245–260, 1992.
P. Godefroid, G.J. Holzmann, and D. Pirottin, “State space caching revisited.” in Proc. 6th International Conference on Computer Aided Verification, LNCS 697, Canada, pp. 178–191, June 1992.
P. Godefroid and P. Wolper, “A partial order approach to model checking,” in Proc. of the 6th Symposium on Logic in Computer Science, Amsterdam, pp. 406–415, July 1991.
G.J. Holzmann, “An improved protocol reachability analysis technique,” Software-Practice and Experience, Vol. 18,No. 2, pp. 137–161, 1988.
G.J. Holzmann, Design and Validation of Computer Protocols, Prentice Hall, 1991.
G.J. Holzmann and D. Peled, “An improvement in formal verification,” in Proc. FORTE 1994 Conference, Switzerland, Oct. 1994.
S. Katz and D. Peled, “Conditional independence using collapses,” Theoretical Computer Science, Vol. 101, pp. 337–359, 1992.
H. Krumm, “Projections of the reachability graph and environments models,” in Proc. 1st International Workshop on Automatic Verification Methods for Finite State Systems, LNCS 407, France, pp. 89–96, June 1989.
L. Lamport, “What good is temporal logic?” in Proc. IFIP 9th World Congress, Paris, pp. 657–668, 1983.
O. Lichtenstein and A. Pnueli, “Checking that finite state concurrent programs satisfy their linear specification,” in Proc. of the Twelfth ACM Symposium on Principles of Programming Languages, New Orleans, pp. 97–107, Jan. 1985.
Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems, Springer-Verlag, 1992.
D. Peled, “Combining partial order reductions with on-the-fly model checking,” Formal Methods in System Design, Vol. 8, pp. 39–64, 1996.
A. Valmari, “A stubborn attack on state explosion,” Formal Methods in System Design, Vol. 1, pp. 297–322, 1992.
M. Vardi and P. Wolper, “An automata-theoretic approach to automatic program verification,” in Proc. of the First Symposium on Logic in Computer Science, Cambridge, pp. 322–331, June 1986.
P. Wolper and D. Leroy, “Reliable hashing without collision detection,” in Proc. 5th International Conference on Computer Aided Verification, LNCS 697, Greece, pp. 59–70, June 1993.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Katz, S., Miller, H. Saving Space by Fully Exploiting Invisible Transitions. Formal Methods in System Design 14, 311–332 (1999). https://doi.org/10.1023/A:1008775109219
Issue Date:
DOI: https://doi.org/10.1023/A:1008775109219