Recursive Decomposition of Progress Graphs
Search of a state transition system is traditionally how deadlock detection for concurrent programs has been accomplished. This paper examines an approach to deadlock detection that uses geometric semantics involving the topo-logical notion of dihomotopy to partition the state space into components; after that the reduced state space is exhaustively searched. Prior work partitioned the state space inductively. In this paper we show that a recursive technique provides greater reduction of the size of the state transition system and therefore more efficient deadlock detection. If the preprocessing can be done efficiently, then for large problems we expect to see more efficient deadlock detection and eventually more efficient verification of some temporal properties.
deadlock dihomotopy LTL SPIN verification
David A. Cape Bruce M. McMillin Benjamin W. Passer Mayur Thakur
Department of Computer Science Missouri University of Science and Technology Rolla, MO 65409, USA Google, Inc. 1600 Amphitheatre Parkway Mountain View, CA 94043, USA
国际会议
上海
英文
23-31
2009-07-08（万方平台首次上网日期，不代表论文的发表时间）