Reference : Memory Efficient Algorithms for the Verification of Temporal Properties
Scientific journals : Article
Engineering, computing & technology : Computer science
http://hdl.handle.net/2268/164300
Memory Efficient Algorithms for the Verification of Temporal Properties
English
Courcoubetis, Constantin [> > > >]
Vardi, Moshe Y [> > > >]
Wolper, Pierre mailto [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 [> > > >]
1992
Formal Methods in System Design
Springer Science & Business Media B.V.
1
275--288
Yes (verified by ORBi)
International
0925-9856
1572-8102
[en] model-checking ; temporal properties ; Büchi automata
[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.
Researchers
http://hdl.handle.net/2268/164300
10.1007/BF00121128
he final publication is available at Springer via http://dx.doi.org/10.1007/BF00121128

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
CVWY FMSD 92.pdfAuthor postprint279.73 kBView/Open

Bookmark and Share SFX Query

All documents in ORBi are protected by a user license.