Paper published in a book (Scientific congresses and symposiums)
Memory efficient algorithms for the verification of temporal properties
Courcoubetis, Costas; Vardi, Moshe; Wolper, Pierre et al.
1991In Computer-Aided Verification, 2nd International Conference Proceedings
Peer reviewed
 

Files


Full Text
CVWY CAV 90.pdf
Author postprint (251.58 kB)
Download

The final publication is available at Springer via http://dx.doi.org/10.1007/BFb0023737


All documents in ORBi are protected by a user license.

Send to



Details



Keywords :
model-checking; temporal properties; Buchi automata
Abstract :
[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
Publisher :
Springer, Berlin, Germany
ISBN/EAN :
978-3-540-54477-7
Collection name :
Lecture Notes in Computer Science, vol 531
Pages :
233-242
Peer reviewed :
Peer reviewed
Available on ORBi :
since 22 January 2015

Statistics


Number of views
40 (0 by ULiège)
Number of downloads
428 (0 by ULiège)

Scopus citations®
 
74
Scopus citations®
without self-citations
63
OpenCitations
 
51

Bibliography


Similar publications



Contact ORBi