Hierarchical Control of Concurrent Discrete Event Systems with Linear Temporal Logic Specifications

In this paper, we study a control problem of a concurrent discrete event system, where several subsystems are partially synchronized via shared events, under local and global constraints described by linear temporal logic formulas. We propose a hierarchical control architecture consisting of local supervisors and a coordinator. While the supervisors ensure the local requirements, the coordinator decides which shared events to be disabled so as to satisfy the global specification. First, we construct Rabin games to obtain local supervisors. Next, we reduce them based on shared transitions. Finally, we construct a global Rabin game from the reduced supervisors and a deterministic Rabin automaton that accepts every run satisfying the global specification. By solving it, we obtain a coordinator that disables shared events to guarantee the global requirement. Moreover, the concurrent system controlled by the coordinator and the local supervisors is deadlock-free.