# Incremental Verification of Inference Observability in Decentralized Discrete-Event Control

S.H. Yoon, Laurie S. L. Ricker, Hervé Marchand

► To cite this version:

S.H. Yoon, Laurie S. L. Ricker, Hervé Marchand. Incremental Verification of Inference Observability in Decentralized Discrete-Event Control. ICCA 2025 - IEEE 19th International Conference on Control & Automation, Jun 2025, Taline, Estonia. pp.262-267, 10.1109/ICCA65672.2025.11129743. hal-05364720

HAL Id: hal-05364720

https://inria.hal.science/hal-05364720v1

Submitted on 14 Nov 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
# Incremental Verification of Inference Observability in Decentralized Discrete-Event Control

S.H. Yoon and S.L. Ricker and H. Marchand

**Abstract**— Inference observability is one of the properties that must be satisfied to synthesize solutions to decentralized supervisory control problems. Current verification strategies require the construction of the complete system model. However, when a system model consists of multiple components, these monolithic approaches may be computationally infeasible due to the state-space explosion problem, a situation that arises when the system's state space increases exponentially with the number of its components. Incremental verification algorithms have been proposed to navigate this issue, where verification occurs component-wise. Our proposed solution to this issue involves updating an algorithm for the incremental verification of co-observability and extending it to inference observability.

## I. INTRODUCTION

Decision-making architectures in discrete-event control feature a model of an uncontrolled system along with a specification of the ideal behavior of the system [1]. We assume the modeling approach of [2], where the system and its specified behavior are modeled with finite state automata. Often, a collection of models best describes the uncontrolled system and the specifications. In this case, the first step in verifying whether a control solution exists is to produce a monolithic view of the system and specification models by taking their product. The overall state space increases exponentially with the number of its components<fnref n="1" />. This phenomenon is commonly called the “state space explosion problem.”

To mitigate this problem, the idea of incremental verification algorithms has been proposed [3]. With this approach, verifying system properties is guided by the use of *counterexamples*, systematically considering each of the components of the system models instead of building the monolithic view. A counterexample is a scenario that represents possible violations of the property being verified.

We want to extend the incremental verification approach to round-based *inferencing* in decentralized decision-making architectures, e.g., [4], [5]. In this case, a decentralized agent makes control decisions by reasoning about what the other agents know. Based on information about correct decisions taken in previous rounds, each subsequent round of inferencing leads to some agent(s) definitively taking correct control decisions. The process continues until all control

decisions are correctly taken or no agents can correctly make the remaining control decisions.

Before inferencing, the primary decentralized property to verify was *co-observability* [1]. Co-observability is equivalent to zero rounds of inferencing [5]: either agents can make the correct control decisions immediately, or they cannot. An incremental algorithm to verify co-observability was proposed in [6], [7]. Here, we update the co-observability incremental verification algorithm from [6] to inferencing.

The paper is organized as follows. First, Section II establishes the notation and background on inferencing in decentralized discrete-event control. Then in Section III, we propose an alternate definition of inferencing that generalizes the one introduced in [4], which considered only one round of inferencing. With this new definition, in Section IV, we extend the propositions that underlie the incremental verification strategy of [6] from co-observability to a flavor of inference observability. In Section V, we present an updated version of the incremental verification algorithm of [6] as it pertains to inferencing. Finally, we demonstrate the algorithm with a small example.

## II. NOTATION

Let $\Sigma$ be a finite alphabet of events, $\Sigma^*$ be the set of words formed from elements of $\Sigma$, and $\varepsilon$ be the empty word. A language $L \subseteq \Sigma^*$ is a set of words over $\Sigma$.

A language $L \subseteq \Sigma^*$ is *prefix-closed*, denoted $\overline{L}$, if $\forall w \in L$ there exist two words, $u$ and $v$, such that $u \in L$ and $w = uv$, where $uv$ is the *concatenation* of $u$ and $v$. Unless otherwise stated, for the remainder of this paper, we will be considering prefix-closed languages only.

A deterministic finite automaton $M_L = (Q, \Sigma, T_L, q^t)$ is a 4-tuple, where $Q$ is a finite set of states, $\Sigma$ is the alphabet, $T_L \subseteq Q \times \Sigma^* \times Q$ is a deterministic transition relation closed under concatenation, and $q^t \in Q$ is the initial state. We say that $M_L$ recognizes $L$ if and only if $\forall w \in L$ there exists a state $q_k \in Q$ such that $(q^t, w, q_k) \in T_L$. A regular language is one recognized by a finite automaton.

A deterministic finite automaton $M_K = (Q_K, \Sigma, T_K, q_K^t)$ that recognizes regular language $K \subseteq \Sigma^*$ is a *sub-automaton* of $L$, denoted $M_K \subseteq M_L$, if $Q_K \subseteq Q$, $T_K \subseteq T_L$ and $q_K^t = q^t$. By definition, $K \subseteq L$.

We will also make use of a variant of $M_L$ that represents the joint automaton of $M_L$ and $M_K$ with the addition of self-loops of $\varepsilon$ at each state of $Q$. We denote this automaton by $M^\varepsilon = (Q, \Sigma^\varepsilon, T^\varepsilon, q^\varepsilon)$, where $\Sigma^\varepsilon := \Sigma \cup \{\varepsilon\}$, $T^\varepsilon := T_{L \setminus K} \cup T_K \cup \{(q, \varepsilon, q) \mid \forall q \in Q\}$ and $T_{L \setminus K} := T_L \setminus T_K$. We

<footnote>S.H. Yoon and S.L. Ricker are with the Department of Mathematics and Computer Science, Mount Allison University, Sackville NB, CANADA. Email: {syoon2, lricker}@mta.ca</footnote>

<footnote>H. Marchand is with the University of Rennes, Inria, CNRS and IRISA, Rennes, FRANCE herve.marchand@inria.fr</footnote>

