Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Bounded-Time Nonblocking Supervisory Control of Timed Discrete-Event Systems

Renyuan Zhang, Jiale Wu, Junhua Gou, Yabo Zhu, Kai Cai

TL;DR

This work addresses time-bounded task completion in timed discrete-event systems by introducing bounded-time nonblockingness for tick-based models. It develops a two-tier synthesis framework: first computing supremal bounded-time completable sublanguages and then enforcing controllability to obtain maximally permissive supervisors, with a fixpoint algorithm for practical realization. The key contributions include the bounded-time completability concept, a formal BTNSCP solvability condition, and an automaton-based method to compute the supremal BTC sublanguage and the overall optimal supervisor. The approach provides provable guarantees for bounded-time task completion in industrial TDES applications, enabling timely safety-compliant supervisory control.

Abstract

Recently an automaton property of quantitative nonblockingness was proposed in supervisory control of untimed discrete-event systems (DES), which quantifies the standard nonblocking property by capturing the practical requirement that all tasks be completed within a bounded number of steps. However, in practice tasks may be further required to be completed in specific time. To meet this new requirement, in this paper we introduce the concept of bounded-time nonblockingness, which extends the concept of quantitative nonblockingness from untimed DES to timed DES. This property requires that each task must be completed within a bounded time counted by the number of ticks, rather than bounded number of transition steps in quantitative nonblockingness. Accordingly, we formulate a new bounded-time nonblocking supervisory control problem (BTNSCP) of timed DES, and characterize its solvability in terms of a new concept of bounded-time language completability. Then we present an approach to compute the maximally permissive solution to the new BTNSCP.

Bounded-Time Nonblocking Supervisory Control of Timed Discrete-Event Systems

TL;DR

This work addresses time-bounded task completion in timed discrete-event systems by introducing bounded-time nonblockingness for tick-based models. It develops a two-tier synthesis framework: first computing supremal bounded-time completable sublanguages and then enforcing controllability to obtain maximally permissive supervisors, with a fixpoint algorithm for practical realization. The key contributions include the bounded-time completability concept, a formal BTNSCP solvability condition, and an automaton-based method to compute the supremal BTC sublanguage and the overall optimal supervisor. The approach provides provable guarantees for bounded-time task completion in industrial TDES applications, enabling timely safety-compliant supervisory control.

Abstract

Recently an automaton property of quantitative nonblockingness was proposed in supervisory control of untimed discrete-event systems (DES), which quantifies the standard nonblocking property by capturing the practical requirement that all tasks be completed within a bounded number of steps. However, in practice tasks may be further required to be completed in specific time. To meet this new requirement, in this paper we introduce the concept of bounded-time nonblockingness, which extends the concept of quantitative nonblockingness from untimed DES to timed DES. This property requires that each task must be completed within a bounded time counted by the number of ticks, rather than bounded number of transition steps in quantitative nonblockingness. Accordingly, we formulate a new bounded-time nonblocking supervisory control problem (BTNSCP) of timed DES, and characterize its solvability in terms of a new concept of bounded-time language completability. Then we present an approach to compute the maximally permissive solution to the new BTNSCP.
Paper Structure (10 sections, 7 theorems, 23 equations, 11 figures, 1 table, 2 algorithms)

This paper contains 10 sections, 7 theorems, 23 equations, 11 figures, 1 table, 2 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries and Motivating Example
  3. Nonblocking Supervisory Control of TDES
  4. Motivating Example
  5. Bounded-Time Nonblocking Supervisory Control Problem Formulation
  6. Supremal Bounded-Time Completable Sublanguage and Its Computation
  7. Supremal Bounded-Time Completable Sublanguage
  8. Automaton-Based Computation of $\sup\mathcal{BTC}(K, ({Q_{m,i}}, N_i))$
  9. Maximally Permissive Bounded-Time Nonblocking Supervisory Control
  10. Conclusion and Future Work

Key Result

Theorem 1

Let $K\subseteq L_m({\bf G})$, $K \neq \emptyset$. There exists a nonblocking (marking) TDES supervisory control $V$ (for $(K, {\bf G})$) such that $L_m(V/{\bf G}) = K$ if and only if $K$ is controllable. Moreover, if such a nonblocking TDES supervisory control $V$ exists, then it may be implemented

Figures (11)

  • Figure 1: Routes of the vehicle
  • Figure 2: Transition graph of ${\bf G}_{act}$. In the transition graph, states 0, 2, 5, 8, and 11 represent that the vehicle stays at the area Z0, Z1, Z2, Z4 and Z3 respectively; other states represent that the vehicle is in the process of moving from one zone to the next, e.g. state 1 represents that the vehicle is in the process of moving from zone 0 to zone 1.
  • Figure 3: Transition graph of ${\bf G}$
  • Figure 4: Transition graph of $\bf SUP$
  • Figure 5: Transition graphs of ${\bf NG}$ and ${\bf NSPEC}$
  • ...and 6 more figures

Theorems & Definitions (14)

  • Theorem 1
  • Example 1
  • Remark 1
  • Definition 1
  • Definition 2
  • Proposition 1
  • Definition 3
  • Theorem 2
  • Proposition 2
  • Example 2: Continuing Example 2.2
  • ...and 4 more