Exposure to deadlock for communicating processes is hard to detect (Q1064050)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: Exposure to deadlock for communicating processes is hard to detect |
scientific article; zbMATH DE number 3919792
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Exposure to deadlock for communicating processes is hard to detect |
scientific article; zbMATH DE number 3919792 |
Statements
Exposure to deadlock for communicating processes is hard to detect (English)
0 references
1985
0 references
It is shown that the applicability of global state analysis as a tool for proving correctness of communication protocols is limited. \textit{D. Brand} and \textit{P. Zafiropulo} [J. Assoc. Comput. Mach. 30, 323-342 (1983; Zbl 0512.68039)] showed that reachability of global deadlock states for protocols with unbounded FIFO channels is undecidable. It is shown that the same is true for unbounded non-FIFO channels. For bounded FIFO channels the problem is shown to be PSPACE-hard.
0 references
undecidability
0 references
validation
0 references
global state analysis
0 references
correctness of communication protocols
0 references
reachability of global deadlock states
0 references
FIFO channels
0 references
0 references