<footnote n="1">¹The exact magnitude of the increase depends on the original system, and there exists no generalized formula that quantifies it.</footnote>
assume that, when necessary, we can determine membership of a transition $(q, \sigma, q') \in T^\epsilon$ in either $T_{L\setminus K}$ or $T_K$.

Given two deterministic finite automata $M_1 = (Q_1, \Sigma_1, T_1, q'_1)$ and $M_2 = (Q_2, \Sigma_2, T_2, q'_2)$, their synchronous product $M_1|M_2 := (Q_1 \times Q_2, \Sigma_1 \cup \Sigma_2, T, (q'_1, q'_2))$, where $((q_1, q_2), \sigma, (q'_1, q'_2)) \in T$ iff $((q_1, \sigma, q'_1) \in T_1 \wedge q_2 = q'_2 \wedge \sigma \in \Sigma_1 \setminus \Sigma_2)$ or $((q_2, \sigma, q'_2) \in T_2 \wedge q_1 = q'_1 \wedge \sigma \in \Sigma_2 \setminus \Sigma_1)$ or $((q_1, \sigma, q'_1) \in T_1 \wedge (q_2, \sigma, q'_2) \in T_2 \wedge \sigma \in \Sigma_1 \cap \Sigma_2)$.

### A. Decentralized Control Architectures

In decentralized discrete-event control architectures, there is a set of $n$ agents $I = \{1, \dots, n\}$ that cooperate to ensure that an uncontrolled system $M_L$ adheres to a given specification $M_K$. Each agent issues local control decisions to enable or disable events. These local decisions are combined with those from other agents to produce a final global decision.

To accommodate global control decisions, $\Sigma$ is partitioned into disjoint sets of controllable events $\Sigma_c$ and uncontrollable events $\Sigma_{uc}$. A language $K$ is controllable, with respect to (wrt) $L$ and $\Sigma_{uc}$, if $K\Sigma_{uc} \cap L \subseteq K$. Local control decisions require the further definition of a controllable alphabet for each agent $i \in I$, denoted $\Sigma_{c,i} \subseteq \Sigma_c$. We let $I_c(\sigma) := \{i \in I \mid \sigma \in \Sigma_{c,i}\}$.

Agents may not observe all the events in $\Sigma$ and, thus, make control decisions under conditions of partial observation. To facilitate partial observation of the system, as we did for control decisions, $\Sigma$ is partitioned into disjoint sets of observable events, denoted by $\Sigma_o$, and unobservable events, $\Sigma_{uo}$. The observable alphabet for agent $i \in I$, $\Sigma_{o,i} \subseteq \Sigma_o$ are events that $i$ can observe, where $\Sigma_o = \cup_{i \in I} \Sigma_{o,i}$. We expand the agent index set and let $I_0 := I \cup \{0\}$, and consider that agent 0 represents the observations of the system itself, where $\Sigma_{o,0} := \Sigma_o$. The natural projection defines the observations of a decentralized agent $i \in I_0$ by removing all occurrences of events in $\Sigma \setminus \Sigma_{o,i}$ from a word in $\Sigma^*$. Formally, $\pi_i: \Sigma^* \to \Sigma_{o,i}^*$, for $i \in I_0$, and we have $\pi_i(\epsilon) := \epsilon$ and

$$ \pi_i(w\sigma) := \begin{cases} \pi_i(w)\sigma, & \text{when } \sigma \in \Sigma_{o,i}; \\ \pi_i(w), & \text{otherwise.} \end{cases} $$

The inverse projection $\pi_i^{-1}: \Sigma_{o,i}^* \to 2^{\Sigma^*}$ is defined as $\pi_i^{-1}(w) := \{v \in \Sigma^* | \pi_i(v) = w\}$. We use $[w]_i$ to denote $\pi_i^{-1}\pi_i(w)$, for $i \in I_0$. For purposes of the verification algorithm, we further assume that $\Sigma_c \subseteq \Sigma_o$.

### B. Monolithic Verification of Inference Observability

We recently introduced a monolithic algorithm for verifying inference observability [8]. This algorithm relies on the following finite-state verification structure. The construction of the structure uses a special product we call synchronized composition, denoted by $\times_S$, and takes $n+1$ copies of $M^\epsilon$:

$$ \mathcal{U} = \underbrace{\mathcal{M}^{\epsilon} \times_S \mathcal{M}^{\epsilon} \times_S \dots \times_S \mathcal{M}^{\epsilon}}_{(n+1) \text{ times}} \\ = (Q_S, \Delta_S, T_S, q_S^t, D_{\Sigma_c}, E_{\Sigma_c}), $$

where

* $Q_S \subseteq Q^{n+1}$ is a set of state vectors;

* $\Delta_S \subseteq \Sigma^{n+1}$ is a set of vector labels [9];

* $T_S \subseteq Q_S \times \Delta_S \times Q_S$ is the transition relation defined as follows: $(q, \sigma, \hat{q}) \in T_S$ iff $\forall i \in I_0$, $(q_i, \sigma_i, \hat{q}_i) \in T^\epsilon$;

* $q_S^t = (q^t, q^t, \dots, q^t)$ is the initial state;

* $D_{\Sigma_c} := \cup_{\sigma \in \Sigma_c} \{d_\sigma | d_\sigma \in Q_S \text{ is an illegal disablement configuration wrt } \sigma\}$ (see Definition 1); and

* $E_{\Sigma_c} := \cup_{\sigma \in \Sigma_c} \{e_\sigma | e_\sigma \in Q_S \text{ is an illegal enablement configuration wrt } \sigma\}$.

State vectors $q \in Q_S$ have the form $q = (q_0, q_1, \dots, q_n)$, where $q_i \in Q$ ($i \in I_0$), whereas vector labels $\sigma \in \Delta_S$ have the form $\sigma = (\sigma_0, \sigma_1, \dots, \sigma_n)$, where $\sigma_i \in \Sigma^\epsilon$ ($i \in I_0$). We variously refer to the $j$th element of $q$ and $\sigma$ as $q(j)$ or $q_j$ and $\sigma(j)$ or $\sigma_j$, respectively, for $j \in I_0$.

Labels in $\Delta_S$ are partitioned into sets of observable labels $\Delta_o$ and unobservable labels $\Delta_{uo} := \cup_{i \in I_0} \Delta_{uo,i}$. We generate labels $\sigma \in \Delta_o$ as follows: $(\forall i \in I_0)(\forall \sigma \in \Sigma_o)\sigma(i) := \pi_i(\sigma)$. We generate labels $\sigma \in \Delta_{uo,i}$ as follows: $(\forall j \in I_0) \sigma(j) := \sigma$, if $j = i$; otherwise $\sigma(j) := \epsilon$. For convenience, we define the empty vector label $\epsilon$ as follows: $(\forall i \in I_0) \epsilon(i) := \epsilon$.

Let $\mathcal{L}(U)$ denote the language generated by $U$. Given a vector word $w = \sigma_0\sigma_1\dots\sigma_{|w|-1} \in \mathcal{L}(U)$, the word $w(i)$ formed by concatenating $\sigma_0(i)$ up to $\sigma_{|w|-1}(i)$ is a word in $L$. Further, by construction, $\pi_i(w(0)) = \pi_i(w(i))$ for all $i \in I$.

We identify states in $Q_S$, called illegal configurations, that represent potential (but not guaranteed) violations of inference observability. Specifically, we are interested in states where the expected control decision for some $\sigma \in \Sigma_c$ in the system is the opposite of what all the agents in $I_c(\sigma)$ believe the correct control decision to be.

Here we focus on illegal configurations that correspond to disablement decisions about some $\sigma \in \Sigma_c$. Although not used here, we can similarly define an illegal enablement configuration.

**Definition 1:** An illegal disablement configuration wrt $\sigma \in \Sigma_c$ is a state $d_\sigma = (q, q_1, \dots, q_n) \in Q_S$ such that $\exists (q', q'_1, \dots, q'_n) \in Q_S$ and $\exists \sigma \in \Sigma_c$ such that $(q, \sigma, q') \in T_L \setminus T_K$ while $(\forall i \in I_c(\sigma))(q_i, \sigma, q'_i) \in T_K$. We use $D_\sigma$ to denote the set of all illegal disablement configurations wrt $\sigma \in \Sigma_c$. Thus, $D_{\Sigma_c} = \cup_{\sigma \in \Sigma_c} D_\sigma$.

In Fig. 1 we demonstrate how to identify such an illegal configuration in $U$. Suppose we have some sequence

<figure><img src="image_2.png" /><figcaption>Fig. 1: Identifying an illegal disablement configuration wrt $\sigma$, $d_\sigma$, via $w\sigma \in \mathcal{L}(U)$. We use the color red to draw attention to the idea that $(q, \sigma, q') \notin T_K$ and a disablement decision is required for $\sigma$ at state $q$ in $M_L$.</figcaption></figure>
$w \in \mathcal{L}(\mathcal{U})$ such that $(q_S^t, w, q) \in T_S$, where $q = (q, q_1, \dots, q_i, \dots, q_n)$ such that $(q^t, w(0), q) \in T_K$ but $(q, \sigma, q') \in T_L \setminus T_K$ and for all $i \in I_c(\sigma)$ we have $(q^t, w(i), q_i) \in T_K$ and $(q_i, \sigma, q'_i) \in T_K$. This corresponds to some possible system behavior where the correct control decision is to disable $\sigma$, since $\sigma$ takes $w(0)$ out of $K$, but all the agents that control $\sigma$ consider that the system has generated some sequence where the occurrence of $\sigma$ keeps the system within $K$. Thus, the vector state $(q, q_1, \dots, q_n)$ is an illegal disablement configuration wrt $\sigma$ and is identified by $d_\sigma$ in Fig. 1.

### III. INFERENCE OBSERVABILITY

Solutions to control problems in decentralized architectures focus on two frameworks: *enable by default* (EBD) [1] and *disable by default* (DBD) [10]. In the EBD framework, the focus is on agents being able to make all the correct disablement decisions, and uncertainty leads to a default enablement decision. In contrast, the DBD framework focuses on agents being able to make all the correct enablement decisions. The default decision is to disable events in the face of uncertainty.

Interpreting the generalization of these frameworks for multi-level inferencing in the *control* domain is less straightforward because the objectives are contradictory. Under EBD, the goal is maximal specified behavior: everything is enabled until an agent “knows” to make a disablement decision. In contrast, under DBD, the system is inhibited as everything is disabled until an agent knows when to make an enablement decision. To circumvent these issues, we define inferencing separately for the EBD and DBD frameworks. Here we examine only EBD decision-making, with the understanding that results for the DBD framework are equivalently formulated.

Instead of using the inductive definition of inference observability from [5], we have chosen to generalize the definition of conditional co-observability<fnref n="2" /> from [4]. Below, we include the original definition from [4] to provide context for our more general Definition 3.

**Definition 2:** [Adapted from [4]] Let $K, L = \bar{L}$ be languages defined over $\Sigma$. A language $K$ is **conditionally co-observable** wrt $L$, $\pi_i$ and $\Sigma_{c,i}$, for $i \in I$, if there exist $i_0, i_1 \in I_c(\sigma)$, $i_0 \neq i_1$, such that

$$ 
\begin{align*}
(\forall w \in \bar{K} \cap L)(\forall \sigma \in \Sigma_c) w\sigma \in L \setminus \bar{K} &\Rightarrow \\
(\forall i_0 \in I_c(\sigma))[\![w]\!]_{i_0} \sigma \cap \bar{K} \cap L &\neq \emptyset \Rightarrow \\
(\exists i_0 \in I_c(\sigma))(\forall w_1 \in [w]\!]_{i_0} \sigma \cap \bar{K} \cap L) &\Rightarrow \\
(\exists i_1 \in I_c(\sigma))[\![w_1]\!]_{i_1} \sigma \cap L \setminus \bar{K} = \emptyset. &
\end{align*}
$$

Conditional co-observability has been shown to be equivalent to the definition of level 1 inference observability [5], which simply means that it takes a maximum of one round of inferencing to determine all the correct decisions. Here we generalize Definition 2 to apply to $m$ rounds of inferencing in the EBD framework, where $m \in 2^{\mathbb{N}_0}$.

**Definition 3:** Let $K, L = \bar{L}$ be languages defined over $\Sigma$. A language $K$ is **EBD inference observable** wrt $L$, $\pi_i$ and $\Sigma_{c,i}$, for $i \in I$, if there exists a natural number $m$ for every word $w\sigma$, for $w \in \bar{K}$, $\sigma \in \Sigma_c$ such that $w\sigma \in L \setminus \bar{K}$, that requires a disablement decision for $\sigma$, after $m$ rounds, there is a sequence of words $w_1, w_2, \dots, w_m \in \bar{K} \cap L$ and a sequence of agents $i_0, i_1, \dots, i_m \in I_c(\sigma)$, (where $i_j \neq i_{j+1}$ for $j \in \{0, \dots, m-1\}$) such that agent $i_m$ can definitively take the disablement decision for $\sigma$ after its partial observation of $w_m$.

$$ 
\begin{align*}
(\forall w \in \bar{K})(\forall \sigma \in \Sigma_c) w\sigma \in L \setminus \bar{K} &\Rightarrow \\
(\exists m \in 2^{\mathbb{N}_0}) &\Rightarrow \\
(\forall i_0 \in I_c(\sigma))[\![w]\!]_{i_0} \sigma \cap \bar{K} \cap L &\neq \emptyset \Rightarrow \\
(\exists i_0 \in I_c(\sigma))(\forall w_1 \sigma \in [w]\!]_{i_0} \sigma \cap \bar{K} \cap L) &\Rightarrow \\
(\forall i_1 \in I_c(\sigma))(\forall w_2 \sigma \in [w_1]\!]_{i_1} \sigma \cap L \setminus \bar{K}) &\Rightarrow \\
(\forall i_2 \in I_c(\sigma))[\![w_2]\!]_{i_2} \sigma \cap \bar{K} \cap L &\neq \emptyset \Rightarrow \\
\dots &\Rightarrow \\
(\forall i_{m-1} \in I_c(\sigma))[\![w_{m-1}]\!]_{i_{m-1}} \sigma \cap L \setminus \bar{K} &\neq \emptyset \Rightarrow \\
(\exists i_{m-1} \in I_c(\sigma))(\forall w_m \sigma \in [w_{m-1}]\!]_{i_{m-1}} \sigma \cap L \setminus \bar{K}) &\Rightarrow \\
(\exists i_m \in I_c(\sigma))[\![w_m]\!]_{i_m} \sigma \cap \bar{K} \cap L = \emptyset. &
\end{align*}
\tag{1}
$$

**Remark 1:** Definition 3 relies on distinguishing, at each step $j$, the existence of a specific agent $i_j \in I_c(\sigma)$ so that reaching the conclusion of inferencing the correct control decision is associated with a finite series of agents that contribute to the inferencing process.

### IV. INCREMENTAL INFERENCE

In many applications, automata are the starting point for modeling fragments of a large-scale system consisting of several composed and nested subsystems. Knowing that the number of states of the global system grows exponentially with the number of parallel subsystems will help us exploit some properties of decentralized discrete-event control architectures; we will consider them shortly.

The original incremental verification algorithm for co-observability assumed that the system and its specifications were defined over sets of automata [6]. The algorithm was based on a suite of propositions that demonstrated how co-observability was preserved across sub-language, intersection and super-language relationships between languages of system components and of specification components.

As pointed out in [6], a significant motivation for the original algorithm was the observation that the synchronous product of languages defined over a common alphabet is equivalent to taking the intersection of those languages. Thus, the role of language intersection plays an important role in the propositions from [6] that have been updated wrt inferencing in this section.

**Definition 3** permits us to perform straightforward updating of the propositions of [6], [7] from co-observability to inference observability, something that would not have

<footnote n="2">²We use the color red to distinguish words $w \in \bar{K} \cap L$ such that $\exists \sigma \in \Sigma_c$ and $w\sigma \in L \setminus \bar{K}$.</footnote>
been possible if we had used the definition of inferencing in [5]. Due to space restrictions, these proofs are omitted. For Propositions 3, 4 and 6, the updated proofs follow simply from the substitution of “EBD inference observable” for “co-observable”, and these proofs are omitted. For the remainder, they largely follow the logic of the originals and thus, their proofs are also omitted.

**Proposition 1:** Given languages $K, L_1 = \overline{L_1}$, and $L_2 = \overline{L_2}$ defined over $\Sigma$. If $K$ is EBD inference observable wrt $L_1$ and $L_2 \subseteq L_1$, then $K$ is EBD inference observable wrt $L_2$.

*Proof:* Assume that $K$ is EBD inference observable wrt $L_1$ and $L_2 \subseteq L_1$. We must show that $K$ is EBD inference observable wrt $L_2$.

Choose $w \in \overline{K} \cap L_2$ and $\sigma \in \Sigma_c$ such that $w\sigma \in L_2 \setminus \overline{K}$.

It is sufficient to show that there exists a finite sequence of $i \in I_c(\sigma)$ of length (at most) $m \in 2\mathbb{N}_0$, namely $i_0, i_1, \dots, i_m$ and a sequence of $w$ (chosen above), $w_1, w_2, \dots, w_{m-1}, w_m \in \overline{K} \cap L_2$ such that Eq. (1) is satisfied.

Since $L_2 \subseteq L_1$ and $w \in \overline{K} \cap L_2$, we have $w \in \overline{K} \cap L_1$. Since $w\sigma \in L_2 \setminus \overline{K}$, we have $w\sigma \in L_2$ and $w\sigma \notin \overline{K}$. This implies $w\sigma \in L_1$ and $w\sigma \notin \overline{K}$, as $L_2 \subseteq L_1$. This, in turn, implies $w\sigma \in L_1 \setminus \overline{K}$.

Now we have established that $w \in \overline{K} \cap L_1$ and $w\sigma \in L_1 \setminus \overline{K}$. Since $K$ is inference observable wrt $L_1$, we have a finite sequence of length $m \in 2\mathbb{N}_0$, namely $i_0, i_1, \dots, i_m$ and a sequence of words $w, w_1, w_2, \dots, w_{m-1}, w_m \in \overline{K} \cap L_1$ such that Eq. (1) is satisfied. Recall that we chose $w \in \overline{K} \cap L_2$. But we must examine the remaining $w_1, \dots, w_j, \dots, w_m$ to determine whether they, too, are in $\overline{K} \cap L_2$. There are two cases that we repeat for each $w_j \in w_1, \dots, w_m$, for $j \in \{1, \dots, m\}$:

**Corollary 1:** Given languages $K, L_1 = \overline{L_1}$, and $L_2 = \overline{L_2}$ defined over $\Sigma$. If $K$ is EBD inference observable wrt $L_1$, then $K$ is EBD inference observable wrt $L = L_1 \cap L_2$.

The success of the incremental verification strategy of inference observability also relies on whether or not the intersection of two inference-observable languages is inference observable.

**Proposition 2:** Let $K_1, K_2, L \subseteq \Sigma^*$ be prefix-closed. If $K_1$ and $K_2$ are both EBD inference observable wrt $L$, then $K_1 \cap K_2$ is EBD inference observable wrt $L$.

**Proposition 3:** Let $K_1, K_2, L_1, L_2 \subseteq \Sigma^*$ be prefix-closed. If $K_1$ is EBD inference observable wrt $L_1$ and $K_2$ is EBD inference observable wrt $L_2$, then $K = K_1 \cap K_2$ is EBD inference observable wrt $L = L_1 \cap L_2$.

Next, we note that any language is inference observable wrt all its sublanguages.

**Proposition 4:** Let $K, L \subseteq \Sigma^*$ be prefix-closed. If $K \supseteq L$, then $K$ is EBD inference observable wrt $L$.

Next, we examine whether intersection preserves inference observability.

**Proposition 5:** Let $K_1, K_2, L \subseteq \Sigma^*$ be prefix-closed. If $K_1$ is EBD inference observable wrt $L \cap K_2$ and $K_2$ is EBD

inference observable wrt $L$, then $K_1 \cap K_2$ is EBD inference observable wrt $L$.

**Proposition 6:** Let $K_1, K_2, L_1, L_2 \subseteq \Sigma^*$ be prefix-closed. If $K_1$ is EBD inference observable wrt $L_1 \cap K_2$ and $K_2$ is EBD inference observable wrt $L_2$, then $K = K_1 \cap K_2$ is EBD inference observable wrt $L = L_1 \cap L_2$.

**Proposition 7:** Let $K_1, K_2, L \subseteq \Sigma^*$ be prefix-closed. If $K_1$ is not EBD inference observable wrt $L \cap K_2$, then $K_1 \cap K_2$ is not EBD inference observable wrt $L$.

# V. INCREMENTAL INFERENCE OBSERVABILITY ALGORITHM

Incremental verification algorithms are guided by counterexamples [3]. In the context of the EBD decision-making framework of decentralized control, a counterexample represents a situation where the system has generated a word $w \in \overline{K} \cap L$ after which a disablement decision for some $\sigma \in \Sigma_c$ is required; however, all the agents capable of taking a control decision for $\sigma$ believe that an enablement decision is appropriate based on one explanation of their partial observation of word $w$.

**Definition 4:** (adapted from [6]) Let $K$ and $L = \overline{L}$ be languages defined over $\Sigma$. Let $\Sigma_{c,i} \subseteq \Sigma$ and $\Sigma_{o,i} \subseteq \Sigma$ be sets of controllable and observable events, and let $\pi_i: \Sigma^* \to \Sigma_{o,i}$ be natural projections, for $i \in \{1, \dots, n\}$. An EBD counterexample wrt $\sigma$, denoted by $c$, is a tuple

$$c = (\sigma, w, w_1, \dots, w_i, \dots, w_n),$$

where $\sigma \in \Sigma_c$; $w \in \overline{K} \cap L$ and $w\sigma \in L \setminus \overline{K}$; ($\forall i \in I_c(\sigma)$) $w_i\sigma \in \overline{K} \cap L$; and ($\forall i \in I_c(\sigma)$) $\pi_i(w) = \pi_i(w_i)$.

The discovery of a counterexample does not necessarily lead to a verdict of a language not being inference observable. A counterexample can be dismissed or rejected by either a system or a specification language.

**Definition 5:** (adapted from [7]) Given an EBD counterexample $c = (\sigma, w, w_1, \dots, w_i, \dots, w_n)$ we say that:

(a) $L$ rejects $c$ if $w\sigma \notin L$ or ($\exists i \in I_c(\sigma)$) $w_i\sigma \notin L$.

(b) $K$ rejects $c$ if $w \notin L$ or ($\exists i \in I_c(\sigma)$) $w_i\sigma \notin K$.

We can pinpoint a collection of sequences in a counterexample $c$ by examining the illegal disablement configurations of Definition 1 that have been identified during the construction of our verification structure $\mathcal{U}$. In this case, given an illegal configuration $d_\sigma \in Q_S$, for which $\exists w \in \mathcal{L}(\mathcal{U})$ where $(q_S, w, d_\sigma)(d_\sigma, \sigma, q') \in T_S$, we construct a counterexample $c(d_\sigma)$ as follows: $c(d_\sigma) = (\sigma, w(0), w(1), \dots, w(n))$. Algorithm 2 generates all counterexamples for the current set of examined system and specification components via our verification structure $\mathcal{U}$. Algorithm 3 indicates whether a given counterexample has been rejected or not by any of the rules of Algorithm 1. The role of Algorithm 1 has some focus (adapted from [6]): if each specification component $M_{K_j}$, for $j \in \{1, \dots, |M_K|\}$ is EBD inference observable wrt some $M_{L_r}$, for $r \in \{1, \dots, |M_L|\}$, then by Propositions 2 and 3, $\mathcal{L}(M_K)$ is EBD inference observable wrt $\mathcal{L}(M_L)$. Or suppose that only a subset $M'_K \subseteq M_K$ are EBD inference observable wrt a subset $M'_L \subseteq M_L$. Again, by Propositions 2 and 3, $\mathcal{L}(M'_K)$ is EBD inference observable wrt $\mathcal{L}(M_L)$. When

the current unexamined components.
<caption>**Algorithm 1 Incremental verification of EBD inference observability**</caption>

**Input:** $\mathbf{M}_L = \{M_{L_1}, M_{L_2}, \dots, M_{L_{|M_L|}}\}, \mathbf{M}_K = \{M_{K_1}, M_{K_2}, \dots, M_{K_{|M_K|}}\}$
**Output:** whether the system is inference observable
1: **procedure** ISINCREMENTALINFOBS($\mathbf{M}_L, \mathbf{M}_K$)
2: &nbsp;&nbsp;&nbsp;while $\mathbf{M}_K \neq \emptyset$ do
3: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Choose $M_{K_j} \in \mathbf{M}_K$, for $j \in \{1, \dots, |\mathbf{M}_K|\}$
4: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;M'_{K} \leftarrow \{M_{K_j}\}
5: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;M'_{L} \leftarrow \{M_{\Sigma^*}\} \triangleright M_{\Sigma^*} \text{ is the automaton such that } \mathcal{L}(M_{\Sigma^*}) = \Sigma^*$
6: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;\triangleright \mathcal{L}(M'_{K}) \text{ is the language of } M'_{K_1} \mid \dots \mid M'_{K_{|M'_{K}|}} \text{. Equivalently defined for } \mathcal{L}(M'_{L}) \triangleright
7: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;while $\mathcal{L}(M'_{K})$ is not inference observable w.r.t. $\mathcal{L}(M'_{L})$ do
8: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;C \leftarrow BUILD COUNTER EXAMPLES($M'_{L_1} \mid \dots \mid M'_{L_{|M'_{L}|}}, M'_{K_1} \mid \dots \mid M'_{K_{|M'_{K}|}}$)
9: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;found \leftarrow False
10: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;\triangleright \text{Select } c \in C \text{ that fits to heuristic ShortC or LongC the best.}
11: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;for all $\mathcal{M} \in (\mathbf{M}_L \setminus M'_{L}) \cup (\mathbf{M}_K \setminus M'_{K})$ do
12: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;\triangleright \text{A heuristic may be used to optimize the iteration order of this loop}
13: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;if $\neg$found \wedge TESTREJECT(c, $\mathcal{M}, \mathcal{M} \in \mathbf{M}_K \setminus M'_{K}$) then
14: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;found \leftarrow True
15: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;\text{if } \mathcal{M} \in \mathbf{M}_L \setminus M'_{L} \text{ then}
16: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;M'_{L} \leftarrow M'_{L} \cup \{\mathcal{M}\}
17: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;\text{else}
18: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;M'_{K} \leftarrow M'_{K} \cup \{\mathcal{M}\}
19: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;\text{if } \neg\text{found then}
20: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;\text{return False}
21: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;\text{M}_{K} \leftarrow \mathbf{M}_{K} \setminus M'_{K}
22: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;\text{M}_{L} \leftarrow \mathbf{M}_{L} \cup M'_{K}
23: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;\text{return True}

a component $\mathcal{M}_{K_j} \in \mathbf{M}_K$, for $j \in \{1, \dots, |\mathbf{M}_K|\}$, is EBD inference observable wrt some component of $\mathbf{M}_L$ then, by Propositions 5 and 6, $\mathcal{M}_{K_j}$ can be considered as a system component to be synchronized with the elements of $\mathbf{M}_L$. But when there is a counterexample that demonstrates that $\mathcal{M}_{K_j}$ is not EBD inference observable wrt $\mathbf{M}_L \parallel \mathcal{M}_{K_1} \parallel \dots \parallel \mathcal{M}_{K_{j-1}} \parallel \mathcal{M}_{K_{j+1}} \parallel \dots \parallel \mathcal{M}_{K_{|\mathbf{M}_K|}}$, then Proposition 7 confirms that $\mathcal{L}(\mathbf{M}_K)$ is not EBD inference observable wrt $\mathcal{L}(\mathbf{M}_L)$.

## VI. EXAMPLE

We demonstrate our algorithm on an example that features $I = \{1, 2\}$ and $\mathbf{M}_L = \{M_{L_1}, M_{L_2}, M_{L_3}\}$, as shown in Fig. 2, and $\mathbf{M}_K = \{M_{K_1}, M_{K_2}, M_{K_3}\}$, as shown in Fig. 3. We assume (even when not explicitly shown) self-loops of events in $\Sigma$ minus the events that appear in each automaton. For example, in $M_{L_1}$ each state has a self-loop of $\Sigma \setminus \{a_3, a_4, a_5, a_6, b_4, b_5, b_6\}$.

<caption>**Algorithm 2 Construct Counterexamples from Illegal Configurations**</caption>

**Input:** $\mathcal{M}_L, \mathcal{M}_K$
**Output:** Set of counterexamples $\mathcal{C}$
1: **function** BUILD COUNTER EXAMPLES($\mathcal{M}_L, \mathcal{M}_K$)
2: &nbsp;&nbsp;&nbsp;\triangleright \text{If } \mathcal{M}_K \not\subseteq \mathcal{M}_L, \text{ perform the appropriate operation to make this the case}
3: &nbsp;&nbsp;&nbsp;\triangleright \text{Construct } \mathcal{M}^\epsilon
4: &nbsp;&nbsp;&nbsp;\triangleright \text{Construct } \mathcal{U} \text{ from } \mathcal{M}^\epsilon
5: &nbsp;&nbsp;&nbsp;\mathcal{C} \leftarrow \emptyset \quad \triangleright \text{Initialize the set of counterexamples } \mathcal{C}
6: &nbsp;&nbsp;&nbsp;\triangleright \text{for all } \sigma \in \Sigma_c \text{ do}
7: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;\triangleright \text{Use illegal disablement configurations from } \mathcal{U} \text{ to populate } \mathcal{C}.
8: &nbsp;&nbsp;&nbsp;\triangleright \text{for all } \mathbf{d}_\sigma \in \mathcal{D}_\sigma \text{ do}
9: &nbsp;&nbsp;&nbsp;\triangleright \text{for all } w \in \mathcal{L}(\mathcal{U}) \text{ s.t. } (q_S^w, w, \mathbf{d}_\sigma) \in T_S \text{ do}
10: &nbsp;&nbsp;&nbsp;\triangleright \mathcal{C} \leftarrow \mathcal{C} \cup \{(\sigma, w(0), \dots, w(n))\}
11: &nbsp;&nbsp;&nbsp;\triangleright \text{return } \mathcal{C}

<caption>**Algorithm 3 Does Component $\mathcal{M}$ Reject Counterexample $c(d_\sigma)$**</caption>

**Input:** $c(d_\sigma) = (\sigma, w(0), w(1), \dots, w(n))$, component $\mathcal{M}$, boolean predicate isSpec that indicates if $\mathcal{M} \in \mathbf{M}_K \setminus M'_{K}$
**Output:** whether $\mathcal{M}$ rejects $c(d_\sigma)$
1: **function** TESTREJECT(c(d_\sigma), $\mathcal{M}$, isSpec)
2: &nbsp;&nbsp;&nbsp;\triangleright \mathcal{M}$ rejects $c(d_\sigma)$ if $\mathcal{M} \in \mathbf{M}_K \setminus M'_{K}$ and $w(0) \notin L(\mathcal{M})$, or $\mathcal{M} \in \mathbf{M}_L \setminus M'_{L}$ and $w(0)\sigma \notin L(\mathcal{M})$.
3: &nbsp;&nbsp;&nbsp;\triangleright \text{if } (\text{isSpec} \wedge w(0) \notin \mathcal{L}(\mathcal{M})) \vee (\neg \text{isSpec} \wedge w(0)\sigma \notin \mathcal{L}(\mathcal{M})) \text{ then}
4: &nbsp;&nbsp;&nbsp;\triangleright \text{return True}
5: &nbsp;&nbsp;&nbsp;\triangleright \mathcal{M}$ rejects $c(d_\sigma)$ if $(\exists i \in I_c(\sigma)) w(i) \notin \mathcal{L}(\mathcal{M})$.
6: &nbsp;&nbsp;&nbsp;\triangleright \text{for all } i \in I_c(\sigma) \text{ do}
7: &nbsp;&nbsp;&nbsp;\triangleright \text{if } w(i)\sigma \notin \mathcal{L}(\mathcal{M}) \text{ then}
8: &nbsp;&nbsp;&nbsp;\triangleright \text{return True}
9: &nbsp;&nbsp;&nbsp;\triangleright \text{return False}

We use Algorithm 1 to verify that the $\mathcal{L}(\mathcal{M}_K)$ is EBD inference observable wrt $\mathcal{L}(\mathcal{M}_L)$, where $\mathcal{M}_K = \mathcal{M}_{K_1} \parallel \mathcal{M}_{K_2} \parallel \mathcal{M}_{K_3}$ and $\mathcal{M}_L = \mathcal{M}_{L_1} \parallel \mathcal{M}_{L_2} \parallel \mathcal{M}_{L_3}$.

By Propositions 2 and 3, if the language of each of the specifications is EBD inference observable wrt $\mathcal{L}(\mathcal{M}_L)$, then the language of their product $\mathcal{L}(\mathcal{M}_K)$ is EBD inference observable wrt $\mathcal{L}(\mathcal{M}_L)$. Further, by Proposition 1, we need only consider a subsystem of $\mathcal{M}_L$ and not the entire $\mathcal{M}_L$.

We start with line 3 and arbitrarily choose to examine the specification automata in order. Subsequently, we have $M'_{K} \leftarrow \{\mathcal{M}_{K_1}\}$ and need to determine if it is EBD inference observable wrt the empty subset of $\mathbf{M}_L$, namely the automaton that generates $\Sigma$, denoted here by $\mathcal{M}_{\Sigma^*}$. Thus, $M'_{L} \leftarrow \{\mathcal{M}_{\Sigma^*}\}$. It is the case that $\mathcal{L}(\mathcal{M}_{K_1})$ is EBD inference observable wrt $\Sigma^*$.

By Proposition 1 and Corollary 1, we have that $\mathcal{L}(\mathcal{M}_{K_1})$ is EBD inference observable wrt $\mathcal{L}(\mathcal{M}_L)$.

In accordance with lines 21 and 22, we now have $\mathbf{M}_K = \{\mathcal{M}_{K_2}, \mathcal{M}_{K_3}\}$, $\mathbf{M}_L = \{M_{L_1}, M_{L_2}, M_{L_3}, M_{K_1}\}$.
<figure><img src="image_3.png" /><figcaption>Fig. 2: System components for the example; initial state denoted by entry arrow; $\Sigma_{o,1} = \{\mathbf{a}_1, \mathbf{a}_2, \mathbf{a}_3, \mathbf{a}_4, \mathbf{a}_5, \mathbf{a}_6, \sigma\}$, $\Sigma_{o,2} = \{\mathbf{b}_1, \mathbf{b}_2, \mathbf{b}_3, \mathbf{b}_4, \mathbf{b}_5, \mathbf{b}_6, \sigma\}$, $\Sigma_{c,1} = \Sigma_{c2} = \{\sigma\}$.</figcaption></figure>

<figure><img src="image_4.png" /><figcaption>Fig. 3: Specification components</figcaption></figure>

We return to line 3 and now choose $\mathcal{M}_{K_2}$. This time $M'_{K} \leftarrow \{\mathcal{M}_{K_2}\}$ and we need to determine if $\mathcal{L}(\mathcal{M}_{K_2})$ is EBD inference observable wrt $\Sigma^*$. It is the case that $\mathcal{L}(\mathcal{M}_{K_2})$ is EBD inference observable wrt $\Sigma^*$.

By Proposition 1 and Corollary 1, we have that $\mathcal{L}(\mathcal{M}_{K_1})$ is EBD inference observable wrt $\mathcal{L}(\mathcal{M}_L)$.

Finally, we continue to line 3 and now choose $\mathcal{M}_{K_3}$. This time $M'_{K} \leftarrow \{\mathcal{M}_{K_3}\}$. If $\mathcal{L}(\mathcal{M}_{K_3})$ is not EBD inference observable wrt $\Sigma^*$, then the loop at line 7 will determine the existence of counterexamples wrt the current set of elements in $M'_{K}$ and $M'_{L}$ and whether or not they are true counterexamples or not. The discovery of a true counterexample will terminate the algorithm and return a false verdict, indicating that the system is not EBD inference observable. However, it is the case that $\mathcal{L}(\mathcal{M}_{K_3})$ is EBD inference observable wrt $\Sigma^*$.

By Proposition 1 and Corollary 1, we have that $\mathcal{L}(\mathcal{M}_{K_3})$ is EBD inference observable wrt $\mathcal{L}(\mathcal{M}_L)$.

At this point, by lines 21 and 22, we have $\mathcal{M}_K = \emptyset$ while $\mathcal{M}_L = \{\mathcal{M}_{L_1}, \mathcal{M}_{L_2}, \mathcal{M}_{L_3}, \mathcal{M}_{K_1}, \mathcal{M}_{K_2}, \mathcal{M}_{K_3}\}$.

Since $\mathcal{L}(\mathcal{M}_{K_1})$ is EBD inference observable wrt $\mathcal{L}(\mathcal{M}_L)$, $\mathcal{L}(\mathcal{M}_{K_2})$ is EBD inference observable wrt $\mathcal{L}(\mathcal{M}_L)$, and $\mathcal{L}(\mathcal{M}_{K_3})$ is EBD inference observable wrt $\mathcal{L}(\mathcal{M}_L)$, we conclude that $\mathcal{L}(\mathcal{M}_{K_1}||\mathcal{M}_{K_2}||\mathcal{M}_{K_3}) = \mathcal{L}(\mathcal{M}_K)$ is EBD inference observable wrt $\mathcal{L}(\mathcal{M}_L)$.

We reach line 23 and Algorithm 1 returns True and terminates.

In this example, we determined that $\mathcal{M}_K$ was EBD inference observable wrt $\mathcal{M}_L$ without computing the entire product. In fact, we simply had to verify EBD inference

observability separately for each specification component.

## VII. DISCUSSION

The success of the algorithm relies on the ordering in which components are examined. In fact, there are two main ways that orderings affect the practical runtime of the algorithm:

* The ordering of system components. If the unchecked system components can be ordered in a way such that it minimizes the size growth of the product of checked components, then building the respective $\mathcal{U}$-structures will take shorter runtime, reducing the bottleneck effect.

* The ordering of counterexamples. If a counterexample is rejected by all remaining system components, it could be selected earlier. Then, the number of times to check whether a system component rejects the counterexample can be reduced before making a verdict.

To systematically organize the orderings, we may incorporate heuristics for counterexamples and system components [7], and future work includes verifying combinations of heuristics that provide maximal optimization.

An implementation of Algorithm 1 can be found in [11]. As far as computational complexity is concerned, in the worst case, we have to build $\mathcal{U}$ with respect to $\mathcal{M}_L$, where $\mathcal{M}_L$ is the synchronous product of all $r$ system components, e.g., $\mathcal{M}_L = \mathcal{M}_{L_1}||...||\mathcal{M}_{L_r}$.

## REFERENCES

[1] K. Rudie and W. Wonham, “Think globally, act locally: decentralized supervisory control,” *IEEE Trans. Autom. Control*, vol. 37, no. 11, pp. 1692–1708, 1992.
[2] P. J. Ramadge and W. M. Wonham, "Supervisory control of a class of discrete event processes," *SIAM J. Control Optim.*, vol. 25, no. 1, pp. 206-230, 1987.
[3] B. Brandin, R. Malik, and P. Malik, "Incremental verification and synthesis of discrete-event systems guided by counter examples," *IEEE Trans. Control Syst. Technol.*, vol. 12, no. 3, pp. 387-401, May 2004.
[4] T.-S. Yoo and S. Lafortune, "Decentralized supervisory control with conditional decisions: supervisor existence," *IEEE Trans. Autom. Control*, vol. 49, no. 11, pp. 1886-1904, Nov 2004.
[5] R. Kumar and S. Takai, "Inference-based ambiguity management in decentralized decision-making: Decentralized control of discrete event systems," *IEEE Trans. Autom. Control*, vol. 52, no. 10, pp. 1783-1794, 2007.
[6] H. Liu, R. J. Leduc, R. Malik, and S. L. Ricker, "Incremental verification of co-observability in discrete-event systems," in *Am. Control Conf.*, June 2014, pp. 5446-5452.
[7] H. Liu, "Hierarchical interface-based decentralized supervisory control," PhD, McMaster University, 2015. [Online]. Available: https://www.cas.mcmaster.ca/leduc/studThesis/hLiuPhdThesis15.html
[8] C. Sharpe, S. Yoon, S. Ricker, and H. Marchand, "A new verification algorithm for inferencing in supervisory control of discrete-event systems," *IFAC-PapersOnLine*, vol. 58, no. 1, pp. 102-107, 2024.
[9] A. Arnold, *Finite transition systems: semantics of communicating systems*. GBR: Prentice Hall, 1994.
[10] T.-S. Yoo and S. Lafortune, "Decentralized supervisory control: a new architecture with a dynamic decision fusion rule," in *Proc. Int. Workshop on Discrete Event Systems (WODES)*, Oct 2002, pp. 11-17.
[11] S. H. Yoon and M. Stairs, "JDec," 2015 - 2024. [Online]. Available: https://github.com/Summer2023SHY/JDec