Control of Non-Deterministic Systems With μ-Calculus Specifications Using Quotienting

The supervisory control problem for discrete event system (DES) under control involves identifying the supervisor, if one exists, which, when synchronously composed with the DES, results in a system that conforms to the control specification. In this context, we consider a non-deterministic DES under complete observation and control specification expressed in action-based propositional mu-calculus. The key to our solution is the process of quotienting the control specification against the plan resulting in a new mu-calculus formula such that a model for the formula is the supervisor. Thus the task of control synthesis is reduced a problem of mu-calculus satisfiability. In contrast to the existing mu-calculus quotienting-based techniques that are developed in deterministic setting, our quotienting rules can handle nondeterminism in the plant models. Another distinguishing feature of our technique is that while existing techniques use a separate mu-calculus formula to describe the controllability constraint (that uncontrollable events of plants are never disabled by a supervisor), we absorb this constraint as part of quotienting which allows us to directly capture more general state-dependent controllability constraints. Finally, we develop a tableau-based technique for verifying satisfiability of quotiented formula and model generation. The runtime for the technique is exponential in terms of the size of the plan and the control specification. A better complexity result that is polynomial to plant size and exponential to specification size is obtained when the controllability property is state-independent. A prototype implementation in a tabled logic programming language as well as some experimental results are presented.

Automated summary

The study introduces a new method to address the supervisory control problem for discrete event systems (DES), by folding the control specification to generate a new mu-calculus formula for determining the supervisor, thus simplifying the control synthesis process.