首页 | 本学科首页   官方微博 | 高级检索  
     


Memory-efficient algorithms for the verification of temporal properties
Authors:C. Courcoubetis  M. Vardi  P. Wolper  M. Yannakakis
Affiliation:(1) Institute of Computer Science, 36 Dedalou Street, P.O. Box 1385, 71110 Iraklio, Crete, Greece;(2) Department K55/802, IBM Almaden, 650 Harry Road, 95120-6099 San Jose, CA, U.S.A.;(3) Institut Montefiore, Un. de Liège, B28, B-4000 Liège Sart-Tilman, Belgium;(4) AT&T Bell Labs, 600 Mountain Avenue, 07974 Murray Hill, New Jersey, U.S.A.
Abstract:This article 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 that 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.
Keywords:model-checking  verification  concurrent program  temporal logic  state-space exploration  hashing
本文献已被 SpringerLink 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号