Abstract
The paper presents the LTL preserving stubborn set method for reducing the amount of work needed in the automatic verification of concurrent systems with respect to linear time temporal logic specifications. The method facilitates the generation of reduced state spaces such that the truth values of a collection of linear temporal logic formulas are the same in the ordinary and reduced state spaces. The only restrictions posed by the method are that the collection of formulas must be known before the reduced state space generation is commenced, the use of the temporal operator “next” is prohibited, and the (reduced) state space of the system must be finite. The method cuts down the number of states by utilising the fact that in concurrent systems the nett result of the occurrence of two events is often independent of the order of occurrence.
abridged version
Chapter PDF
Keywords
- Linear Temporal Logic
- Execution Sequence
- Concurrent System
- State Predicate
- Linear Temporal Logic Formula
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
Aho, A. V., Hopcroft, J. E. & Ullman, J. D.: The Design and Analysis of Computer Algorithms. Addison-Wesley, Reading, Massachusetts 1974, 470 p.
Brookes, S. D., Hoare, C. A. R. & Roscoe, A. W.: A Theory of Communicating Sequential Processes. Journal of the ACM 31 (3) 1984, pp. 560–599.
Clarke, E. M., Emerson, E. A. & Sistla, A. P.: Automatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems 8 (2) 1986 pp. 244–263.
Lamport, L.: What Good is Temporal Logic? Information Processing '83, North-Holland pp. 657–668.
Lichtenstein, O. & Pnueli, A.: Checking that Finite State Concurrent Programs Satisfy their Linear Specification. Proceedings of the Twelfth ACM Symposium on the Principles of Programming Languages, January 1985 pp. 97–107.
Overman, W. T.: Verification of Concurrent Systems: Function and Timing. Ph.D. Dissertation, University of California Los Angeles 1981, 174 p.
Pnueli, A.: Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends. In: Current Trends in Concurrency, Lecture Notes in Computer Science 224, Springer 1986 pp. 510–584.
Valmari, A.: Error Detection by Reduced Reachability Graph Generation. Proceedings of the Ninth European Workshop on Application and Theory of Petri Nets, Venice, Italy 1988 pp. 95–112.
Valmari, A.: Heuristics for Lazy State Generation Speeds up Analysis of Concurrent Systems. Proceedings of the Finnish Artificial Intelligence Symposium STeP-88, Helsinki 1988 Vol. 2 pp. 640–650.
Valmari, A.: State Space Generation: Efficiency and Practicality. Ph.D. Thesis, Tampere University of Technology Publications 55, 1988, 169 p.
Valmari, A.: Eliminating Redundant Interleavings during Concurrent Program Verification. Proceedings of Parallel Architectures and Languages Europe '89 Vol 2, Lecture Notes in Computer Science 366, Springer 1989 pp. 89–103.
Valmari, A.: Stubborn Sets for Reduced State Space Generation. Proceedings of the Tenth International Conference on Application and Theory of Petri Nets, Bonn, FRG 1989 Vol. 2 pp. 1–22. A revised version to appear in Advances in Petri Nets 90, Lecture Notes in Computer Science, Springer.
Wheeler, G. R., Valmari, A. & Billington, J.: Baby Toras Eats Philosophers but Thinks about Solitaire. Proceedings of the Fifth Australian Software Engineering Conference, Sydney, NSW, Australia, 1990 pp. 283–288.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Valmari, A. (1991). A stubborn attack on state explosion. In: Clarke, E.M., Kurshan, R.P. (eds) Computer-Aided Verification. CAV 1990. Lecture Notes in Computer Science, vol 531. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0023729
Download citation
DOI: https://doi.org/10.1007/BFb0023729
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54477-7
Online ISBN: 978-3-540-38394-9
eBook Packages: Springer Book Archive