The language of certain conflicts of a nondeterministic process

Abstract

The language of certain conflicts is the most general set of behaviours of a nondeterministic process, which certainly lead to a livelock or deadlock when accepted by another process running in parallel. It is of great use in model checking to detect livelocks or deadlocks in very large systems, and in process-algebra to obtain abstractions preserving livelock and deadlock. Unfortunately, the language of certain conflicts is difficult to compute and has only been approximated in previous work. This paper presents an effective algorithm to calculate the language of certain conflicts for any given nondeterministic finite-state process and discusses its properties. The algorithm is shown to be correct and of exponential complexity.