Building Distributed Controllers for Systems with Priorities

Composition of components by means of multi-party synchronizations and priorities allows specifying properties of systems in a very abstract manner, and are meaningful for many application domains. Such specifications are generally easier to verify than the more concrete ones based on message passing. Synchronizations may introduce deadlocks, whereas priorities do not.In this paper, we propose two algorithms: one which given a specification Sys constructs — if necessary and if possible — a set of priority rules enforcing deadlock freedom. A second algorithm builds a distributed implementation of such a prioritized specification. This second algorithm is presently restricted to binary synchronizations but it differs from comparable algorithms such as α-core (1) by the fact that it handles specifications with (global) priorities. We have implemented this algorithm and compared its efficiency with α-core in the priorityless case.