On the relation between reactive synthesis and supervisory control of non-terminating processes
Schmuck AK, Moor T, Majumdar R (2019)
Publication Type: Journal article
Publication year: 2019
Journal
DOI: 10.1007/s10626-019-00299-5
Abstract
Reactive synthesis and supervisory control theory both provide a design methodology for the automatic and algorithmic design of digital systems from declarative specifications. The reactive synthesis approach originates in computer science, and seeks to synthesise a system that interacts with its environment over time and that, doing so, satisfies a prescribed specification. Here, the distinguishing feature when compared to other synthesis problems in computer science is that the interaction is temporal in that it explicitly refers to a sequence of computation cycles. Supervisory control originates in control theory and seeks to synthesise a controller that - in closed-loop configuration with a plant - enforces a prescribed specification over time. The distinguishing feature compared to other branches of control is that all dynamics are driven by discrete events as opposed to continuous signals. While both methods apparently are closely related, the technical details differ significantly. We provide a formal comparison which allows us to identify conditions under which one can solve one synthesis problem using methods from the other one; we also discuss how the resulting solutions compare. To facilitate this comparison, we give a unified introduction to reactive synthesis and supervisory control and derive formal problem statements and a characterisation of their solutions in terms of omega-languages. Recent contributions to the two fields address different aspects of the respective problem, and we expect the formal relationship identified in this paper to be useful in that it allows the application of algorithmic techniques from one field in the other.
Authors with CRIS profile
Involved external institutions
Germany (DE)How to cite
APA:
Schmuck, A.-K., Moor, T., & Majumdar, R. (2019). On the relation between reactive synthesis and supervisory control of non-terminating processes. Discrete Event Dynamic Systems-Theory and Applications. https://dx.doi.org/10.1007/s10626-019-00299-5
MLA:
Schmuck, Anne-Kathrin, Thomas Moor, and Rupak Majumdar. "On the relation between reactive synthesis and supervisory control of non-terminating processes." Discrete Event Dynamic Systems-Theory and Applications (2019).
BibTeX: Download