Static Deadlock Detection for Active Objects

We present a static technique for deadlock detection for active objects. To do so, we introduce a novel kind of automata (visibly multiset automata, VMAs for short) to describe in an approximative manner the behaviour of one active object resp. a deadlock scenario. In this setting deadlock detection is checking the intersection of the VMAs for emptiness. We illustrate our technique in terms of the Creol language.