A stubborn attack on state explosion. (English) Zbl 0783.68083
Summary: The article 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 linear temporal logic formulas are the same in the ordinary and reduced state spaces. The only restrictions posed by the method are
1) the formulas must be known before the reduced state-space generation is commenced;
2) the use of the temporal operator “next state” is prohibited; and
3) the (reduced) state space of the system must be finite.
The method cuts down the number of states by utilizing the fact that in concurrent systems the net result of the occurrence of two events is often independent of the order of occurrence.
1) the formulas must be known before the reduced state-space generation is commenced;
2) the use of the temporal operator “next state” is prohibited; and
3) the (reduced) state space of the system must be finite.
The method cuts down the number of states by utilizing the fact that in concurrent systems the net result of the occurrence of two events is often independent of the order of occurrence.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B45 | Modal logic (including the logic of norms) |
| 68Q10 | Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) |
Keywords:
\(LTL\)-preserving stubborn set method; automatic verification of concurrent systems; reduced state spaces; temporal logicReferences:
| [1] | E.M.Clarke, E.A.Emerson, and A.P.Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications.ACM Transactions on Programming Languages and Systems, 8 (2): 244-263, 1986. · Zbl 0591.68027 · doi:10.1145/5397.5399 |
| [2] | O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. Proceedings of the Twelfth ACM Symposium on the Principles of Programming Languages, New Orleans, LA, January 1985, pp. 97-107. |
| [3] | A. Pnueli. Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends. InCurrent Trends in Concurrency, Lecture Notes in Computer Science, 224: 510-584, 1986. |
| [4] | A. Valmari.State Space Generation: Efficiency and Practicality. Ph.D. thesis, Tampere University of Technology Publications 55, Tampere, Finland, 1988. |
| [5] | W.T. Overman.Verification of Concurrent Systems: Function and Timing. Ph.D. dissertation, University of California Los Angeles, 1981. |
| [6] | A. Valmari. Error detection by reduced reachability graph generation. Proceedings of the Ninth European Workshop on Application and theory of Petri Nets, Venice, Italy, pp. 95-112, 1988. |
| [7] | A. Valmari. Heuristics for lazy state generation speeds up analysis of concurrent systems. Proceedings of the Finnish Artificial Intelligence Symposium STeP-88, Helsinki, Vol. 2, pp. 640-650, 1988. |
| [8] | A.Valmari. Eliminating redundant interleavings during concurrent program verification. Proceedings of Parallel Architectures and Languages Europe ’89, Eindhoven, The Netherlands, June 1989, Vol. 2.Lecture Notes in Computer Science, 366: 89-103, 1989. |
| [9] | A.Valmari. Stubborn sets for reduced state space generation.Advances in Petri Nets 1990. Lecture Notes in Computer Science, 483: 491-515, 1991. (An earlier version appeared in Proceedings of the Tenth International Conference on Application and Theory of Petri Nets, Bonn, FRG, Vol. II, pp. 1-22, 1989.) |
| [10] | A. Valmari. Stubborn sets of coloured Petri nets. Proceedings of the 12th International Conference on Application and Theory of Petri Nets, Gjern, Denmark, pp. 102-121, 1991. |
| [11] | A. Valmari and M. Clegg. Reduced labelled transition systems save verification effort.Proceedings of CONCUR ’91, Amsterdam, The Netherlands, August 1991.Lecture Notes in Computer Science, 527: 526-540, 1991. |
| [12] | A. Valmari. A stubborn attack on state explosion. Computer-Aided Verification ’90, New Brunswick, NJ (proceedings of a workshop).AMS-ACM DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 3, pp. 25-41. American Mathematical Society, 1991. (An abbreviated version appeared in Computer-Aided Verification, 2nd International Conference,Lecture Notes in Computer Science, 531: 156-165, 1991.) · Zbl 0786.68069 |
| [13] | P. Godefroid. Using partial orders to improve automatic verification methods. Computer-Aided Verification ’90, New Brunswick, NJ (proceedings of a workshop).AMS-ACM DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 3. American Mathematical Society, 1991, pp. 321-340. · Zbl 0786.68061 |
| [14] | P.Godefroid and P.Wolper. Using partial orders for the efficient verification of deadlock-freedom and safety properties. Proceedings of Computer-Aided Verification ’91, Aalborg, Denmark, July 1991.Lecture Notes in Computer Science 575: 332-342, 1992. · Zbl 0772.68064 |
| [15] | P. Godefroid and P. Wolper. A partial approach to model checking. Proceedings of the 6th Symposium on Logic in Computer Science, Amsterdam, The Netherlands, pp. 406-415, July 1991. · Zbl 0806.68079 |
| [16] | M.Itoh and H.Ichikawa. Protocol verification algorithm using reduced reachability analysis.Transactions of the IECE of Japan, E66(2): 88-93, 1983. |
| [17] | R. Janicki and M. Koutny. On some implementation of optimal simulations. Computer-Aided Verification ’90, New Brunswick, NJ, (proceedings of a workshop).AMS-ACM DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 3. American Mathematical Society, 1991, pp. 231-250. · Zbl 0797.68111 |
| [18] | J.Quemada. Compressed state space representation in LOTOS with the interleaved expansion.Protocol Specification, Testing and Verification XI (Proceedings of the 11th International IFIP WG 6.1 Symposium, Stockholm, Sweden, June 1991). North-Holland, Amsterdam, 1991, pp. 19-35. |
| [19] | S.Katz and D.Peled. Interleaving set temporal logic.Theoretical Computer Science, 75: 263-287, 1990. · Zbl 0718.03014 · doi:10.1016/0304-3975(90)90096-Z |
| [20] | L. Lamport. What good is temporal logic? Information Processing ’83,Proceedings of the IFIP 9th World Computer Congress. North-Holland, Amsterdam, pp. 657-668. |
| [21] | A.V.Aho, J.E.Hopcroft and J.D.Ullman.The Design and Analysis of Computer Algorithms. Addison-Wesley, Reading, MA, 1974. · Zbl 0326.68005 |
| [22] | G.R. Wheeler, A. Valmari, and J. Billington, Baby Toras eats philosophers but thinks about solitaire. Proceedings of the Fifth Australian Software Engineering Conference, Sydney, NSW, Australia 1990, pp. 283-288. |
| [23] | J. Kemppainen, M. Levanto, A. Valmari, and M. Clegg. ?ARA? puts advanced reachability analysis methods together. Tampere University of Technology, Software Systems Laboratory Report 14: Proceedings of the Fifth Nordic Workshop on Programming Environment Research, Tampere, Finland, January 1992. |
| [24] | S.D.Brookes, C.A.R.Hoare, and A.W.Roscoe. A theory of communicating sequential processes.Journal of the ACM, 31 (3): 560-599, 1984. · Zbl 0628.68025 · doi:10.1145/828.833 |
| [25] | A.Valmari and M.Tienari. An improved failures equivalence for finite-state systems with a reduction algorithm.Protocol Specification, Testing and Verification XI (Proceedings of the 11th International IFIP WG 6.1 Symposium, Stockholm, Sweden, June 1991). North-Holland, Amsterdam, 1991, pp. 3-18. |
| [26] | S. Graf and B. Steffen. Compositional minimization of finite-state processes. Computer-Aided Verification ’90, New Brunswick, NJ, (proceedings of a workshop).AMS-ACM DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 3. American Mathematical Society, 1991, pp. 57-73. · Zbl 0789.68094 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
