Deadlock Detection in Discrete Concurrent Systems

摘要

In this paper a method of deadlock detection in the concurrent discrete systems is given. Sequent automaton is used as a universal model of discrete systems. The method is based on constructing a sub-graph of reach ability graph of the system. It can be considered as a generalization of the stubborn set method for Petri nets.