Abstract
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. © 2009 IEEE.
Recommended Citation
D. A. Cape et al., "Recursive Decomposition of Progress Graphs," SSIRI 2009 - 3rd IEEE International Conference on Secure Software Integration Reliability Improvement, pp. 23 - 31, article no. 5325396, Institute of Electrical and Electronics Engineers, Dec 2009.
The definitive version is available at https://doi.org/10.1109/SSIRI.2009.19
Department(s)
Computer Science
Keywords and Phrases
Deadlock; Dihomotopy; LTL; SPIN; Verification
International Standard Book Number (ISBN)
978-076953758-0
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
01 Dec 2009
