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

Ami SAKAKIBARA  Toshimitsu USHIO  

IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences   Vol.E101-A   No.2   pp.313-321
Publication Date: 2018/02/01
Online ISSN: 1745-1337
DOI: 10.1587/transfun.E101.A.313
Type of Manuscript: INVITED PAPER (Special Section on Mathematical Systems Science and its Applications)
concurrent discrete event systems,  coordinator,  hierarchical supervisory control,  linear temporal logic,  Rabin games,  

Full Text: PDF(1.1MB)
>>Buy this Article

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.