[en] This paper addresses the problem of designing memory efficient algorithms for the verification of temporal properties of finite-state programs. Both the programs and their desired temporal properties are modeled as automata on infinite words (Buchi automata). Verification is then reduced to checking the emptiness of the automaton resulting from the product of the program and the property. This problem is usually solved by computing the strongly connected components of the graph representing the product automaton. Here, we present algorithms which solve the emptiness problem without explicitly constructing the strongly connected components of the product graph. By allowing the algorithms to err with a small probability, we can implement them with a randomly accessed memory of size O(n) bits, where n is the number of states of the graph, instead of O(n log n) bits which the presently known algorithms require.
Disciplines :
Computer science
Author, co-author :
Courcoubetis, Costas
Vardi, Moshe
Wolper, Pierre ; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique (parallélisme et banques de données)
Yannakakis, Mihailis
Language :
English
Title :
Memory efficient algorithms for the verification of temporal properties
Publication date :
1991
Event name :
2nd International Conference on Computer Aided Verification (CAV '90)
Event place :
New Brunswick, United States - New Jersey
Event date :
June 18–21, 1990
Audience :
International
Main work title :
Computer-Aided Verification, 2nd International Conference Proceedings
scite shows how a scientific paper has been cited by providing the context of the citation, a classification describing whether it supports, mentions, or contrasts the cited claim, and a label indicating in which section the citation was made.
Bibliography
S. Aggarwal, C. Courcoubetis, and P. Wolper. Adding liveness properties to coupled finite-state machines. ACM Transactions on Programming Languages and Systems, 12(2):303-339, 1990.
Alfred V. Aho, John E. Hopcroft, and Jeffrey D. Ullman. The Design and Analysis of Computer Algorithms. Addison Wesley, Reading, 1974.
Alfred V. Aho, John E. Hopcroft, and Jeffrey D. Ullman. Data Structures and Algorithms. Addison Wesley, Reading, 1982.
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, January 1986.
E. M. Clarke and O. Grümberg. Avoiding the state explosion problem in temporal logic model-checking algorithms. In Proc. 6th ACM Symposium on Principles of Distributed Computing, pages 294-303, Vancouver, British Columbia, August 1987.
R. Grotz, C. Jard, and C. Lassudrie. Attacking a complex distributed systems from different sides: an experience with complementary validation tools. In Proc. 4th Work. Protocol Specification, Testing, and Verification, pages 3-17. North-Holland, 1984.
B.T. Hailpern. Tools for verifying network protocols. In K. Apt, editor, Logic and Models of Concurrent Systems, NATO ISI Series, pages 57-76. Springer-Verlag, 1985.
G. Holzmann. An improved protocol reachability analysis technique. Software Practice and Experience, pages 137-161, February 1988.
C. Jard and T. Jeron. On-line model-checking for finite linear temporal logic specifications. In Automatic Verification Methods for Finite State Systems, Proc. Int. Workshop, Grenoble, volume 407, pages 189-196, Grenoble, June 1989. Lecture Notes in Computer Science, Springer-Verlag.
M.T. Liu. Protocol engineering. Advances in Computing, 29:79-195, 1989.
O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proceedings of the Twelfth ACM Symposium on Principles of Programming Languages, pages 97-107, New Orleans, January 1985.
J.P. Quielle and J. Sifakis. Specification and verification of concurrent systems in cesar. In Proc. 5th Int’l Symp. on Programming, volume 137, pages 337-351. Springer-Verlag, Lecture Notes in Computer Science, 1981.
H. Rudin. Network protocols and tools to help produce them. Annual Review of Computer Science, 2:291-316, 1987.
H. Rudin and C.H. West. A validation technique for tightly-coupled protocols. IEEE Transactions on Computers, C-312:630-636, 1982.
C.A. Sunshine. Experience with automated protocol verification. In Proceedings of the International Conference on Communication, pages 1306-1310, 1983.
M. Vardi. Unified verification theory. In B. Banieqbal, H. Barringer, and A. Pnueli, editors, Proc. Temporal Logic in Specification, volume 398, pages 202-212. Lecture Notes in Computer Science, Springer-Verlag, 1989.
M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. Symp. on Logic in Computer Science, pages 322-331, Cambridge, june 1986.
M.Y. Vardi and P. Wolper. Reasoning about infinite computation paths. IBM Research Report RJ6209, 1988.
C.H. West. Generalized technique for communication protocol validation. IBM J. of Res. and Devel., 22:393-404, 1978.
P. Wolper. On the relation of programs and computations to models of temporal logic. In B. Banieqbal, H. Barringer, and A. Pnueli, editors, Proc. Temporal Logic in Specification, volume 398, pages 75-123. Lecture Notes in Computer Science, Springer-Verlag, 1989.
C.H. West and P. Zafiropulo. Automated validation of a communication protocol: the ccitt x.21 recommendation. IBM Journal of Research and Development, 22:60-71, 1978a
This website uses cookies to improve user experience. Read more
Save & Close
Accept all
Decline all
Show detailsHide details
Cookie declaration
About cookies
Strictly necessary
Performance
Strictly necessary cookies allow core website functionality such as user login and account management. The website cannot be used properly without strictly necessary cookies.
This cookie is used by Cookie-Script.com service to remember visitor cookie consent preferences. It is necessary for Cookie-Script.com cookie banner to work properly.
Performance cookies are used to see how visitors use the website, eg. analytics cookies. Those cookies cannot be used to directly identify a certain visitor.
Used to store the attribution information, the referrer initially used to visit the website
Cookies are small text files that are placed on your computer by websites that you visit. Websites use cookies to help users navigate efficiently and perform certain functions. Cookies that are required for the website to operate properly are allowed to be set without your permission. All other cookies need to be approved before they can be set in the browser.
You can change your consent to cookie usage at any time on our Privacy Policy page.