Supervisory control and reactive synthesis: a comparative introduction

被引:0
作者
Rüdiger Ehlers
Stéphane Lafortune
Stavros Tripakis
Moshe Y. Vardi
机构
[1] University of Bremen,
[2] DFKI GmbH,undefined
[3] University of Michigan,undefined
[4] University of California at Berkeley,undefined
[5] Aalto University,undefined
[6] Rice University,undefined
来源
Discrete Event Dynamic Systems | 2017年 / 27卷
关键词
Supervisory control; Reactive synthesis; Non-blockingness; Maximal permissiveness;
D O I
暂无
中图分类号
学科分类号
摘要
This paper presents an introduction to and a formal connection between synthesis problems for discrete event systems that have been considered, largely separately, in the two research communities of supervisory control in control engineering and reactive synthesis in computer science. By making this connection mathematically precise in a paper that attempts to be as self-contained as possible, we wish to introduce these two research areas to non-expert readers and at the same time to highlight how they can be bridged in the context of classical synthesis problems. After presenting general introductions to supervisory control theory and reactive synthesis, we provide a novel reduction of the basic supervisory control problem, non-blocking case, to a problem of reactive synthesis with plants and with a maximal permissiveness requirement. The reduction is for fully-observed systems that are controlled by a single supervisor/controller. It complements prior work that has explored problems at the interface of supervisory control and reactive synthesis. The formal bridge constructed in this paper should be a source of inspiration for new lines of investigation that will leverage the power of the synthesis techniques that have been developed in these two areas.
引用
收藏
页码:209 / 260
页数:51
相关论文
共 39 条
[1]  
Arnold A(2003)Games for synthesis of controllers with partial observation Theor Comput Sci 303 7-34
[2]  
Vincent A(1969)Solving sequential conditions by finite-state strategies Trans. AMS 138 295-311
[3]  
Walukiewicz I(1986)Automatic verification of finite-state concurrent systems using temporal logic specifications ACM Trans Program Lang Syst 8 244-263
[4]  
Büchi JR(2005)Multitasking supervisory control of discrete-event systems. Discrete Event Dynamic Systems Theory Appl 15 375-395
[5]  
Landweber LH(1982)Using branching time logic to synthesize synchronization skeletons Sci Comput Program 2 241-266
[6]  
Clarke EM(1986)Sometimes and Not Never revisited: on branching versus linear time temporal logic J. ACM 33 151-178
[7]  
Emerson EA(2009)A direct path to dependable software Commun. ACM 52 78-88
[8]  
Sistla AP(2006)Supervisory Control of Discrete Event Systems with CTL* Temporal Logic Specifications SIAM J Control Optim 44 2079-2103
[9]  
de Queiroz MH(1992)On supervisory control of sequential behaviors IEEE Trans Autom Control 37 1978-1985
[10]  
Cury JER(2012)Supervisory control synthesis of discrete-event systems using a coordination scheme Automatica 48 247-254