%T Parallel Algorithms for Deadlock and Livelock Analysis of Concurrent Systems
%A  Jeremy M. R. Martin,  Yvonne Huddart
%E Peter H. Welch,  Andr\[`e] W. P. Bakkers
%B Communicating Process Architectures 2000
%X Conventional model\-checking techniques for analysing
   concurrent systems for deadlock or livelock are hampered by
   the problem of exponential state explosion: the overall
   number of global states that needs to be checked may grow
   exponentially with the number of component processes in the
   system. The state\-of\-the\-art commercial tool FDR provides
   deadlock and livelock analysis but it is limited at present
   to analysing systems of up to one hundred million global
   states. The Deadlock Checker tool is capable of analysing
   very much larger systems by taking certain short\-cuts. But
   this is achieved at the cost of incompleteness \-\- there
   are certain deadlock\-free and livelock\-free networks that
   may not be proven so using that tool. Here we investigate a
   different approach. We present parallelised model\-checking
   algorithms for deadlock and livelock analysis and describe
   their implementation. The techniques are found to scale well
   running either on a conventional supercomputer or on a PC
   cluster.