TY - GEN
T1 - Maximally permissive controlled system synthesis for modal logic
AU - van Hulst, Allan C.
AU - Reniers, Michel A.
AU - Fokkink, Wan
PY - 2015
Y1 - 2015
N2 - We propose a new method for controlled system synthesis on non-deterministic automata, which includes the synthesis for deadlock-freeness, as well as invariant and reachability expressions. Our technique restricts the behavior of a Kripke-structure with labeled transitions, representing the uncontrolled system, such that it adheres to a given requirement specification in an expressive modal logic, while all non-invalidating behavior is retained. This induces maximal permissiveness in the context of supervisory control. Research presented in this paper allows a system model to be constrained according to a broad set of liveness, safety and fairness specifications of desired behavior, and embraces most concepts from Ramadge-Wonham supervisory control, including controllability and marker-state reachability. The synthesis construction is formally verified using the Coq proof assistant.
AB - We propose a new method for controlled system synthesis on non-deterministic automata, which includes the synthesis for deadlock-freeness, as well as invariant and reachability expressions. Our technique restricts the behavior of a Kripke-structure with labeled transitions, representing the uncontrolled system, such that it adheres to a given requirement specification in an expressive modal logic, while all non-invalidating behavior is retained. This induces maximal permissiveness in the context of supervisory control. Research presented in this paper allows a system model to be constrained according to a broad set of liveness, safety and fairness specifications of desired behavior, and embraces most concepts from Ramadge-Wonham supervisory control, including controllability and marker-state reachability. The synthesis construction is formally verified using the Coq proof assistant.
UR - http://www.scopus.com/inward/record.url?scp=84922010222&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84922010222&partnerID=8YFLogxK
M3 - Conference contribution
VL - 8939
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 230
EP - 241
BT - SOFSEM 2015: Theory and Practice of Computer Science - 41st International Conference on Current Trends in Theory and Practice of Computer Science
PB - Springer/Verlag
T2 - 41st International Conference on Current Trends in Theory and Practice of Computer Science, SOFSEM 2015
Y2 - 24 January 2015 through 29 January 2015
ER -