کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
715492 | 892204 | 2014 | 6 صفحه PDF | دانلود رایگان |
We present a formal connection between supervisory control theory in the field of control engineering and reactive synthesis in the field of formal methods. We focus on the case of fully-observed discrete-event systems that are controlled by a single controller/supervisor in order to achieve a safety specification and a non-blocking specification. The connection is shown by a reduction of the corresponding supervisory control problem to a problem of reactive synthesis with plants and maximal permissiveness, subject to a CTL temporal logic specification. In order to establish the desired reduction, we prove two new results regarding (i) a simplified version of the standard supervisory control problem and (ii) a class of reactive synthesis problems that admit unique maximally permissive solutions. The reduction complements prior work at the boundary of supervisory control and reactive synthesis.
Journal: IFAC Proceedings Volumes - Volume 47, Issue 2, 2014, Pages 222-227