[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 (Büchi 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 some 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 that the presently known algorithms require.
Disciplines :
Computer science
Author, co-author :
Courcoubetis, Constantin
Vardi, Moshe Y
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, Mihalis
Language :
English
Title :
Memory Efficient Algorithms for the Verification of Temporal Properties
West C.H. (1978) Generalized technique for communication protocol validation. IBM Journal of Research and Development 22:393-404.
Liu M.T. (1989) Protocol engineering. Advances in Computing 29:79-195.
Rudin H. (1987) Network protocols and tools to help produce them. Annual Review of Computer Science 2:191-316.
West C.H., Zafiropulo P. (1978) Automated validation of a communication protocol: the ccitt x.21 recommendation. IBM Journal of Research and Development 22:60-71.
Rudin H., West C.H. (1982) A validation technique for tightly-coupled protocols. IEEE Transactions on Computers 312:630-636.
.
Hailpern B.T. (1985) Tools for verifying network protocols. Logic and Models of Concurrent Systems , K., Apt, NATO ISI Series, Springer-Verlag, New York; 57-76.
Grotz R., Jard C., Lassudrie C. (1984) Attacking a complex distributed systems for different sides: an experience with complementary validation tools. Proceedings of the 4th Workshop of Protocol Specification, Testing, and Verification , North-Holland, Amsterdam; 3-17.
Clarke E.M., Emerson E.A., Sistla A.P. (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems 8(2):244-263.
.
.
Queille J.P., Sifakis J. (1981) Specification and verification of concurrent systems in cesar. Proceedings of the 5th International Symposium on Programming , Lecture Notes in Computer Science, Springer Verlag, New York; 337-351.
Vardi M. (1989) Unified verification theory. Proceedings of Temporal Logic in Specification , B., Banieqbal, H., Barringer, A., Pneuli, Lecture Notes in Computer Science, Springer-Verlag, New York; 202-212.
.
Wolper P. (1989) On the relation of programs and computations to models of temporal logic. Proceedings of Temporal Logic in Specification , B., Banieqbal, H., Barringer, A., Pnueli, Lecture Notes in Computer Science, Springer-Verlag, New York; 75-123.
Holzmann G. (1988) An improved protocol reachability analysis technique. Software Practice and Experience 18(2):137-161.
Jard C., Jéron T. (1989) On-line model-checking for finite linear temporal logic specifications. Automatic Verification Methods for Finite State Systems, Proceedings of a International Workshop, Grenoble , Lecture Notes in Computer Science, Springer-Verlag, New York; 189-96.
.
Thayse From Modal Logic to Deductive Databases: Introducing a Logic Based Approach to Artificial Intelligence, Wiley, New York; 1989.
Aho, Hopcroft, Ullman The Design and Analysis of Computer Algorithms, Addison Wesley, Reading, MA; 1974.
Aggarwal S., Courcoubetis C., Wolper P. (1990) Adding liveness properties to coupled finite-state machines. ACM Transactions on Programming Languages and Systems 12(2):303-339.
Aho, Hopcroft, Ullman Data Structures and Algorithms, Addison Wesley, Reading, MA; 1982.
