A stubborn attack on state explosion
Tóm tắt
Từ khóa
Tài liệu tham khảo
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.
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.
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.
A. Valmari.State Space Generation: Efficiency and Practicality. Ph.D. thesis, Tampere University of Technology Publications 55, Tampere, Finland, 1988.
W.T. Overman.Verification of Concurrent Systems: Function and Timing. Ph.D. dissertation, University of California Los Angeles, 1981.
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.
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.
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.
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.)
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.
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.
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.)
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.
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.
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.
M.Itoh and H.Ichikawa. Protocol verification algorithm using reduced reachability analysis.Transactions of the IECE of Japan, E66(2): 88?93, 1983.
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.
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.
S.Katz and D.Peled. Interleaving set temporal logic.Theoretical Computer Science, 75: 263?287, 1990.
L. Lamport. What good is temporal logic? Information Processing '83,Proceedings of the IFIP 9th World Computer Congress. North-Holland, Amsterdam, pp. 657?668.
A.V.Aho, J.E.Hopcroft and J.D.Ullman.The Design and Analysis of Computer Algorithms. Addison-Wesley, Reading, MA, 1974.
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.
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.
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.
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.