Deadlock Detection for a Class of Communicating Finite State Machines
Yao-Tin Yu, Mohamed G. Gouda · IRE Transactions on Communications Systems · 1982
LetMandNbe two communicating finite state machines which exchange one type of message. We develope a polynomial algorithm to detect whether or notMandNcan reach a deadlock. The time complexity of the algorithm isO(m^{3}n^{3}and its space isO(mn)wheremandnare the numbers of states inMandN, respectively. The algorithm can also be used to verify that two communicating machines which exchange many types of messages are deadlock-free.