Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On Prediction-Based Properties of Discrete-Event Systems: Notions, Applications and Supervisor Synthesis

Bohan Cui, Yu Chen, Alessandro Giua, Xiang Yin

TL;DR

This work develops a general framework for synthesizing property-enforcing supervisors in partially observed DES when the property depends on predicted future behavior. It introduces prediction-based properties, formalizes prediction vectors over a finite horizon $H$, and constructs an augmented information structure that borrows from future states to resolve future-dependency in synthesis. The main algorithm builds an IS-based control structure through expansion, pruning, and extraction steps, and is proven sound, complete, and maximally permissive, with exponential worst-case complexity inherent to partial observation. The framework subsumes scenarios such as $(M,K)$-pre-opacity and $(M,K)$-predictability, enabling active control to enforce or protect future information. This approach provides a flexible, generalizable toolkit for active prediction, fault prognosis, and intention-security applications in DES.

Abstract

In this work, we investigate the problem of synthesizing property-enforcing supervisors for partially-observed discrete-event systems (DES). Unlike most existing approaches, where the enforced property depends solely on the executed behavior of the system, here we consider a more challenging scenario in which the property relies on predicted future behaviors that have not yet occurred. This problem arises naturally in applications involving future information, such as active prediction or intention protection. To formalize the problem, we introduce the notion of prediction-based properties, a new class of observational properties tied to the system's future information. We demonstrate that this notion is very generic and can model various practical properties, including predictability in fault prognosis and pre-opacity in intention security. We then present an effective approach for synthesizing supervisors that enforce prediction-based properties. Our method relies on a novel information structure that addresses the fundamental challenge arising from the dependency between current predictions and the control policy. The key idea is to first borrow information from future instants and then ensure information consistency. This reduces the supervisor synthesis problem to a safety game in the information space. We prove that the proposed algorithm is both sound and complete, and the resulting supervisor is maximally permissive.

On Prediction-Based Properties of Discrete-Event Systems: Notions, Applications and Supervisor Synthesis

TL;DR

This work develops a general framework for synthesizing property-enforcing supervisors in partially observed DES when the property depends on predicted future behavior. It introduces prediction-based properties, formalizes prediction vectors over a finite horizon , and constructs an augmented information structure that borrows from future states to resolve future-dependency in synthesis. The main algorithm builds an IS-based control structure through expansion, pruning, and extraction steps, and is proven sound, complete, and maximally permissive, with exponential worst-case complexity inherent to partial observation. The framework subsumes scenarios such as -pre-opacity and -predictability, enabling active control to enforce or protect future information. This approach provides a flexible, generalizable toolkit for active prediction, fault prognosis, and intention-security applications in DES.

Abstract

In this work, we investigate the problem of synthesizing property-enforcing supervisors for partially-observed discrete-event systems (DES). Unlike most existing approaches, where the enforced property depends solely on the executed behavior of the system, here we consider a more challenging scenario in which the property relies on predicted future behaviors that have not yet occurred. This problem arises naturally in applications involving future information, such as active prediction or intention protection. To formalize the problem, we introduce the notion of prediction-based properties, a new class of observational properties tied to the system's future information. We demonstrate that this notion is very generic and can model various practical properties, including predictability in fault prognosis and pre-opacity in intention security. We then present an effective approach for synthesizing supervisors that enforce prediction-based properties. Our method relies on a novel information structure that addresses the fundamental challenge arising from the dependency between current predictions and the control policy. The key idea is to first borrow information from future instants and then ensure information consistency. This reduces the supervisor synthesis problem to a safety game in the information space. We prove that the proposed algorithm is both sound and complete, and the resulting supervisor is maximally permissive.

Paper Structure

This paper contains 26 sections, 6 theorems, 59 equations, 3 figures, 4 algorithms.

Table of Contents

  1. Introduction
  2. Motivations
  3. Our Results and Contributions
  4. Related Works
  5. Supervisor Control under Partial Observation
  6. Supervisor Control with Delayed Information
  7. Notions and Verification of Prediction-Based Properties
  8. Control Synthesis of Prediction-Based Properties
  9. Organization
  10. Preliminary
  11. System Model
  12. Supervisory Control
  13. Notions of Prediction-Based Properties
  14. State Predictions and Prediction-Based Properties
  15. Applications of Prediction-Based Properties
  16. ...and 11 more sections

Key Result

Proposition 1

Let ${\mathfrak{S}}$ be an IS-based control structure and $S:\Sigma_o^*\to \Gamma$ be its induced partial-observation supervisor. For each observation $\alpha\in P(\mathcal{L}(S/G))$, we have

Figures (3)

  • Figure 1: For $G$, we have $\Sigma_{o}=\{o_1,o_2\}$, $\Sigma_{c}=\{a,b,c\}$ and $X_S=\{7\}$.
  • Figure 2: Control Structure of $S_1$ in Figure \ref{['fig:G1']}.
  • Figure 3: Partial representation of structure ${\mathfrak{B}}$. Incomplete states are highlighted in red. The structure with all states complete is in the blue-lined box.

Theorems & Definitions (38)

  • Definition 1: Prediction Vectors
  • Definition 2: Prediction Sets
  • Example 1
  • Definition 3: Evaluation Functions
  • Definition 4: Prediction-Based Properties
  • Example 2
  • Example 3
  • Definition 5: ($M,K$)-Pre-Opacity
  • Definition 6: ($M,K$)-Predictability
  • Definition 7: ($M,K,m$)-Anonymity
  • ...and 28 more