Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Similarity Control Problem with Required Events

Yu Wang, Zhaohui Zhu, Rob van Glabbeekd, Jinjin Zhang, Yixuan Li

TL;DR

The paper addresses ensuring that a supervised discrete event system satisfies both safety requirements and must-enable events specified in the model. It introduces covariant-contravariant simulation (cc-simulation) to capture these dual constraints and establishes a necessary-and-sufficient solvability condition via Sigma_ucr-controllability sets, along with a method to synthesize a maximally permissive supervisor. The approach unifies and extends existing similarity and bisimilarity control results, and provides constructive procedures for implementing supervisors that are both safe and compliant with required events. This yields practically relevant guarantees for DES supervision and clarifies the relationships to related control paradigms such as range control and state-controllability.

Abstract

In order to guarantee that a supervised system satisfies safety requirements of the specification, as well as requirements saying that in certain states certain events must be enabled, this paper introduces required events for discrete event systems and reconsiders the similarity control problem while taking all requirements from the specification into account. The notion of a covariant-contravariant simulation, which is finer than the conventional notion of simulation, is adopted to act as the behavioral relation of supervisory control theory. A necessary and sufficient condition for the solvability of this problem is established and a method for synthesizing a maximally permissive supervisor is provided.

The Similarity Control Problem with Required Events

TL;DR

The paper addresses ensuring that a supervised discrete event system satisfies both safety requirements and must-enable events specified in the model. It introduces covariant-contravariant simulation (cc-simulation) to capture these dual constraints and establishes a necessary-and-sufficient solvability condition via Sigma_ucr-controllability sets, along with a method to synthesize a maximally permissive supervisor. The approach unifies and extends existing similarity and bisimilarity control results, and provides constructive procedures for implementing supervisors that are both safe and compliant with required events. This yields practically relevant guarantees for DES supervision and clarifies the relationships to related control paradigms such as range control and state-controllability.

Abstract

In order to guarantee that a supervised system satisfies safety requirements of the specification, as well as requirements saying that in certain states certain events must be enabled, this paper introduces required events for discrete event systems and reconsiders the similarity control problem while taking all requirements from the specification into account. The notion of a covariant-contravariant simulation, which is finer than the conventional notion of simulation, is adopted to act as the behavioral relation of supervisory control theory. A necessary and sufficient condition for the solvability of this problem is established and a method for synthesizing a maximally permissive supervisor is provided.
Paper Structure (6 sections, 17 theorems, 46 equations, 11 figures)

This paper contains 6 sections, 17 theorems, 46 equations, 11 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. The Similarity Control Problem with Required Events
  4. Synthesis of Maximally Permissive Supervisors
  5. Relations to Other Control Problems
  6. Conclusion

Key Result

Lemma 7

Let $G$ and $R$ be two automata and let $E$ be a $\Sigma_{ucr}$-controllability set from $G$ to $R$. Then$\bigcup_{\widetilde{W}\in E}\raisebox{.15\baselineskip}{\Large$\wp$} (\widetilde{W})$ is a $\Sigma_{ucr}$-controllability set from $G$ to $R$. Moreover, for this $\Sigma_{ucr}$-controllable set,

Figures (11)

  • Figure 1: The plant $G$ (left) and specification $R$ (right)
  • Figure 2: The supervisor $S$ (left) and supervised system $S||G$ (right)
  • Figure 3: The plant $G$ (left), specification $R$ (middle) and reachable part of supervisor $\mathcal{A}(E)$ (right)
  • Figure 4: The reachable part of supervised system $\mathcal{A} (E)||G$
  • Figure 5: The plant $G$ (left) and specification $R$ (right)
  • ...and 6 more figures

Theorems & Definitions (33)

  • Definition 1
  • Definition 2
  • Definition 3
  • Example 4
  • Definition 5
  • Definition 6
  • Lemma 7
  • Definition 8
  • Example 9
  • Lemma 10
  • ...and 23 more