Abstract
Deadlock detection for concurrent programs has traditionally been accomplished by symbolic methods or by search of a state transition system. We examine an approach that uses geometric semantics involving the topological notion of dihomotopy to partition the state-space into components, after which the reduced state-space is exhaustively searched. Prior work partitioned the state-space inductively, but in this paper, we show that a recursive technique provides greater reduction of the size of the state transition system. as a result, we expect to see more efficient deadlock detection and eventually more efficient verification of some temporal properties for large problems if the partitioning can be done efficiently. © 2009 IEEE.
Recommended Citation
D. A. Cape and B. M. McMillin, "Dihomotopic Reduction Used in Deadlock Detection," Proceedings - International Computer Software and Applications Conference, vol. 1, pp. 648 - 651, article no. 5254192, Institute of Electrical and Electronics Engineers, Nov 2009.
The definitive version is available at https://doi.org/10.1109/COMPSAC.2009.200
Department(s)
Computer Science
Keywords and Phrases
Deadlock; Dihomotopy; LTL; SPIN; Verification
International Standard Book Number (ISBN)
978-076953726-9
International Standard Serial Number (ISSN)
0730-3157
Document Type
Article - Conference proceedings
Document Version
Citation
File Type
text
Language(s)
English
Rights
© 2024 Institute of Electrical and Electronics Engineers, All rights reserved.
Publication Date
23 Nov 2009
