Maximally permissive controlled system synthesis for non-determinism and modal logic

We propose a new technique for controlled system synthesis on non-deterministic automata for requirements in modal logic. Synthesis, as defined in this paper, restricts a behavioral specification of the uncontrolled system such that it satisfies a given logical expression, while adhering to the rule...

Full description

Saved in:
Bibliographic Details
Published in:Discrete event dynamic systems 2017-03, Vol.27 (1), p.109-142
Main Authors: van Hulst, A. C., Reniers, M. A., Fokkink, W. J.
Format: Article
Language:English
Subjects:
Case studies
Control
Control theory
Controllability
Convex and Discrete Geometry
Electrical Engineering
Logic
Machines
Manufacturing
Mathematics
Mathematics and Statistics
Operations Research/Decision Theory
Processes
Stability
Supervisory control
Synthesis
Systems Theory
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We propose a new technique for controlled system synthesis on non-deterministic automata for requirements in modal logic. Synthesis, as defined in this paper, restricts a behavioral specification of the uncontrolled system such that it satisfies a given logical expression, while adhering to the rules dictated by supervisory control such as maximal permissiveness and controllability. The applied requirement formalism extends Hennessy-Milner logic with the invariant and reachability modalities from Gödel-Löb logic, and is therefore able to express a broad range of control requirements, such as marker state reachability and deadlock-freeness. This paper contributes to the field of control synthesis by achieving maximal permissiveness in a non-deterministic context for control requirements in modal logic, and treatment of controllability via partial bisimulation. We present a well-defined and complete derivation of the synthesis result, which is supported further by computer-verified proofs created using the Coq proof assistant. The synthesis method is also presented in algorithmic form, including an analysis of its computational complexity. We show that the proposed synthesis theory allows full expressibility of Ramadge-Wonham supervisory control theory and we illustrate its applicability in two small industrial case studies, including an analysis with regard to scalability.
ISSN:0924-6703
1573-7594
DOI:10.1007/s10626-016-0231-8