Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Supervisory Control Theory with Event Forcing

Michel Reniers, Kai Cai

TL;DR

This work extends Ramadge–Wonham supervisory control theory by introducing forcible events that allow a supervisor to preempt uncontrollable events, formalizing forcible-controllability and proving the existence of a maximally permissive, forcibly-controllable, nonblocking supervisor. It provides a constructive synthesis algorithm to compute such a supervisor and proves a solvability condition: a specification $F\subseteq L_m(P)$ is achievable iff $F$ is forcibly-controllable; it also defines a supremal forcibly-controllable sublanguage $F_{\sup}$ to realize maximal permissiveness. The approach is illustrated through two case studies (a small manufacturing line and a small factory) showing increased permissiveness when forcible events are available. The results broaden SCT applicability to settings where forcing can preempt undesirable uncontrollable behavior, with implications for nonblocking guarantees and practical controller implementations. The framework leverages standard language-theoretic constructs ($L(P)$, $L_m(P)$) and introduces new notions like forcible-sublanguages and forced preemption to enable richer supervisory behavior.

Abstract

In the Ramadge-Wonham supervisory control theory the only interaction mechanism between supervisor and plant is that the supervisor may enable/disable events from the plant and the plant makes a final decision about which of the enabled events is actually taking place. In this paper, the interaction between supervisor and plant is enriched by allowing the supervisor to force specific events (called forcible events) that are allowed to preempt uncontrollable events. A notion of forcible-controllability is defined that captures the interplay between controllability of a supervisor w.r.t. the uncontrollable events provided by a plant in the setting with event forcing. Existence of a maximally permissive, forcibly-controllable, nonblocking supervisor is shown and an algorithm is provided that computes such a supervisor. The approach is illustrated by two small case studies.

Supervisory Control Theory with Event Forcing

TL;DR

This work extends Ramadge–Wonham supervisory control theory by introducing forcible events that allow a supervisor to preempt uncontrollable events, formalizing forcible-controllability and proving the existence of a maximally permissive, forcibly-controllable, nonblocking supervisor. It provides a constructive synthesis algorithm to compute such a supervisor and proves a solvability condition: a specification is achievable iff is forcibly-controllable; it also defines a supremal forcibly-controllable sublanguage to realize maximal permissiveness. The approach is illustrated through two case studies (a small manufacturing line and a small factory) showing increased permissiveness when forcible events are available. The results broaden SCT applicability to settings where forcing can preempt undesirable uncontrollable behavior, with implications for nonblocking guarantees and practical controller implementations. The framework leverages standard language-theoretic constructs (, ) and introduces new notions like forcible-sublanguages and forced preemption to enable richer supervisory behavior.

Abstract

In the Ramadge-Wonham supervisory control theory the only interaction mechanism between supervisor and plant is that the supervisor may enable/disable events from the plant and the plant makes a final decision about which of the enabled events is actually taking place. In this paper, the interaction between supervisor and plant is enriched by allowing the supervisor to force specific events (called forcible events) that are allowed to preempt uncontrollable events. A notion of forcible-controllability is defined that captures the interplay between controllability of a supervisor w.r.t. the uncontrollable events provided by a plant in the setting with event forcing. Existence of a maximally permissive, forcibly-controllable, nonblocking supervisor is shown and an algorithm is provided that computes such a supervisor. The approach is illustrated by two small case studies.
Paper Structure (8 sections, 6 theorems, 17 equations, 7 figures)

This paper contains 8 sections, 6 theorems, 17 equations, 7 figures.

Table of Contents

  1. Introduction
  2. Forcible Events and Forcing Supervisory Control
  3. Forcibly-Controllable Sublanguages
  4. Supremal Forcibly-Controllable Sublanguages
  5. Synthesizing the maximally permissive forcibly-controllable nonblocking supervisor
  6. Case study - small manufacturing line
  7. Case study - small factory
  8. Conclusions

Key Result

Theorem 1

Consider a plant $P$ and a specification $\varnothing \neq F \subseteq L_m(P)$. There exists a supervisory control $V : L(P) \rightarrow Pwr(\Sigma)$ such that $V/P$ is nonblocking and $L_m(V/P) = F$ iff $F$ is forcibly-controllable.

Figures (7)

  • Figure 1: Control mechanisms for supervisory control.
  • Figure 2: Comparisons among controllable, forcibly-controllable, and forcible sublanguages.
  • Figure 3: Automata for the machines and the specification in the small manufacturing line.
  • Figure 4: Automaton representing the synchronous product and, using colors as described in the text, three different supervisors.
  • Figure 5: Automata representing the machines $M_1$ and $M_2$ in the small factory.
  • ...and 2 more figures

Theorems & Definitions (22)

  • Definition 1: Nonblocking
  • Definition 2: Controllable sublanguage
  • Definition 3: Forcibly-controllable sublanguage
  • Definition 4: Forcible sublanguage
  • proof
  • Theorem 1
  • proof
  • Proposition 1
  • proof
  • Theorem 2
  • ...and 12 more