# A New Verification Algorithm for Inferencing in
Supervisory Control of Discrete-Event Systems

C K Sharpe, S.H. Yoon, Laurie S. L. Ricker, Hervé Marchand

► To cite this version:

C K Sharpe, S.H. Yoon, Laurie S. L. Ricker, Hervé Marchand. A New Verification Algorithm for Inferencing in Supervisory Control of Discrete-Event Systems. 17th Ifac Workshop on Discrete Event Systems, Apr 2024, Rio De Janeiro, Brazil. hal-04581576

HAL Id: hal-04581576

https://inria.hal.science/hal-04581576

Submitted on 21 May 2024

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>

Distributed under a Creative Commons Attribution 4.0 International License
<figure><img src="image_1.png" /></figure>

HAL
open science

# A New Verification Algorithm for Inferencing in Supervisory Control of Discrete-Event Systems

C K Sharpe, S.H. Yoon, Laurie S. L. Ricker, Hervé Marchand

► To cite this version:

C K Sharpe, S.H. Yoon, Laurie S. L. Ricker, Hervé Marchand. A New Verification Algorithm for Inferencing in Supervisory Control of Discrete-Event Systems. 17th Ifac Workshop on Discrete Event Systems, Apr 2024, Rio De Janeiro, Brazil. hal-04581576

HAL Id: hal-04581576

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

Submitted on 21 May 2024

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_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# A New Verification Algorithm for Inferencing in Supervisory Control of Discrete-Event Systems

C.K. Sharpe* S.H. Yoon* S.L. Ricker* and H. Marchand**

* Mount Allison University, Sackville NB, CANADA(e-mail: {cksharpe,syoon2,lricker}@mta.ca).

** University of Rennes, Inria, CNRS and IRISA, Rennes, FRANCE (e-mail: herve.marchand@inria.fr).

**Abstract:** We present a new algorithm to verify inference observability in supervisory control of decentralized discrete-event systems. The algorithm's success relies on the following idea. An inferencing solution exists only when a language contains no *inferencing cycles*. When there are no cycles, the algorithm computes the smallest upper bound for an inferencing solution.

## 1. INTRODUCTION

Decentralized decision-making in supervisory control can involve direct knowledge of the correct control decision (Rudie and Wonham, 1992), a one-level inference about another agent's direct knowledge (Yoo and Lafortune, 2004) or multi-level inferencing involving multiple rounds of inferencing among the agents (Takai and Kumar, 2008). There are two decision-making architectures: *enable by default (EBD)*, where the focus is on agents who can make the correct “disable” decision, and *disable by default (DBD)*, which is concerned with agents who can make the correct “enable” decision. As Yoo and Lafortune (2004) noted, these architectures are incomparable. However, a general decision-making framework that combined the two in the context of diagnosis was presented in Takai and Kumar (2017).

The inferencing definition introduced by Takai and Kumar (2008) assumes the existence of two non-increasing sequences of regular languages defined over a set of controllable events. The first consists of words after which a disablement decision must occur for a given controllable event. The other has words after which an enablement decision must occur for the same controllable event. To have an *N*-level inferencing solution, at least one of these sequences of languages must eventually be empty in *N*+1 steps. Implicit in this definition is the assumption that multi-agent inferencing is defined only over finite languages up to self-loops.

A verification algorithm for the inferencing definition introduced by Takai and Kumar (2008) does not appear in the literature; however, Takai and Kumar (2017, 2018) introduce an algorithm to assert whether a pair of languages is *N*-inference *diagnosable*,<fnref n="1" /> where the user provides *N*. These algorithms hinge on the observation that establishing the non-emptiness after *N* rounds of inferencing of both of the sets of failure sequences and the non-failure sequences can be characterized as the existence of 2*k* + 1 traces in the language, where 1 ≤ *k* ≤ *N* + 1, which have specific relationships to each other. The algorithm is formulated for only two agents, while the authors claim that extending it to more than two agents is a straightforward exercise.

In particular, the algorithm's computational complexity depends largely on *N* and not the number of agents.

We are targeting the verification of inferencing in the control domain. Our state-based algorithm first asserts that an inferencing strategy exists, i.e., the existence of an upper bound on the number of rounds required to ensure that we take all the correct control decisions. The current version of our algorithm determines the feasibility of constructing a control solution by computing such a bound if it exists. Our algorithm can be further extended to calculate a set of offline state-based local and global control decisions by adapting the language-based strategy of Takai and Kumar (2008), which we do not present here.

Our algorithm uses a finite-state structure for verifying properties of decentralized architectures (Ricker and Marchand, 2013). Subsequently, we derive a bipartite graph from the states of this structure to examine the relationships between the bipartition of states where decentralized decision-makers must make disablement decisions and indistinguishable states where enablement decisions occur. In particular, when specific cycles are present in the bipartite graph, this corresponds to an inferencing cycle in which no agent can make the correct control decision or, equivalently, the lack of an inferencing bound.

The paper is organized as follows. First, Section 2 establishes the notation and background on inferencing in supervisory control. Then, in Section 3, we present the intuition behind our algorithm and review the finite structure (Ricker and Marchand, 2013) we use to determine if a system has an inferencing solution. Next, we present our algorithm in Section 4 and demonstrate it on an example that does not have an inferencing solution. Finally, we conclude the paper and discuss future extensions in Section 5.

## 2. NOTATION

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

Automata recognize words of a language, and an automaton is finite if it has a finite number of states. A deterministic finite automaton is a 5-tuple $M_L = (Q, \Sigma, T_L, q', F)$, where $Q$ is a finite set of states, $\Sigma$ is the alphabet, $q' \in Q$ is the initial state, $F \subseteq Q$ is a set of final states, and $T_L \subseteq Q \times \Sigma^* \times Q$ is a deterministic transition relation closed under concatenation.

<footnote n="1">¹ When applied to the diagnosis domain, the definition refers to two language sequences: failure sequences and non-failure sequences containing elements of a minimal length.</footnote>
# A New Verification Algorithm for Inferencing in Supervisory Control of Discrete-Event Systems

C.K. Sharpe* S.H. Yoon* S.L. Ricker* and H. Marchand**

* Mount Allison University, Sackville NB, CANADA(e-mail: {cksharpe,syoon2,lricker}@mta.ca).

** University of Rennes, Inria, CNRS and IRISA, Rennes, FRANCE (e-mail: herve.marchand@inria.fr).

**Abstract:** We present a new algorithm to verify inference observability in supervisory control of decentralized discrete-event systems. The algorithm's success relies on the following idea. An inferencing solution exists only when a language contains no *inferencing cycles*. When there are no cycles, the algorithm computes the smallest upper bound for an inferencing solution.

## 1. INTRODUCTION

Decentralized decision-making in supervisory control can involve direct knowledge of the correct control decision (Rudie and Wonham, 1992), a one-level inference about another agent's direct knowledge (Yoo and Lafortune, 2004) or multi-level inferencing involving multiple rounds of inferencing among the agents (Takai and Kumar, 2008). There are two decision-making architectures: *enable by default (EBD)*, where the focus is on agents who can make the correct “disable” decision, and *disable by default (DBD)*, which is concerned with agents who can make the correct “enable” decision. As Yoo and Lafortune (2004) noted, these architectures are incomparable. However, a general decision-making framework that combined the two in the context of diagnosis was presented in Takai and Kumar (2017).

The inferencing definition introduced by Takai and Kumar (2008) assumes the existence of two non-increasing sequences of regular languages defined over a set of controllable events. The first consists of words after which a disablement decision must occur for a given controllable event. The other has words after which an enablement decision must occur for the same controllable event. To have an *N*-level inferencing solution, at least one of these sequences of languages must eventually be empty in *N*+1 steps. Implicit in this definition is the assumption that multi-agent inferencing is defined only over finite languages up to self-loops.

A verification algorithm for the inferencing definition introduced by Takai and Kumar (2008) does not appear in the literature; however, Takai and Kumar (2017, 2018) introduce an algorithm to assert whether a pair of languages is *N*-inference *diagnosable*,<fnref n="1" /> where the user provides *N*. These algorithms hinge on the observation that establishing the non-emptiness after *N* rounds of inferencing of both of the sets of failure sequences and the non-failure sequences can be characterized as the existence of 2*k* + 1 traces in the language, where 1 ≤ *k* ≤ *N* + 1, which have specific relationships to each other. The algorithm is formulated for only two agents, while the authors claim that extending it to more than two agents is a straightforward exercise.

In particular, the algorithm's computational complexity depends largely on *N* and not the number of agents.

We are targeting the verification of inferencing in the control domain. Our state-based algorithm first asserts that an inferencing strategy exists, i.e., the existence of an upper bound on the number of rounds required to ensure that we take all the correct control decisions. The current version of our algorithm determines the feasibility of constructing a control solution by computing such a bound if it exists. Our algorithm can be further extended to calculate a set of offline state-based local and global control decisions by adapting the language-based strategy of Takai and Kumar (2008), which we do not present here.

Our algorithm uses a finite-state structure for verifying properties of decentralized architectures (Ricker and Marchand, 2013). Subsequently, we derive a bipartite graph from the states of this structure to examine the relationships between the bipartition of states where decentralized decision-makers must make disablement decisions and indistinguishable states where enablement decisions occur. In particular, when specific cycles are present in the bipartite graph, this corresponds to an inferencing cycle in which no agent can make the correct control decision or, equivalently, the lack of an inferencing bound.

The paper is organized as follows. First, Section 2 establishes the notation and background on inferencing in supervisory control. Then, in Section 3, we present the intuition behind our algorithm and review the finite structure (Ricker and Marchand, 2013) we use to determine if a system has an inferencing solution. Next, we present our algorithm in Section 4 and demonstrate it on an example that does not have an inferencing solution. Finally, we conclude the paper and discuss future extensions in Section 5.

## 2. NOTATION

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

Automata recognize words of a language, and an automaton is finite if it has a finite number of states. A deterministic finite automaton is a 5-tuple $M_L = (Q, \Sigma, T_L, q', F)$, where $Q$ is a finite set of states, $\Sigma$ is the alphabet, $q' \in Q$ is the initial state, $F \subseteq Q$ is a set of final states, and $T_L \subseteq Q \times \Sigma^* \times Q$ is a deterministic transition relation closed under concatenation.

<footnote n="1">¹ When applied to the diagnosis domain, the definition refers to two language sequences: failure sequences and non-failure sequences containing elements of a minimal length.</footnote>
Hence, $\forall q_i, q_j, q_k \in Q$ and $\forall \sigma \in \Sigma$, if $(q_i, \sigma, q_j) \in T_L$ and $(q_i, \sigma, q_k) \in T_L$ then $q_j = q_k$. We say that a word $w$ is accepted by $\mathcal{M}_L$ if $(q', w, q_k) \in T_L$ and $q_k \in F$. The regular language $L$ recognized by $\mathcal{M}_L$ is the set of words accepted by $\mathcal{M}_L$. An automaton $\mathcal{M}_K = (Q_K, \Sigma, T_K, q'_K, F_K)$ that recognizes regular language $K$ is a sub-automaton of $\mathcal{M}_L$ and we write $\mathcal{M}_K \subseteq \mathcal{M}_L$ if $Q_K \subseteq Q \wedge T_K \subseteq T_L \wedge F_K \subseteq F \wedge q'_K = q'$. Subsequently, $K \subseteq L$.

A language $L \subseteq \Sigma^*$ is prefix-closed if for all words $w \in L$ and any words $u, v$ satisfying $w = uv$, we have that $u \in L$. Throughout this work, we will be considering only prefix-closed languages. Thus, all states are final, and we will omit further reference to $F$ in our automaton notation.

In the context of decentralized discrete-event control, which is our focus here, there is a set of $n$ agents $I = \{1, \dots, n\}$ that cooperate to ensure that an uncontrolled system $\mathcal{M}_L$ adheres to a given specification $\mathcal{M}_K$. We further assume, without loss of generality, that $\mathcal{M}_K \subseteq \mathcal{M}_L$. Each agent issues local control decisions combined with those of other agents to produce a global decision to enable or disable events.

To facilitate partial observation, we partition the alphabet $\Sigma$ into disjoint sets of observable events $\Sigma_o$ and unobservable events $\Sigma_{uo}$. We further define observable sub-alphabets $\Sigma_{o,i}$ (not necessarily disjoint) for each agent $i \in I$, where $\Sigma_{o,i} \subseteq \Sigma_o$, and $\Sigma_o := \cup_{i \in I} \Sigma_{o,i}$. Later, we will refer to agent 0 and expand the agent index set: $I_0 = I \cup \{0\}$, where $\Sigma_{0,0} := \Sigma_o$. The natural projection $\pi_i : \Sigma^* \to \Sigma_{o,i}^*$ defines the observations of an agent $i \in I_0$ by removing all occurrences of events in $\Sigma \setminus \Sigma_{o,i}$ from a word in $\Sigma^*$. Specifically, $\pi_i(\varepsilon) := \varepsilon$ and for $s \in \Sigma^*$, $\pi_i(s\sigma) := \begin{cases} \pi_i(s)\sigma & \text{when } \sigma \in \Sigma_{o,i} \\ \pi_i(s) & \text{otherwise} \end{cases}$. The inverse projection is defined as follows: $(\forall w \in \Sigma_{o,i}^*) \pi_i^{-1}(w) := \{v \in \Sigma^* | \pi_i(v) = w\}$. We use $[[w]]_i$ to denote $\pi_i^{-1}\pi_i(w) \cap L$, for $i \in I_0$.

Similarly, for control purposes, $\Sigma$ is partitioned into controllable events $\Sigma_c$ and uncontrollable events $\Sigma_{uc}$. We define controllable sub-alphabets $\Sigma_{c,i}$ for each agent $i \in I$, where $\Sigma_{c,i} \subseteq \Sigma_c$. To identify the agents that control an event $\sigma \in \Sigma_c$, we use the notation $I_c(\sigma) = \{i \in I | \sigma \in \Sigma_{c,i}\}$.

## 2.1 Inference observability

The approach to inferencing, as proposed by Kumar and Takai (2007), requires the construction of two non-increasing sequences of prefix-closed languages with respect to (w.r.t.) the subset relation (Rabin and Scott, 1959), corresponding to words after which a controllable event must be disabled<fnref n="2" /> and words after which a controllable event must be enabled. Thus, for all $\sigma \in \Sigma_c$:

$$D_0(\sigma) = \{w \in K : w\sigma \notin K\}; \quad (1)$$

$$E_0(\sigma) = \{w \in K : w\sigma \in K\}. \quad (2)$$

Intuitively, $D_0(\sigma)$ is the set of all words in $K$ after which $\sigma$ must be disabled to keep the system within $K$, and $E_0(\sigma)$ is the set of all words in $K$ after which $\sigma$ must/can be enabled.

Each subsequent round of reasoning (for $k \ge 0$) is inductively defined<fnref n="3" /> as follows:

$$D_{k+1}(\sigma) = D_k(\sigma) \cap (\cap_{i \in I_c(\sigma)} [[E_k(\sigma)]]_i); \quad (3)$$

$$E_{k+1}(\sigma) = E_k(\sigma) \cap (\cap_{i \in I_c(\sigma)} [[D_k(\sigma)]]_i). \quad (4)$$

Remember that $[[E_k(\sigma)]]_i$ is the set of words that are indistinguishable from $E_k(\sigma)$ w.r.t. $\Sigma_{o,i}$ for agents $i \in I_c(\sigma)$ during round $k$. By taking the intersection of these sets across all $i \in I_c(\sigma)$ with $D_k(\sigma)$, we have the list of disablement decisions w.r.t. $\sigma$ for which no agent has yet inferred the correct disablement decision. And equivalently for $[[D_k(\sigma)]]_i$.

**Definition 1.** (Takai and Kumar (2008)). Let $K \subseteq L$ be a specification language defined w.r.t. system language $L$, and $\Sigma_{o,i}, \Sigma_{c,i}$ be the sets of observable and controllable events defined for agents $i \in I$. If there exists an upper bound $N \in \mathbb{N}_0$, for all $\sigma \in \Sigma_c$, such that $D_{N+1}(\sigma) = \emptyset$ or $E_{N+1}(\sigma) = \emptyset$, then $K$ is N-inference observable w.r.t. $L, \Sigma_{o,i}, \Sigma_{c,i}$, for $i \in I$.

Thus, when $K$ is not N-inference observable, then $\exists \sigma \in \Sigma_c$ such that $D_{N+1}(\sigma) \neq \emptyset$ and $E_{N+1}(\sigma) \neq \emptyset$. For the remainder of this paper, we say $K$ is inference observable w.r.t. $L$ if $\exists N \in \mathbb{N}_0$ satisfying Def. 1.

**Example 2.** Consider the example in Fig. 1, noting that the solid line transitions indicate transitions in $T_K$, whereas the dashed line transition is in $T_L \setminus T_K$.

<figure><img src="image_2.png" /><figcaption>Fig. 1. Joint $\mathcal{M}_L$ (all transitions) and $\mathcal{M}_K$ (only solid-line transitions) for Ex. 2 where $n = 2, \Sigma_{o,1} = \{a_1, a_2\}, \Sigma_{o,2} = \{b_1, b_2\}$, and $I_c(\sigma) = \{1, 2\}$.</figcaption></figure>

By Eqs (1)-(4), this system is not inference observable:

$$D_0(\sigma) = \{a_1 b_2, a_2 b_1\}, \quad E_0(\sigma) = \{a_1 b_1, a_2 b_2\};$$

$$D_1(\sigma) = D_0(\sigma), \quad E_1(\sigma) = E_0(\sigma). \quad \blackdiamond$$

<figure><img src="image_3.png" /></figure>

Finally, we introduce notation that will be used in the sequel. Let $R$ be a finite set $\{1, 2, \dots, r\}$ and $\rho(R)$ be a permutation of the set $R$ of length $|R|$. We refer to the $j$th element of $\rho(R)$ as $[\rho(R)]_j$, for $j \in I$. Given two permutations of $R$, namely $\rho_1(R)$ and $\rho_2(R)$, we denote their concatenation by $\rho_1(R)\rho_2(R)$.

## 3. A FINITE-STATE VERIFICATION STRUCTURE

We use the finite-state verification structure for decentralized architectures described in Ricker and Marchand (2013). Its construction uses a special product called synchronized composition, denoted by $\times_S$. Specifically, we take $n+1$ copies of $\mathcal{M}_L^\epsilon$, which is simply $\mathcal{M}_L$ augmented with self-loops of $\epsilon$ at each state:

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

where $Q_S \subseteq Q^{n+1}$ is a set of state vectors of the form $q = (q_0, q_1, \dots, q_n)$; $\Delta_S \subseteq \Sigma^{n+1}$ is a set of vector labels (Arnold, 1994) of the form $\sigma = (\sigma_0, \sigma_1, \dots, \sigma_i, \dots, \sigma_n)$; the transition relation $T_S \subseteq Q_S \times \Delta_S \times Q_S$ is 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_L^\epsilon$, where $T_L^\epsilon$ is the transition

<footnote n="2">² In the sequel, we use the color red to distinguish words $w \in K$ such that $\exists \sigma \in \Sigma_c$ and $w\sigma \in L \setminus K$.</footnote>

<footnote n="3">³ In Kumar and Takai (2007), the more general mask is used instead of natural projection.</footnote>
Hence, $\forall q_i, q_j, q_k \in Q$ and $\forall \sigma \in \Sigma$, if $(q_i, \sigma, q_j) \in T_L$ and $(q_i, \sigma, q_k) \in T_L$ then $q_j = q_k$. We say that a word $w$ is accepted by $\mathcal{M}_L$ if $(q', w, q_k) \in T_L$ and $q_k \in F$. The regular language $L$ recognized by $\mathcal{M}_L$ is the set of words accepted by $\mathcal{M}_L$. An automaton $\mathcal{M}_K = (Q_K, \Sigma, T_K, q'_K, F_K)$ that recognizes regular language $K$ is a sub-automaton of $\mathcal{M}_L$ and we write $\mathcal{M}_K \subseteq \mathcal{M}_L$ if $Q_K \subseteq Q \wedge T_K \subseteq T_L \wedge F_K \subseteq F \wedge q'_K = q'$. Subsequently, $K \subseteq L$.

A language $L \subseteq \Sigma^*$ is prefix-closed if for all words $w \in L$ and any words $u, v$ satisfying $w = uv$, we have that $u \in L$. Throughout this work, we will be considering only prefix-closed languages. Thus, all states are final, and we will omit further reference to $F$ in our automaton notation.

In the context of decentralized discrete-event control, which is our focus here, there is a set of $n$ agents $I = \{1, \dots, n\}$ that cooperate to ensure that an uncontrolled system $\mathcal{M}_L$ adheres to a given specification $\mathcal{M}_K$. We further assume, without loss of generality, that $\mathcal{M}_K \subseteq \mathcal{M}_L$. Each agent issues local control decisions combined with those of other agents to produce a global decision to enable or disable events.

To facilitate partial observation, we partition the alphabet $\Sigma$ into disjoint sets of observable events $\Sigma_o$ and unobservable events $\Sigma_{uo}$. We further define observable sub-alphabets $\Sigma_{o,i}$ (not necessarily disjoint) for each agent $i \in I$, where $\Sigma_{o,i} \subseteq \Sigma_o$, and $\Sigma_o := \cup_{i \in I} \Sigma_{o,i}$. Later, we will refer to agent 0 and expand the agent index set: $I_0 = I \cup \{0\}$, where $\Sigma_{0,0} := \Sigma_o$. The natural projection $\pi_i : \Sigma^* \to \Sigma_{o,i}^*$ defines the observations of an agent $i \in I_0$ by removing all occurrences of events in $\Sigma \setminus \Sigma_{o,i}$ from a word in $\Sigma^*$. Specifically, $\pi_i(\varepsilon) := \varepsilon$ and for $s \in \Sigma^*$,
$$ \pi_i(s\sigma) := \begin{cases} \pi_i(s)\sigma & \text{when } \sigma \in \Sigma_{o,i} \\ \pi_i(s) & \text{otherwise} \end{cases} $$
The inverse projection is defined as follows: $(\forall w \in \Sigma_{o,i}^*) \pi_i^{-1}(w) := \{v \in \Sigma^* | \pi_i(v) = w\}$. We use $[[w]]_i$ to denote $\pi_i^{-1}\pi_i(w) \cap L$, for $i \in I_0$.

Similarly, for control purposes, $\Sigma$ is partitioned into controllable events $\Sigma_c$ and uncontrollable events $\Sigma_{uc}$. We define controllable sub-alphabets $\Sigma_{c,i}$ for each agent $i \in I$, where $\Sigma_{c,i} \subseteq \Sigma_c$. To identify the agents that control an event $\sigma \in \Sigma_c$, we use the notation $I_c(\sigma) = \{i \in I | \sigma \in \Sigma_{c,i}\}$.

## 2.1 Inference observability

The approach to inferencing, as proposed by Kumar and Takai (2007), requires the construction of two non-increasing sequences of prefix-closed languages with respect to (w.r.t.) the subset relation (Rabin and Scott, 1959), corresponding to words after which a controllable event must be disabled<fnref n="2" /> and words after which a controllable event must be enabled. Thus, for all $\sigma \in \Sigma_c$:

$$ D_0(\sigma) = \{w \in K : w\sigma \notin K\}; \quad (1) $$

$$ E_0(\sigma) = \{w \in K : w\sigma \in K\}. \quad (2) $$

Intuitively, $D_0(\sigma)$ is the set of all words in $K$ after which $\sigma$ must be disabled to keep the system within $K$, and $E_0(\sigma)$ is the set of all words in $K$ after which $\sigma$ must/can be enabled.

Each subsequent round of reasoning (for $k \ge 0$) is inductively defined<fnref n="3" /> as follows:

$$ D_{k+1}(\sigma) = D_k(\sigma) \cap (\cap_{i \in I_c(\sigma)} [[E_k(\sigma)]]_i); \quad (3) $$

$$ E_{k+1}(\sigma) = E_k(\sigma) \cap (\cap_{i \in I_c(\sigma)} [[D_k(\sigma)]]_i). \quad (4) $$

Remember that $[[E_k(\sigma)]]_i$ is the set of words that are indistinguishable from $E_k(\sigma)$ w.r.t. $\Sigma_{o,i}$ for agents $i \in I_c(\sigma)$ during round $k$. By taking the intersection of these sets across all $i \in I_c(\sigma)$ with $D_k(\sigma)$, we have the list of disablement decisions w.r.t. $\sigma$ for which no agent has yet inferred the correct disablement decision. And equivalently for $[[D_k(\sigma)]]_i$.

**Definition 1.** (Takai and Kumar (2008)). Let $K \subseteq L$ be a specification language defined w.r.t. system language $L$, and $\Sigma_{o,i}, \Sigma_{c,i}$ be the sets of observable and controllable events defined for agents $i \in I$. If there exists an upper bound $N \in \mathbb{N}_0$, for all $\sigma \in \Sigma_c$, such that $D_{N+1}(\sigma) = \emptyset$ or $E_{N+1}(\sigma) = \emptyset$, then $K$ is N-inference observable w.r.t. $L, \Sigma_{o,i}, \Sigma_{c,i}$, for $i \in I$.

Thus, when $K$ is not N-inference observable, then $\exists \sigma \in \Sigma_c$ such that $D_{N+1}(\sigma) \neq \emptyset$ and $E_{N+1}(\sigma) \neq \emptyset$. For the remainder of this paper, we say $K$ is inference observable w.r.t. $L$ if $\exists N \in \mathbb{N}_0$ satisfying Def. 1.

**Example 2.** Consider the example in Fig. 1, noting that the solid line transitions indicate transitions in $T_K$, whereas the dashed line transition is in $T_L \setminus T_K$.

<figure><img src="image_3.png" /><figcaption>Fig. 1. Joint $\mathcal{M}_L$ (all transitions) and $\mathcal{M}_K$ (only solid-line transitions) for Ex. 2 where $n = 2, \Sigma_{o,1} = \{a_1, a_2\}, \Sigma_{o,2} = \{b_1, b_2\}$, and $I_c(\sigma) = \{1, 2\}$.</figcaption></figure>

By Eqs (1)-(4), this system is not inference observable:

$$ D_0(\sigma) = \{a_1 b_2, a_2 b_1\}, \quad E_0(\sigma) = \{a_1 b_1, a_2 b_2\}; $$

$$ D_1(\sigma) = D_0(\sigma), \quad E_1(\sigma) = E_0(\sigma). \quad \blackdiamond $$

Finally, we introduce notation that will be used in the sequel. Let $R$ be a finite set $\{1, 2, \dots, r\}$ and $\rho(R)$ be a permutation of the set $R$ of length $|R|$. We refer to the $j$th element of $\rho(R)$ as $[\rho(R)]_j$, for $j \in I$. Given two permutations of $R$, namely $\rho_1(R)$ and $\rho_2(R)$, we denote their concatenation by $\rho_1(R)\rho_2(R)$.

## 3. A FINITE-STATE VERIFICATION STRUCTURE

We use the finite-state verification structure for decentralized architectures described in Ricker and Marchand (2013). Its construction uses a special product called synchronized composition, denoted by $\times_S$. Specifically, we take $n+1$ copies of $\mathcal{M}_L^\epsilon$, which is simply $\mathcal{M}_L$ augmented with self-loops of $\epsilon$ at each state:

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

where $Q_S \subseteq Q^{n+1}$ is a set of state vectors of the form $q = (q_0, q_1, \dots, q_n)$; $\Delta_S \subseteq \Sigma^{n+1}$ is a set of vector labels (Arnold, 1994) of the form $\sigma = (\sigma_0, \sigma_1, \dots, \sigma_i, \dots, \sigma_n)$; the transition relation $T_S \subseteq Q_S \times \Delta_S \times Q_S$ is 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_L^\epsilon$, where $T_L^\epsilon$ is the transition

<footnote n="2">² In the sequel, we use the color red to distinguish words $w \in K$ such that $\exists \sigma \in \Sigma_c$ and $w\sigma \in L \setminus K$.</footnote>

<footnote n="3">³ In Kumar and Takai (2007), the more general mask is used instead of natural projection.</footnote>
relation for $\mathcal{M}_L^\epsilon$; and, the initial state $q_S^l = (q^l, q^i, ..., q^l)$. The $j$th element of $q$ and $\sigma$ are referred to as $q(j)$ or $q_j$ and $\sigma(j)$ or $\sigma_j$, respectively, for $j \in \{0, 1, ..., n\}$. We can extend $T_S$ to be defined over $\Delta_S^*$. As a result, we have a word $v = \sigma_0\sigma_1...\sigma_{|v|-1}$ in the language generated by $\mathcal{U}$ that consists of a vector of words in $L: v(0) = \sigma_0(0)\sigma_1(0)...\sigma_{|v|-1}(0), v(1) = \sigma_0(1)\sigma_1(1)...\sigma_{|v|-1}(1), ..., v(n) = \sigma_0(n)\sigma_1(n)...\sigma_{|v|-1}(n)$ where, by construction, $\pi_i(v(0)) = \pi_i(v(i))$, for all $i \in I$.

Labels in $\Delta_S$ are partitioned into sets of observable labels $\Delta_o$ and unobservable labels $\Delta_{uo}$. For $\sigma \in \Sigma_o$, the corresponding label in $\Delta_o$ has the form $\sigma := \langle \pi_0(\sigma), \pi_1(\sigma), ..., \pi_n(\sigma) \rangle$. Unobservable labels are created for each $i \in I_0$. If $\sigma \in \Sigma \setminus \Sigma_{o,i}$, the unobservable label in $\Delta_{uo,i}$ is assembled as follows: $\sigma(i) = \sigma$, while for all $j \in I_0 \setminus \{i\}$ we have $\sigma(j) = \epsilon$. Then $\Delta_{uo} = \bigcup_{i \in I_0} \Delta_{uo,i} = \Delta_S \setminus \Delta_o$. We also define the empty vector label $\epsilon = \langle \epsilon, ..., \epsilon \rangle$, where $\forall i \in I_0$, $\epsilon(i) = \epsilon$. Finally, although we omit a formal definition here, we can partition $\Delta_S$ into controllable and uncontrollable labels, denoted by $\Delta_c$ and $\Delta_{uc}$, based on membership in $\Sigma_c$ and $\Sigma_{uc}$.

We focus on states of $\mathcal{U}$, where a control decision for $\sigma \in \Sigma_c$ must be taken, which we call control configurations.

**Definition 3.** (a) The set $\mathcal{D}_\sigma(\mathcal{U}) \subseteq \mathcal{Q}_S$ of control configurations for $\sigma$ w.r.t. disablement for $\mathcal{U}$ is a set of states with outgoing transitions that have labels involving $\sigma \in \Sigma_c$ as follows.

$$ \mathcal{D}_{\sigma}(\mathcal{U}) = \{q \in \mathcal{Q}_{S} | (\exists \hat{q} \in \mathcal{Q}_{S}) \text{ s.t. } (q_0, \sigma, \hat{q}_0) \in T_L \setminus T_K \wedge (\forall i \in I_c(\sigma))(q_i, \sigma, \hat{q}_i) \in T_L\}. $$

(b) The set $\mathcal{E}_\sigma(\mathcal{U}) \subseteq \mathcal{Q}_S$ of control configurations for $\sigma$ w.r.t. enablement for $\mathcal{U}$ is a set of states with outgoing transitions that have labels involving $\sigma \in \Sigma_c$ as follows.

$$ \mathcal{E}_{\sigma}(\mathcal{U}) = \{q \in \mathcal{Q}_{S} | (\exists \hat{q} \in \mathcal{Q}_{S}) \text{ s.t. } (q_0, \sigma, \hat{q}_0) \in T_K \wedge (\forall i \in I_c(\sigma))(q_i, \sigma, \hat{q}_i) \in T_L\}. $$

Note that for $(q_S^l, v, q) \in T_S$, where $q \in \mathcal{D}_\sigma(\mathcal{U})$ and $\sigma \in \Sigma_c$, $v(0)$ corresponds to a word $w \in L$ such that $w \in D_0(\sigma)$, according to Eq. (1). As a result, for each word in Eq. (1), we identify state-based equivalents in Def. 3(a). Similarly, we have state-based equivalents for the words in Eq. (2).

Instead of inferring over words or families of languages, we want to inference over the finite set of control configurations. A state $d \in \mathcal{D}_\sigma(\mathcal{U})$ requires an overall control decision of disable, and we want to be able to discuss the states in $\mathcal{E}_\sigma(\mathcal{U})$ that each agent $i \in I_c(\sigma)$ cannot distinguish from $d$. To capture these aspects, we shall use the natural projection over each alphabet of each agent to capture the states that are indistinguishable for agent $i$ in $\mathcal{U}$.

Recall that the natural projection extends to automata via the determinization algorithm, i.e., the subset relation. To represent the partial observation of $\mathcal{U}$ w.r.t. agent $i \in I_0$, we construct its determinization, denoted by $\mathcal{O}_{\Delta_i}$, and use this structure to formulate state-based control decisions. Initially, we first replace all the transitions in $\mathcal{U}$ that have a label $\sigma \in \Delta_{uo,i}$ with $\epsilon$. Subsequently, we apply the subset relation. More formally, we define the $\epsilon$-reach of a state $q_S \in \mathcal{Q}_S$, w.r.t. alphabet $\Delta_i \subseteq \Delta_S$ as $\epsilon$-reach($q_S$, $\Delta_i$) = $\{\hat{q}_S \in \mathcal{Q}_S | (\exists u \in (\Delta_S \setminus \Delta_i^*))(q_S, u, \hat{q}_S) \in T_S\}$. Then we have

$$ \mathcal{O}_{\Delta_i} = (X_i, \Delta_i, T_{\Delta_i}, x_{i,0}), $$

where $X_i \subseteq 2^{\mathcal{Q}_S}$; $x_{i,0} = \epsilon$-reach($q_S^l$, $\Delta_i$); and $(x_i, \sigma, x_i') \in T_{\Delta_i}$, where $x_i' = \bigcup_{q_S \in x} \epsilon$-reach($\hat{q}_S$, $\Delta_i$) s.t. $(q_S, \sigma, \hat{q}_S) \in T_S$.

A consequence of using subset construction on $\mathcal{U}$ is that states, including control configurations, may appear in more than one state of the determinized state space. This is because the subset relation is not an equivalence relation, and it may be the case that the determinization process allocates states into more than one deterministic state. Thus, we can refine the set of control configurations of Def. 3. To determine the complete set of states for $\mathcal{D}_\sigma(\mathcal{U})$ and $\mathcal{E}_\sigma(\mathcal{U})$, we compute $\mathcal{O}_{\Delta_0}$, where $\Delta_0 = \Delta_o$. If a state $q_S$ of $\mathcal{U}$ appears in more than one state of $\mathcal{O}_{\Delta_0}$, we create a copy (or copies) of $q_S$ with a label $q_S^j$, for $j \in$ some finite index set $J$, in $\mathcal{U}$ and we relabel these states in $\mathcal{O}_{\Delta_0}$. Further, each copy is then added appropriately to either $\mathcal{E}_\sigma(\mathcal{U})$ or $\mathcal{D}_\sigma(\mathcal{U})$. The procedure is demonstrated below in the continuation of our example.

**Ex. 2 cont.** The $\mathcal{U}$ structure for Ex. 2 is shown in Fig. 2, and its $\mathcal{O}_{\Delta_0}$ is shown in Fig. 3. The control configurations (highlighted in red—$\mathcal{D}_\sigma(\mathcal{U})$—and green—$\mathcal{E}_\sigma(\mathcal{U})$) are listed as follows:

$$ \mathcal{D}_{\sigma}(\mathcal{U}) = \{(4, 3, 3), (4, 3, 4), (4, 4, 3), (4, 4, 4)\}; \quad (5) $$

$$ \mathcal{E}_{\sigma}(\mathcal{U}) = \{(3, 3, 3), (3, 3, 4), (3, 4, 3), (3, 4, 4)\}. \quad (6) $$

In Fig. 1, some words have different projections w.r.t. $\pi_i$ (for $i = \{1, 2\}$), but happen to go to the same state. For example, $a_1b_1$ and $a_2b_2$ have different projections for both agents, but both go to state 3. In $\mathcal{U}$, it is also possible to find two different words that go to the same state, but because they have different projections, that common state will appear in two different states of $\mathcal{O}_{\Delta_0}$. As can be seen in Fig. 2, the word $w = \langle a_1, a_1, \epsilon \rangle \langle \epsilon, b_1, \epsilon \rangle \langle \epsilon, \epsilon, a_2 \rangle \langle b_1, b_1, \epsilon \rangle$ goes to control configuration $(3, 3, 4)$, but so does the word $w' = \langle a_2, a_2, \epsilon \rangle \langle \epsilon, \epsilon, a_1 \rangle \langle \epsilon, b_2, \epsilon \rangle \langle b_2, b_2, \epsilon \rangle$. We then construct $\mathcal{O}_{\Delta_0}$, where $\Delta_0 = \{\langle a_1, a_1, \epsilon \rangle, \langle a_2, a_2, \epsilon \rangle, \langle b_1, \epsilon, b_1 \rangle, \langle b_2, \epsilon, b_2 \rangle\}$. Because $\pi_0(w(0)) \neq \pi_0(w'(0))$, the subset relation over $\Delta_0$ results in the control configuration $(3, 3, 4)$ appearing in two different states of $\mathcal{O}_{\Delta_0}$, namely $x_{03}$ and $x_{05}$. Each state in $\mathcal{D}_\sigma(\mathcal{U})$ (Eq. (5)) and $\mathcal{E}_\sigma(\mathcal{U})$ (Eq. (6)) appears in two different states of $\mathcal{O}_{\Delta_0}$: $x_{03}$ and $x_{05}$ for $\mathcal{E}_\sigma(\mathcal{U})$, and $x_{04}$ and $x_{06}$ for $\mathcal{D}_\sigma(\mathcal{U})$. Here, we label the copies with a subscript of '$\alpha$' to distinguish them from the originals. The states of $\mathcal{O}_{\Delta_0}$ after relabeling the copies are presented in the leftmost column of Table 1.

<table><caption>Table 1. State sets $X_0$ (left), $X_1$ (center) and $X_2$ (right) for Ex. 2. The control configurations in $\mathcal{E}_\sigma(\mathcal{U})$ are noted in green, while $\mathcal{D}_\sigma(\mathcal{U})$ are red.</caption><thead><tr><th></th><th>States of O<sub>Δ<sub>0</sub></sub></th><th>States of O<sub>Δ<sub>1</sub></sub></th><th>States of O<sub>Δ<sub>2</sub></sub></th></tr></thead><tbody><tr><td>x<sub>00</sub></td><td>{(0,0,0),(0,0,1),(0,0,2)}</td><td>x<sub>10</sub></td><td>{(0,0,0),(0,0,1),(0,0,2)}</td><td>x<sub>20</sub></td></tr><tr><td>x<sub>01</sub></td><td>{(1,1,0),(1,1,1),(1,1,2),<br>(1,3,0),(1,3,1),(1,3,2),<br>(1,4,0),(1,4,1),(1,4,2)}</td><td>x<sub>11</sub></td><td>{(1,1,0),(1,1,1),(1,1,2),<br>(1,3,0),(1,3,1),(1,3,2),<br>(1,4,0),(1,4,1),(1,4,2),<br>(3,1,3),(3,1,4),(3,3,3),<br>(3,3,4),(3,4,3),(3,4,4),<br>(4,1,3),(4,1,4),(4,3,3),<br>(4,3,4),(4,4,3),(4,4,4)}</td><td>x<sub>21</sub></td></tr><tr><td>x<sub>02</sub></td><td>{(2,2,0),(2,2,1),(2,2,2),<br>(2,3,0),(2,3,1),(2,3,2),<br>(2,4,0),(2,4,1),(2,4,2)}</td><td>x<sub>12</sub></td><td>{(2,2,0),(2,2,1),(2,2,2),<br>(2,3,0),(2,3,1),(2,3,2),<br>(2,4,0),(2,4,1),(2,4,2)}</td><td>x<sub>22</sub></td></tr><tr><td>x<sub>03</sub></td><td>{(3,1,3),(3,1,4),(3,3,3),<br>(3,3,4),(3,4,3),(3,4,4)}</td><td></td><td></td><td>{(3,1,3),(3,1,4),(3,3,3),<br>(3,3,4),(3,4,3),(3,4,4),<br>(4,2,3),(4,2,4),(4,3,3),<br>(4,3,4),(4,4,3), (4,4,4)g}</td></tr><tr><td>x<sub>04</sub></td><td>{(4,1,3),(4,1,4),(4,3,3),<br>(4,3,4),(4,4,3),(4,4,4)}</td><td></td><td></td><td></td></tr><tr><td>x<sub>05</sub></td><td>{(3,2,3),(3,2,4),(3,3,3),<br>(3,3,4), (3,4,3), (3,4,4)g}</td><td></td><td></td><td>{(4,1,3),(4,1,4),(4,3,3),<br>(4,3,4),(4,4,3), (4,4,4)g}</td></tr><tr><td>x<sub>06</sub></td><td>{(4,2,3),(4,2,4),(4,3,3),<br>(4,3,4), (4,4,3), (4,4,4)g}</td><td></td><td></td><td>{(3,2,3),(3,2,4),(3,3,3),<br>(3,3,4), (3,4,3), (3,4,4)g}</td></tr></tbody></table>

After relabeling the duplicate states:

$$ \mathcal{D}_{\sigma}(\mathcal{U}) = \{(4, 3, 3), (4, 3, 4), (4, 4, 3), (4, 4, 4), (4, 3, 3)_{\alpha}, (4, 3, 4)_{\alpha}, (4, 4, 3)_{\alpha}, (4, 4, 4)_{\alpha}\}; $$

$$ \mathcal{E}_{\sigma}(\mathcal{U}) = \{(3, 3, 3), (3, 3, 4), (3, 4, 3), (3, 4, 4), (3, 3, 3)_{\alpha}, (3, 3, 4)_{\alpha}, (3, 4, 3)_{\alpha}, (3, 4, 4)_{\alpha}\}. \quad \blacklozenge $$

<figure><img src="image_4.png" /></figure>

Using $\mathcal{O}_{\Delta_i}$, we can determine the states of $\mathcal{U}$ that are indistinguishable for agent $i$. By construction, such states correspond
relation for $\mathcal{M}_L^\epsilon$; and, the initial state $q_S^l = (q^l, q^i, ..., q^l)$. The $j$th element of $q$ and $\sigma$ are referred to as $q(j)$ or $q_j$ and $\sigma(j)$ or $\sigma_j$, respectively, for $j \in \{0, 1, ..., n\}$. We can extend $T_S$ to be defined over $\Delta_S^*$. As a result, we have a word $v = \sigma_0\sigma_1...\sigma_{|v|-1}$ in the language generated by $\mathcal{U}$ that consists of a vector of words in $L: v(0) = \sigma_0(0)\sigma_1(0)...\sigma_{|v|-1}(0), v(1) = \sigma_0(1)\sigma_1(1)...\sigma_{|v|-1}(1), ..., v(n) = \sigma_0(n)\sigma_1(n)...\sigma_{|v|-1}(n)$ where, by construction, $\pi_i(v(0)) = \pi_i(v(i))$, for all $i \in I$.

Labels in $\Delta_S$ are partitioned into sets of observable labels $\Delta_o$ and unobservable labels $\Delta_{uo}$. For $\sigma \in \Sigma_o$, the corresponding label in $\Delta_o$ has the form $\sigma := \langle \pi_0(\sigma), \pi_1(\sigma), ..., \pi_n(\sigma) \rangle$. Unobservable labels are created for each $i \in I_0$. If $\sigma \in \Sigma \setminus \Sigma_{o,i}$, the unobservable label in $\Delta_{uo,i}$ is assembled as follows: $\sigma(i) = \sigma$, while for all $j \in I_0 \setminus \{i\}$ we have $\sigma(j) = \epsilon$. Then $\Delta_{uo} = \bigcup_{i \in I_0} \Delta_{uo,i} = \Delta_S \setminus \Delta_o$. We also define the empty vector label $\epsilon = \langle \epsilon, ..., \epsilon \rangle$, where $\forall i \in I_0$, $\epsilon(i) = \epsilon$. Finally, although we omit a formal definition here, we can partition $\Delta_S$ into controllable and uncontrollable labels, denoted by $\Delta_c$ and $\Delta_{uc}$, based on membership in $\Sigma_c$ and $\Sigma_{uc}$.

We focus on states of $\mathcal{U}$, where a control decision for $\sigma \in \Sigma_c$ must be taken, which we call control configurations.

**Definition 3.** (a) The set $D_\sigma(\mathcal{U}) \subseteq Q_S$ of control configurations for $\sigma$ w.r.t. disablement for $\mathcal{U}$ is a set of states with outgoing transitions that have labels involving $\sigma \in \Sigma_c$ as follows.

$$D_\sigma(\mathcal{U}) = \{q \in Q_S | (\exists \hat{q} \in Q_S) \text{ s.t. } (q_0, \sigma, \hat{q}_0) \in T_L \setminus T_K \wedge (\forall i \in I_c(\sigma))(q_i, \sigma, \hat{q}_i) \in T_L\}.$$

(b) The set $E_\sigma(\mathcal{U}) \subseteq Q_S$ of control configurations for $\sigma$ w.r.t. enablement for $\mathcal{U}$ is a set of states with outgoing transitions that have labels involving $\sigma \in \Sigma_c$ as follows.

$$E_\sigma(\mathcal{U}) = \{q \in Q_S | (\exists \hat{q} \in Q_S) \text{ s.t. } (q_0, \sigma, \hat{q}_0) \in T_K \wedge (\forall i \in I_c(\sigma))(q_i, \sigma, \hat{q}_i) \in T_L\}.$$

Note that for $(q_S^l, v, q) \in T_S$, where $q \in D_\sigma(\mathcal{U})$ and $\sigma \in \Sigma_c$, $v(0)$ corresponds to a word $w \in L$ such that $w \in D_0(\sigma)$, according to Eq. (1). As a result, for each word in Eq. (1), we identify state-based equivalents in Def. 3(a). Similarly, we have state-based equivalents for the words in Eq. (2).

Instead of inferring over words or families of languages, we want to inference over the finite set of control configurations. A state $d \in D_\sigma(\mathcal{U})$ requires an overall control decision of disable, and we want to be able to discuss the states in $E_\sigma(\mathcal{U})$ that each agent $i \in I_c(\sigma)$ cannot distinguish from $d$. To capture these aspects, we shall use the natural projection over each alphabet of each agent to capture the states that are indistinguishable for agent $i$ in $\mathcal{U}$.

Recall that the natural projection extends to automata via the determinization algorithm, i.e., the subset relation. To represent the partial observation of $\mathcal{U}$ w.r.t. agent $i \in I_0$, we construct its determinization, denoted by $\mathcal{O}_{\Delta_i}$, and use this structure to formulate state-based control decisions. Initially, we first replace all the transitions in $\mathcal{U}$ that have a label $\sigma \in \Delta_{uo,i}$ with $\epsilon$. Subsequently, we apply the subset relation. More formally, we define the $\epsilon$-reach of a state $q_S \in Q_S$, w.r.t. alphabet $\Delta_i \subseteq \Delta_S$ as $\epsilon$-reach($q_S$, $\Delta_i$) = $\{\hat{q}_S \in Q_S | (\exists u \in (\Delta_S \setminus \Delta_i^*) (q_S, u, \hat{q}_S) \in T_S\}$. Then we have

$$\mathcal{O}_{\Delta_i} = (X_i, \Delta_i, T_{\Delta_i}, x_{i,0}),$$

where $X_i \subseteq 2^{Q_S}$; $x_{i,0} = \epsilon$-reach($q_S^l$, $\Delta_i$); and $(x_i, \sigma, x'_i) \in T_{\Delta_i}$, where $x'_i = \bigcup_{q_S \in x} \epsilon$-reach($\hat{q}_S$, $\Delta_i$) s.t. $(q_S, \sigma, \hat{q}_S) \in T_S$.

A consequence of using subset construction on $\mathcal{U}$ is that states, including control configurations, may appear in more than one state of the determinized state space. This is because the subset relation is not an equivalence relation, and it may be the case that the determinization process allocates states into more than one deterministic state. Thus, we can refine the set of control configurations of Def. 3. To determine the complete set of states for $D_\sigma(\mathcal{U})$ and $E_\sigma(\mathcal{U})$, we compute $\mathcal{O}_{\Delta_0}$, where $\Delta_0 = \Delta_o$. If a state $q_S$ of $\mathcal{U}$ appears in more than one state of $\mathcal{O}_{\Delta_0}$, we create a copy (or copies) of $q_S$ with a label $q_{S,j}$, for $j \in$ some finite index set $J$, in $\mathcal{U}$ and we relabel these states in $\mathcal{O}_{\Delta_0}$. Further, each copy is then added appropriately to either $E_\sigma(\mathcal{U})$ or $D_\sigma(\mathcal{U})$. The procedure is demonstrated below in the continuation of our example.

**Ex. 2 cont.** The $\mathcal{U}$ structure for Ex. 2 is shown in Fig. 2, and its $\mathcal{O}_{\Delta_0}$ is shown in Fig. 3. The control configurations (highlighted in red—$D_\sigma(\mathcal{U})$—and green—$E_\sigma(\mathcal{U})$) are listed as follows:

$$D_\sigma(\mathcal{U}) = \{(4, 3, 3), (4, 3, 4), (4, 4, 3), (4, 4, 4)\}; \quad (5)$$

$$E_\sigma(\mathcal{U}) = \{(3, 3, 3), (3, 3, 4), (3, 4, 3), (3, 4, 4)\}. \quad (6)$$

In Fig. 1, some words have different projections w.r.t. $\pi_i$ (for $i = \{1, 2\}$), but happen to go to the same state. For example, $a_1b_1$ and $a_2b_2$ have different projections for both agents, but both go to state 3. In $\mathcal{U}$, it is also possible to find two different words that go to the same state, but because they have different projections, that common state will appear in two different states of $\mathcal{O}_{\Delta_0}$. As can be seen in Fig. 2, the word $w = \langle a_1, a_1, \epsilon \rangle \langle \epsilon, b_1, \epsilon \rangle \langle \epsilon, \epsilon, a_2 \rangle \langle b_1, b_1, \epsilon \rangle$ goes to control configuration (3, 3, 4), but so does the word $w' = \langle a_2, a_2, \epsilon \rangle \langle \epsilon, \epsilon, a_1 \rangle \langle \epsilon, b_2, \epsilon \rangle \langle b_2, b_2, \epsilon \rangle$. We then construct $\mathcal{O}_{\Delta_0}$, where $\Delta_0 = \{\langle a_1, a_1, \epsilon \rangle, \langle a_2, a_2, \epsilon \rangle, \langle b_1, \epsilon, b_1 \rangle, \langle b_2, \epsilon, b_2 \rangle\}$. Because $\pi_0(w(0)) \neq \pi_0(w'(0))$, the subset relation over $\Delta_0$ results in the control configuration (3,3,4) appearing in two different states of $\mathcal{O}_{\Delta_0}$, namely $x_{03}$ and $x_{05}$. Each state in $D_\sigma(\mathcal{U})$ (Eq. (5)) and $E_\sigma(\mathcal{U})$ (Eq. (6)) appears in two different states of $\mathcal{O}_{\Delta_0}$: $x_{03}$ and $x_{05}$ for $E_\sigma(\mathcal{U})$, and $x_{04}$ and $x_{06}$ for $D_\sigma(\mathcal{U})$. Here, we label the copies with a subscript of '$\alpha$' to distinguish them from the originals. The states of $\mathcal{O}_{\Delta_0}$ after relabeling the copies are presented in the leftmost column of Table 1.

<table><caption>Table 1. State sets $X_0$ (left), $X_1$ (center) and $X_2$ (right) for Ex. 2. The control configurations in $E_\sigma(\mathcal{U})$ are noted in green, while $D_\sigma(\mathcal{U})$ are red.</caption><thead><tr><th></th><th>States of O<sub>Δ<sub>0</sub></sub></th><th>States of O<sub>Δ<sub>1</sub></sub></th><th>States of O<sub>Δ<sub>2</sub></sub></th></tr></thead><tbody><tr><td>x<sub>00</sub></td><td>{(0,0,0),(0,0,1),(0,0,2)}</td><td>x<sub>10</sub></td><td>{(0,0,0),(0,0,1),(0,0,2)}</td><td>x<sub>20</sub></td></tr><tr><td>x<sub>01</sub></td><td>{(1,1,0),(1,1,1),(1,1,2),<br>(1,3,0),(1,3,1),(1,3,2),<br>(1,4,0),(1,4,1),(1,4,2)}</td><td>x<sub>11</sub></td><td>{(1,1,0),(1,1,1),(1,1,2),<br>(1,3,0),(1,3,1),(1,3,2),<br>(1,4,0),(1,4,1),(1,4,2),<br>(3,1,3),(3,1,4),(3,3,3),<br>(3,3,4),(3,4,3),(3,4,4),<br>(4,1,3),(4,1,4),(4,3,3),<br>(4,3,4),(4,4,3),(4,4,4)}</td><td>x<sub>21</sub></td></tr><tr><td>x<sub>02</sub></td><td>{(2,2,0),(2,2,1),(2,2,2),<br>(2,3,0),(2,3,1),(2,3,2),<br>(2,4,0),(2,4,1),(2,4,2)}</td><td>x<sub>12</sub></td><td>{(2,2,0),(2,2,1),(2,2,2),<br>(2,3,0),(2,3,1),(2,3,2),<br>(2,4,0),(2,4,1),(2,4,2)}</td><td>x<sub>22</sub></td></tr><tr><td>x<sub>03</sub></td><td>{(3,1,3),(3,1,4),(3,3,3),<br>(3,3,4),(3,4,3),(3,4,4)}</td><td></td><td></td><td>{(3,1,3),(3,1,4),(3,3,3),<br>(3,3,4),(3,4,3),(3,4,4),<br>(4,2,3),(4,2,4),(4,3,3),<br>(4,3,4),(4,4,3),(4,4,4)<sub>a</sub>}</td></tr><tr><td>x<sub>04</sub></td><td>{(4,1,3),(4,1,4),(4,3,3),<br>(4,3,4),(4,4,3),(4,4,4)}</td><td></td><td></td><td>{(4,1,3),(4,1,4),(4,3,3),<br>(4,3,4),(4,4,3),(4,4,4)<sub>a</sub>}</td></tr><tr><td>x<sub>05</sub></td><td>{(3,2,3),(3,2,4),(3,3,3),<br>(3,3,4)<sub>a</sub>,(3,4,3)<sub>a</sub>,(3,4,4)<sub>a</sub>}</td><td></td><td></td><td>{(3,2,3),(3,2,4),(3,3,3),<br>(3,3,4)<sub>a</sub>,(3,4,3)<sub>a</sub>,(3,4,4)<sub>a</sub>}</td></tr><tr><td>x<sub>06</sub></td><td>{(4,2,3),(4,2,4),(4,3,3),<br>(4,3,4)<sub>a</sub>,(4,4,3)<sub>a</sub>,(4,4,4)<sub>a</sub>}</td><td></td><td></td><td>{(3,2,3),(3,2,4),(3,3,3),<br>(3,3,4)<sub>a</sub>,(3,4,3)<sub>a</sub>,(3,4,4)<sub>a</sub>}</td></tr></tbody></table>

After relabeling the duplicate states:

$$D_\sigma(\mathcal{U}) = \{(4, 3, 3), (4, 3, 4), (4, 4, 3), (4, 4, 4), (4, 3, 3)_\alpha, (4, 3, 4)_\alpha, (4, 4, 3)_\alpha, (4, 4, 4)_\alpha\};$$

$$E_\sigma(\mathcal{U}) = \{(3, 3, 3), (3, 3, 4), (3, 4, 3), (3, 4, 4), (3, 3, 3)_\alpha, (3, 3, 4)_\alpha, (3, 4, 3)_\alpha, (3, 4, 4)_\alpha\}.$$

<figure><img src="image_4.png" /></figure>

Using $\mathcal{O}_{\Delta_i}$, we can determine the states of $\mathcal{U}$ that are indistinguishable for agent $i$. By construction, such states correspond
<figure><img src="image_5.png" /><figcaption>Fig. 2. The **U** structure for Ex. 2. Self-loops of $\epsilon$ at each state and labels involving $\sigma$ at states that are not control configurations omitted for readability.</figcaption></figure>

<figure><img src="image_6.png" /><figcaption>Fig. 3. $O_{\Delta_0}$ for Ex. 2.</figcaption></figure>

to words that are equal up to the projection over the observable
alphabet of $i$.

**Definition 4.** Given $q_S, \hat{q}_S \in Q_S$, $q_S$ is indistinguishable from $\hat{q}_S$ for agent $i \in I$, denoted $q_S \sim_i \hat{q}_S$, iff $\exists x \in X_i$ s.t. $q_S, \hat{q}_S \in x$.

We overload our notation and let $[[q_S]]_i$ represent the states in $Q_S$ that agent $i$ cannot distinguish from $q_S$ under $\sim_i$.

Ex. 2 further cont.

The alphabets for each agent are: $\Delta_1 = \{\langle a_1, a_1, \epsilon \rangle, \langle a_2, a_2, \epsilon \rangle\}$ and $\Delta_2 = \{\langle b_1, \epsilon, b_1 \rangle, \langle b_2, \epsilon, b_2 \rangle\}$. The states of $O_{\Delta_1}$ and $O_{\Delta_2}$ are presented in the two rightmost columns of Table 1. Finally, by Table 1, we apply Def. 4 to control configurations w.r.t. $\sigma$, noting that $(3, 3, 3) \sim_1 (4, 3, 3)$ as both these control configurations w.r.t. $\sigma$ are in $x_{11} \in X_1$, and $(3, 3, 3) \sim_2 (4, 3, 3)_\alpha$, as these are both in $x_{21} \in X_2$. ♦

Our focus from here on in is the indistinguishability between
states in $D_\sigma(\mathcal{U})$ and states in $E_\sigma(\mathcal{U})$ for agents in $I_c(\sigma)$.

4. AN ALGORITHM FOR VERIFYING INFERENCE OBSERVABILITY

The inspiration for our algorithm came from using a bipartite graph to examine the relationships between sequences in

Eqs. (3) and (4) when $K$ is not inference observable w.r.t. $L$. A bipartite graph $G$ consists of two disjoint sets of vertices $V_1, V_2$, and each edge of $G$ connects a vertex $v_1 \in V_1$ and a vertex $v_2 \in V_2$. Initially, we constructed vertices based on the sequences in $D_{k+1}(\sigma)$ and $E_{k+1}(\sigma)$, for $\sigma \in \Sigma_c$ and $k \in \mathbb{N}_0$, and drew an edge with a label $i \in I_c(\sigma)$ between two vertices corresponding to $w_d \in D_{k+1}(\sigma)$ and $w_e \in E_{k+1}(\sigma)$ if $\pi_i(w_d) = \pi_i(w_e)$. The members of $D_1(\sigma)$ and $E_1(\sigma)$ from Ex. 2 are presented as a bipartite graph in Fig. 4, where orange lines and purple lines correspond to edge labels $i=1$ and $i=2$, respectively. There are cycles present in this graph, e.g., a vertex sequence of $(a_1 b_2, a_1 b_1, a_2 b_1, a_2 b_2, a_1 b_2)$ and an edge trail of (1, 2, 1, 2). But ultimately, we want a state-based version of an inferencing cycle.

<figure><img src="image_7.png" /><figcaption>Fig. 4. Bipartite graph based on $D_1(\sigma)$ and $E_1(\sigma)$ from Ex. 2.</figcaption></figure>

**Definition 5.** Given $\sigma \in \Sigma_c$, $D = \{d_0, \dots, d_{|D|-1}\} \subseteq D_\sigma(\mathcal{U})$, and $E = \{e_0, \dots, e_{|E|-1}\} \subseteq E_\sigma(\mathcal{U})$. If $\exists m, r \in \mathbb{N}_0$ s.t. $i_0, i_1, \dots, i_{m-1} = \rho_0(I_c(\sigma)) \rho_1(I_c(\sigma)) \dots \rho_{r-1}(I_c(\sigma))$ where $[\rho_{j-1}(I_c(\sigma))]_{I_c(\sigma)|-1} \neq [\rho_j(I_c(\sigma))]_0$ (for $j \in \{1, \dots, r-1\}$) and $d_0 \sim_{i_0} e_0 \sim_{i_1} \dots \sim_{i_{m-1}} d_m$,

then we have an **EBD state-based inferencing cycle** if $\exists t < m-1$ where $d_m = d_t$.

We can similarly define a DBD state-based inferencing cycle
when we instead begin with some $e_0 \in E_\sigma(\mathcal{U})$.
<figure><img src="image_5.png" /><figcaption>Fig. 2. The **U** structure for Ex. 2. Self-loops of $\epsilon$ at each state and labels involving $\sigma$ at states that are not control configurations omitted for readability.</figcaption></figure>

<figure><img src="image_6.png" /><figcaption>Fig. 3. $O_{\Delta_0}$ for Ex. 2.</figcaption></figure>

to words that are equal up to the projection over the observable
alphabet of $i$.

**Definition 4.** Given $q_S, \hat{q}_S \in Q_S$, $q_S$ is indistinguishable from $\hat{q}_S$ for agent $i \in I$, denoted $q_S \sim_i \hat{q}_S$, iff $\exists x \in X_i$ s.t. $q_S, \hat{q}_S \in x$.

We overload our notation and let $[[q_S]]_i$ represent the states in $Q_S$ that agent $i$ cannot distinguish from $q_S$ under $\sim_i$.

Ex. 2 further cont.

The alphabets for each agent are: $\Delta_1 = \{\langle a_1, a_1, \epsilon \rangle, \langle a_2, a_2, \epsilon \rangle\}$ and $\Delta_2 = \{\langle b_1, \epsilon, b_1 \rangle, \langle b_2, \epsilon, b_2 \rangle\}$. The states of $O_{\Delta_1}$ and $O_{\Delta_2}$ are presented in the two rightmost columns of Table 1. Finally, by Table 1, we apply Def. 4 to control configurations w.r.t. $\sigma$, noting that $(3, 3, 3) \sim_1 (4, 3, 3)$ as both these control configurations w.r.t. $\sigma$ are in $x_{11} \in X_1$, and $(3, 3, 3) \sim_2 (4, 3, 3)_\alpha$, as these are both in $x_{21} \in X_2$. ♦

Our focus from here on in is the indistinguishability between
states in $D_\sigma(\mathcal{U})$ and states in $E_\sigma(\mathcal{U})$ for agents in $I_c(\sigma)$.

4. AN ALGORITHM FOR VERIFYING INFERENCE OBSERVABILITY

The inspiration for our algorithm came from using a bipartite graph to examine the relationships between sequences in

Eqs. (3) and (4) when $K$ is not inference observable w.r.t. $L$. A bipartite graph $G$ consists of two disjoint sets of vertices $V_1, V_2$, and each edge of $G$ connects a vertex $v_1 \in V_1$ and a vertex $v_2 \in V_2$. Initially, we constructed vertices based on the sequences in $D_{k+1}(\sigma)$ and $E_{k+1}(\sigma)$, for $\sigma \in \Sigma_c$ and $k \in \mathbb{N}_0$, and drew an edge with a label $i \in I_c(\sigma)$ between two vertices corresponding to $w_d \in D_{k+1}(\sigma)$ and $w_e \in E_{k+1}(\sigma)$ if $\pi_i(w_d) = \pi_i(w_e)$. The members of $D_1(\sigma)$ and $E_1(\sigma)$ from Ex. 2 are presented as a bipartite graph in Fig. 4, where orange lines and purple lines correspond to edge labels $i=1$ and $i=2$, respectively. There are cycles present in this graph, e.g., a vertex sequence of $(a_1 b_2, a_1 b_1, a_2 b_1, a_2 b_2, a_1 b_2)$ and an edge trail of (1, 2, 1, 2). But ultimately, we want a state-based version of an inferencing cycle.

<figure><img src="image_7.png" /><figcaption>Fig. 4. Bipartite graph based on $D_1(\sigma)$ and $E_1(\sigma)$ from Ex. 2.</figcaption></figure>

**Definition 5.** Given $\sigma \in \Sigma_c$, $D = \{d_0, \dots, d_{|D|-1}\} \subseteq D_\sigma(\mathcal{U})$, and $E = \{e_0, \dots, e_{|E|-1}\} \subseteq E_\sigma(\mathcal{U})$. If $\exists m, r \in \mathbb{N}_0$ s.t. $i_0, i_1, \dots, i_{m-1} = \rho_0(I_c(\sigma)) \rho_1(I_c(\sigma)) \dots \rho_{r-1}(I_c(\sigma))$ where $[\rho_{j-1}(I_c(\sigma))]_{I_c(\sigma)|-1} \neq [\rho_j(I_c(\sigma))]_0$ (for $j \in \{1, \dots, r-1\}$) and $d_0 \sim_{i_0} e_0 \sim_{i_1} \dots \sim_{i_{m-1}} d_m$,

then we have an **EBD state-based inferencing cycle** if $\exists t < m-1$ where $d_m = d_t$.

We can similarly define a DBD state-based inferencing cycle
when we instead begin with some $e_0 \in E_\sigma(\mathcal{U})$.
Our algorithm runs on a bipartite graph $G_\sigma$ whose disjoint sets of vertices correspond to the sets of control configurations $D_\sigma(\mathcal{U})$ and $E_\sigma(\mathcal{U})$, denoted here by $V_{D_\sigma}(\mathcal{U})$ and $V_{E_\sigma}(\mathcal{U})$, respectively. There is an edge labelled $i$ between a vertex $v_d \in V_{D_\sigma}(\mathcal{U})$ and a vertex $v_e \in V_{E_\sigma}(\mathcal{U})$ if $d \sim_i e$ in $O_{\Delta_i}$, for $i \in I_c(\sigma)$.

The bipartite graph using the control configurations of $\mathcal{U}$ for Ex. 2 is shown in Fig. 5, using the same color scheme as in Fig. 4. Solid lines indicate a sample inferencing cycle: $(3, 3, 3) \sim_1 (4, 3, 4) \sim_2 (3, 3, 3)_\alpha \sim_1 (4, 3, 4)_\alpha \sim_2 (3, 3, 3)$.

<figure><img src="image_8.png" /><figcaption>Fig. 5. $G_\sigma$ for Ex. 2.</figcaption></figure>

We now present our algorithm for verifying whether a system is inference observable based on whether it contains inferencing cycles. The basic outline of the verification strategy is as follows:

(1) Before running Algorithm 1, compute $\mathcal{U}$ to identify the control configurations w.r.t. enablement and disablement.

(2) Run subset construction on $\mathcal{U}$ over the alphabet of observable labels $\Delta_0$ to build $O_{\Delta_0}$.

(3) Check states of $O_{\Delta_0}$ for duplicates of $E_\sigma(\mathcal{U})$ and $D_\sigma(\mathcal{U})$, for all $\sigma \in \Sigma_c$, relabel and update these states in both $\mathcal{U}$ and $O_{\Delta_0}$ (see Section 3).

(4) Construct $O_{\Delta_i}$ and $\sim_i$ (for $i \in I$).

(5) Run Algorithm 1 consisting of the following milestones:

(a) For some $\sigma \in \Sigma_c$, build $G_\sigma$ using the (relabeled) states of $E_\sigma(\mathcal{U})$ and $D_\sigma(\mathcal{U})$ as the two vertex sets. An edge $(v_e, v_d)$ with label $i \in I_c(\sigma)$ exists in $G_\sigma$ between a vertex $v_e \in V_{E_\sigma}(\mathcal{U})$ and a vertex $v_d \in V_{D_\sigma}(\mathcal{U})$ if agent $i$ cannot distinguish between the states in $\mathcal{U}$ represented by the two vertices, i.e., $e \sim_i d$.

(b) Run a cycle detection on $G_\sigma$ according to Def. 5. Since we work with a finite structure, there is no issue detecting arbitrarily long cycles. If inferencing cycles exist, exit with no solution; otherwise, if more controllable events are left to check, pick one at random and repeat from (5a). If all controllable events have been checked, compute the value for $N$ and exit successfully.

## 4.1 The algorithm

Algorithm 1 begins by initializing $N$ for $\sigma \in \Sigma_c$ (line 4) and the set of the adjacent ("neighboring") vertices of vertex $v$, denoted by $A_{i,v}$ (line 8). At that point (lines 10 - 15), the adjacent vertices for each vertex are built from the $\sim_i$ relation via subset construction of $\mathcal{U}$ w.r.t. $i \in I$.

One further initialization pass (lines 20 - 24) determines if any vertices can be distinguished at the outset. Such vertices are stored in $V_{dist}$ and $N$ for this $\sigma \in \Sigma_c$ is updated to 0 since $v$ can be distinguished immediately in inferencing round 0. Note that at this stage, if we can distinguish none of the vertices, then $V_{dist} = \emptyset$ at line 25, so $\text{prev}_{dist}$ will likewise be empty, and the algorithm will return False at line 46, as we have detected an inferencing cycle involving all the vertices of $G_\sigma$.

Lines 27 - 45 are where the primary inferencing cycle detection occurs. This loop also represents the manipulation of the bipartite graph itself.

If agent $i$ can fully distinguish a vertex $v$, its set of adjacent vertices $A_{i,v}$ is empty. Each iteration endeavors to remove edges from the bipartite graph, that is, edges with a label $i$ between any vertices $v'$ and $v$, since in a previous "round" $i$ could distinguish $v$, no other agent needs to bother. If removing edges now renders the set of $v'$'s neighbors, i.e., $A_{i,v'}$, empty, then $v'$ is added to the list of distinguished vertices for the next iteration and $N(\sigma)$ is updated with the value of the current inferencing round. These lines repeat until there are no more vertices to distinguish. If the condition at line 46 is not met, then $N(\sigma)$ is the smallest number of rounds required to distinguish all the vertices in $G_\sigma$. The algorithm repeats from line 2 with the next controllable event.

When the condition at line 46 is met, the algorithm returns False, signalling the presence of an inferencing cycle since the number of distinguished vertices is not equal to the number of control configurations w.r.t. $\sigma \in \Sigma_c$. Recall that a vertex $v$ is deemed distinguished by agent $i \in I_c(\sigma)$ when $A_{i,v} = \emptyset$. Thus, when the loop at lines 27 - 45 completes in this scenario, it is because none of the agents in $I_c(\sigma)$ can distinguish the remaining vertices $v \in (V_{D_\sigma}(\mathcal{U}) \cup V_{E_\sigma}(\mathcal{U})) \setminus V_{dist}$, indicating the presence of an inferencing cycle.

The algorithm returns True at line 49 if all control configurations across $\Sigma_c$ are distinguished. The final value of $N$ is determined by taking the maximum value across the bounds computed for each $\sigma \in \Sigma_c$ at line 48.

**Proposition 6.** Algorithm 1 correctly verifies a violation of inference observability in the presence of state-based inferencing cycles in $\mathcal{U}$.

*Proof sketch:* Given $\mathcal{U}$ and, for simplicity, assume that $\Sigma_c = \{\sigma\}$. Further, let the control configurations w.r.t. $\sigma$ be $D_\sigma(\mathcal{U}) = \{d\}$ and $E_\sigma(\mathcal{U}) = \{e\}$, and assume $\mathcal{U}$ contains an EBD state-inferencing cycle starting at $d$. That is, $\exists m, r \in \mathbb{N}_0$ such that $\rho_0(I_c(\sigma))\rho_1(I_c(\sigma))... \rho_{r-1}(I_c(\sigma)) = i_0, i_1, ... i_{m-1}$ such that $d \sim_{i_0} e \sim_{i_1} ... d \sim_{i_j} e \sim_{i_{j+1}} ... \sim_{i_{m-1}} d$. In this case, $r = 1$ and $m = |I_c(\sigma)|$ since one permutation of $I_c(\sigma)$ results in an inferencing cycle for $d$ and $e$, regardless of the permutation. Additionally, $\mathcal{U}$ contains a DBD state-inferencing cycle starting at $e$. Since there is no $i \in I_c(\sigma)$ that can distinguish $d$ from $e$, at line 25 of the algorithm, $A_{i,d} = \{e\}$ and $A_{i,e} = \{d\}$, for all $i \in I_c(\sigma)$. Since neither of these sets will allow the algorithm ever to reach line 23, it will never be the case that either of these states will be added to $\text{prev}_{dist}$ in line 25. As a result, when reaching line 46, the algorithm will return False since neither $d$ nor $e$ was distinguished. ■

*Ex. 2 concluded.* We use Algorithm 1 to confirm that the example contains inference cycles and is thus not inference observable. After the initialization loop in lines 6 - 8, the edges of the bipartite graph are constructed in lines 10 - 15. In particular, as can be deduced from Table 1, when $v = (4,3,3)$, we have $A_{1,v} = \{(3,3,3), (3,3,4), (3,4,3), (3,4,4)\}$ and $A_{2,v} = \{(3,3,3)_\alpha, (3,3,4)_\alpha, (3,4,3)_\alpha, (3,4,4)_\alpha\}$. All the other vertices have identically sized (non-empty) sets of adjacent vertices. As a result, after $V_{dist}$ is initialized to $\emptyset$ in line 17, it never changes since the conditional at line 22 is False for every single vertex in $V_{D_\sigma}(\mathcal{U}) \cup V_{E_\sigma}(\mathcal{U})$. Consequently, in line 25, $\text{prev}_{dist} = \emptyset$, and the conditional at line 27 is immediately False, thus terminating the program at line 46 and returning False. ♦

Overall, the computational complexity for Algorithm 1 is $O(\sum_{\sigma \in \Sigma_c} (|I_c(\sigma)| \cdot |E_\sigma(\mathcal{U})| \cdot |D_\sigma(\mathcal{U})|))$. We have implemented
Our algorithm runs on a bipartite graph $G_\sigma$ whose disjoint sets of vertices correspond to the sets of control configurations $D_\sigma(\mathcal{U})$ and $E_\sigma(\mathcal{U})$, denoted here by $V_{D_\sigma}(\mathcal{U})$ and $V_{E_\sigma}(\mathcal{U})$, respectively. There is an edge labelled $i$ between a vertex $v_d \in V_{D_\sigma}(\mathcal{U})$ and a vertex $v_e \in V_{E_\sigma}(\mathcal{U})$ if $d \sim_i e$ in $O_{\Delta_i}$, for $i \in I_c(\sigma)$.

The bipartite graph using the control configurations of $\mathcal{U}$ for Ex. 2 is shown in Fig. 5, using the same color scheme as in Fig. 4. Solid lines indicate a sample inferencing cycle: $(3, 3, 3) \sim_1 (4, 3, 4) \sim_2 (3, 3, 3)_\alpha \sim_1 (4, 3, 4)_\alpha \sim_2 (3, 3, 3)$.

<figure><img src="image_8.png" /><figcaption>Fig. 5. $G_\sigma$ for Ex. 2.</figcaption></figure>

We now present our algorithm for verifying whether a system is inference observable based on whether it contains inferencing cycles. The basic outline of the verification strategy is as follows:

(1) Before running Algorithm 1, compute $\mathcal{U}$ to identify the control configurations w.r.t. enablement and disablement.

(2) Run subset construction on $\mathcal{U}$ over the alphabet of observable labels $\Delta_0$ to build $O_{\Delta_0}$.

(3) Check states of $O_{\Delta_0}$ for duplicates of $E_\sigma(\mathcal{U})$ and $D_\sigma(\mathcal{U})$, for all $\sigma \in \Sigma_c$, relabel and update these states in both $\mathcal{U}$ and $O_{\Delta_0}$ (see Section 3).

(4) Construct $O_{\Delta_i}$ and $\sim_i$ (for $i \in I$).

(5) Run Algorithm 1 consisting of the following milestones:

(a) For some $\sigma \in \Sigma_c$, build $G_\sigma$ using the (relabeled) states of $E_\sigma(\mathcal{U})$ and $D_\sigma(\mathcal{U})$ as the two vertex sets. An edge $(v_e, v_d)$ with label $i \in I_c(\sigma)$ exists in $G_\sigma$ between a vertex $v_e \in V_{E_\sigma}(\mathcal{U})$ and a vertex $v_d \in V_{D_\sigma}(\mathcal{U})$ if agent $i$ cannot distinguish between the states in $\mathcal{U}$ represented by the two vertices, i.e., $e \sim_i d$.

(b) Run a cycle detection on $G_\sigma$ according to Def. 5. Since we work with a finite structure, there is no issue detecting arbitrarily long cycles. If inferencing cycles exist, exit with no solution; otherwise, if more controllable events are left to check, pick one at random and repeat from (5a). If all controllable events have been checked, compute the value for $N$ and exit successfully.

## 4.1 The algorithm

Algorithm 1 begins by initializing $N$ for $\sigma \in \Sigma_c$ (line 4) and the set of the adjacent ("neighboring") vertices of vertex $v$, denoted by $A_{i,v}$ (line 8). At that point (lines 10 - 15), the adjacent vertices for each vertex are built from the $\sim_i$ relation via subset construction of $\mathcal{U}$ w.r.t. $i \in I$.

One further initialization pass (lines 20 - 24) determines if any vertices can be distinguished at the outset. Such vertices are stored in $V_{dist}$ and $N$ for this $\sigma \in \Sigma_c$ is updated to 0 since $v$ can be distinguished immediately in inferencing round 0. Note that at this stage, if we can distinguish none of the vertices, then $V_{dist} = \emptyset$ at line 25, so $\text{prev}_{dist}$ will likewise be empty, and the algorithm will return False at line 46, as we have detected an inferencing cycle involving all the vertices of $G_\sigma$.

Lines 27 - 45 are where the primary inferencing cycle detection occurs. This loop also represents the manipulation of the bipartite graph itself. If agent $i$ can fully distinguish a vertex $v$, its set of adjacent vertices $A_{i,v}$ is empty. Each iteration endeavors to remove edges from the bipartite graph, that is, edges with a label $i$ between any vertices $v'$ and $v$, since in a previous "round" $i$ could distinguish $v$, no other agent needs to bother. If removing edges now renders the set of $v'$'s neighbors, i.e., $A_{i,v'}$, empty, then $v'$ is added to the list of distinguished vertices for the next iteration and $N(\sigma)$ is updated with the value of the current inferencing round. These lines repeat until there are no more vertices to distinguish. If the condition at line 46 is not met, then $N(\sigma)$ is the smallest number of rounds required to distinguish all the vertices in $G_\sigma$. The algorithm repeats from line 2 with the next controllable event.

When the condition at line 46 is met, the algorithm returns False, signalling the presence of an inferencing cycle since the number of distinguished vertices is not equal to the number of control configurations w.r.t. $\sigma \in \Sigma_c$. Recall that a vertex $v$ is deemed distinguished by agent $i \in I_c(\sigma)$ when $A_{i,v} = \emptyset$. Thus, when the loop at lines 27 - 45 completes in this scenario, it is because none of the agents in $I_c(\sigma)$ can distinguish the remaining vertices $v \in (V_{D_\sigma}(\mathcal{U}) \cup V_{E_\sigma}(\mathcal{U})) \setminus V_{dist}$, indicating the presence of an inferencing cycle.

The algorithm returns True at line 49 if all control configurations across $\Sigma_c$ are distinguished. The final value of $N$ is determined by taking the maximum value across the bounds computed for each $\sigma \in \Sigma_c$ at line 48.

**Proposition 6.** Algorithm 1 correctly verifies a violation of inference observability in the presence of state-based inferencing cycles in $\mathcal{U}$.

*Proof sketch:* Given $\mathcal{U}$ and, for simplicity, assume that $\Sigma_c = \{\sigma\}$. Further, let the control configurations w.r.t. $\sigma$ be $D_\sigma(\mathcal{U}) = \{d\}$ and $E_\sigma(\mathcal{U}) = \{e\}$, and assume $\mathcal{U}$ contains an EBD state-inferencing cycle starting at $d$. That is, $\exists m, r \in \mathbb{N}_0$ such that $\rho_0(I_c(\sigma))\rho_1(I_c(\sigma))... \rho_{r-1}(I_c(\sigma)) = i_0, i_1, ... i_{m-1}$ such that $d \sim_{i_0} e \sim_{i_1} ... d \sim_{i_j} e \sim_{i_{j+1}} ... \sim_{i_{m-1}} d$. In this case, $r = 1$ and $m = |I_c(\sigma)|$ since one permutation of $I_c(\sigma)$ results in an inferencing cycle for $d$ and $e$, regardless of the permutation. Additionally, $\mathcal{U}$ contains a DBD state-inferencing cycle starting at $e$. Since there is no $i \in I_c(\sigma)$ that can distinguish $d$ from $e$, at line 25 of the algorithm, $A_{i,d} = \{e\}$ and $A_{i,e} = \{d\}$, for all $i \in I_c(\sigma)$. Since neither of these sets will allow the algorithm ever to reach line 23, it will never be the case that either of these states will be added to $\text{prev}_{dist}$ in line 25. As a result, when reaching line 46, the algorithm will return False since neither $d$ nor $e$ was distinguished. ■

*Ex. 2 concluded.* We use Algorithm 1 to confirm that the example contains inference cycles and is thus not inference observable. After the initialization loop in lines 6 - 8, the edges of the bipartite graph are constructed in lines 10 - 15. In particular, as can be deduced from Table 1, when $v = (4,3,3)$, we have $A_{1,v} = \{(3,3,3), (3,3,4), (3,4,3), (3,4,4)\}$ and $A_{2,v} = \{(3,3,3)_\alpha, (3,3,4)_\alpha, (3,4,3)_\alpha, (3,4,4)_\alpha\}$. All the other vertices have identically sized (non-empty) sets of adjacent vertices. As a result, after $V_{dist}$ is initialized to $\emptyset$ in line 17, it never changes since the conditional at line 22 is False for every single vertex in $V_{D_\sigma}(\mathcal{U}) \cup V_{E_\sigma}(\mathcal{U})$. Consequently, in line 25, $\text{prev}_{dist} = \emptyset$, and the conditional at line 27 is immediately False, thus terminating the program at line 46 and returning False. ♦

Overall, the computational complexity for Algorithm 1 is $O(\sum_{\sigma \in \Sigma_c} (|I_c(\sigma)| \cdot |E_\sigma(\mathcal{U})| \cdot |D_\sigma(\mathcal{U})|))$. We have implemented
<caption>**Algorithm 1** Verifying state-based inference-observability using a bipartite graph</caption>

1: **procedure** ISINFOBS($\Sigma_c$, {$I_c(\sigma)$}$_{\sigma \in \Sigma_c}$, {$\langle V_{D_\sigma}(\mathcal{U}), V_{E_\sigma}(\mathcal{U}) \rangle$}$_{\sigma \in \Sigma_c}$, {$\sim_i$}$_{i \in I_c(\sigma)}$)
2: &nbsp;&nbsp;&nbsp;**for all** $\sigma \in \Sigma_c$ **do**
3: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;▷ Initialize the value of $N$ for each $\sigma \in \Sigma_c$ ▷
4: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**N**($\sigma$) &minus; 1
5: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;▷ For each agent $i$, initialize the set of adjacent
6: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;vertices for all $v \in V_{D_\sigma}(\mathcal{U}) \cup V_{E_\sigma}(\mathcal{U})$: $A_{i,v}$
7: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;The loop below runs in $O((|E_\sigma(\mathcal{U})| + |D_\sigma(\mathcal{U})|) \cdot |I_c(\sigma)|)$ time. ▷
8: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**for all** $i \in I_c(\sigma)$ **do**
9: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**for all** $v \in V_{D_\sigma}(\mathcal{U}) \cup V_{E_\sigma}(\mathcal{U})$ **do**
10: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**for all** $e \in V_{E_\sigma}(\mathcal{U})$ **do**
11: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**for all** $i \in I_c(\sigma)$ **do**
12: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**if** $d \sim_i e$ **then**
13: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**A**$_{i,d}$ &minus; $A_{i,d} \cup \{e\}$
14: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**A**$_{i,e}$ &minus; $A_{i,e} \cup \{d\}$
15: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;▷ $V_{dist}$ is the set of vertices in $V_{D_\sigma}(\mathcal{U}) \cup V_{E_\sigma}(\mathcal{U})$ that
16: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;can be distinguished by at least one $i \in I_c(\sigma)$ ▷
17: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$V_{dist}$ &minus; $\emptyset$
18: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**infLevel** &minus; 0
19: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;▷ Identify vertices that are immediately distinguishable before checking for cycles.
20: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;This can be done in $O((|E_\sigma(\mathcal{U})| + |D_\sigma(\mathcal{U})|) \cdot |I_c(\sigma)|)$ time. ▷
21: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**for all** $v \in V_{D_\sigma}(\mathcal{U}) \cup V_{E_\sigma}(\mathcal{U})$ **do**
22: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**for all** $i \in I_c(\sigma)$ **do**
23: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**if** $A_{i,v} = \emptyset \land v \notin V_{dist}$ **then**
24: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$V_{dist}$ &minus; $V_{dist} \cup \{v\}$
25: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$N(\sigma)$ &minus; $infLevel$
26: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;▷ Loop to detect cycles in the bipartite graph
27: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$G_\sigma$, If $G_\sigma$ has $t_\sigma$ edges, then the complexity is
28: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$O(\sum_{\sigma \in \Sigma_c} (|E_\sigma(\mathcal{U})| + |D_\sigma(\mathcal{U})| + t_\sigma))$ because
29: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;each vertex and edge can be removed at most once. ▷
30: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**while** $\text{prev}_{\text{dist}} \neq \emptyset$ **do**
31: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**infLevel** &minus; $\text{infLevel} + 1$
32: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**curr**$_{\text{dist}}$ &minus; $\emptyset$
33: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**for all** $v \in \text{prev}_{\text{dist}}$ **do**
34: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**for all** $i \in I_c(\sigma)$ **do**
35: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**if** $A_{i,v} = \emptyset \land v \notin V_{\text{dist}}$ **then**
36: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**curr**$_{\text{dist}}$ &minus; $\text{curr}_{\text{dist}} \cup \{v\}$
37: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**if** $\text{infLevel} > N(\sigma)$ **then**
38: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$N(\sigma)$ &minus; $\text{infLevel}$
39: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**else**
40: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**for all** $v' \in A_{i,v}$ **do**
41: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;▷ Removing $v$ from $A_{i,v'}$ effectively removes the edge with
42: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;label $i$ between $v$ and $v'$ ▷
43: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**A**$_{i,v'}$ &minus; $A_{i,v'} \setminus \{v\}$
44: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**if** $A_{i,v'} = \emptyset \land v' \notin V_{\text{dist}}$ **then**
45: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**curr**$_{\text{dist}}$ &minus; $\text{curr}_{\text{dist}} \cup \{v'\}$
46: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**if** $\text{infLevel} > N(\sigma)$ **then**
47: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$N(\sigma)$ &minus; $\text{infLevel}$
48: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$V_{\text{dist}}$ &minus; $V_{\text{dist}} \cup \text{curr}_{\text{dist}}$
49: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$\text{prev}_{\text{dist}}$ &minus; $\text{curr}_{\text{dist}}$
50: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**if** $V_{\text{dist}} \neq (V_{D_\sigma}(\mathcal{U}) \cup V_{E_\sigma}(\mathcal{U}))$ **then** return **False**
51: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;▷ Find the overall upper bound across $\Sigma_c$ ▷
52: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$N$ &minus; $\max_{\sigma \in \Sigma_c} N(\sigma)$
53: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**return** **True**

Algorithm 1 and have examined various examples, including examples with more than two inferencing agents. Our implementation, along with a variety of solved examples, can be found in Yoon and Stairs (2015 - 2024).

## 5. CONCLUSION

We have presented a new way of thinking about inferencing in decentralized discrete-event systems. Specifically, we explored the idea of inferencing cycles and their role in determining when an inferencing solution exists. We proposed an algorithm for verifying this interpretation of inferencing observability. Most notably, when an inferencing solution exists, our algorithm computes the upper bound $N$. Note that Takai and Kumar (2017, 2018) verify $N$ but do not compute it, so our algorithmic results are incomparable. Future work includes extending Algorithm 1 to compute the local and global control decisions when the system is inference observable. Finally, our new understanding of inferencing cycles opens up new avenues we began to explore in decentralized architectures beyond inferencing (Ricker et al., 2017).

## REFERENCES

Arnold, A. (1994). *Finite Transition Systems*. Masson.

Kumar, R. and Takai, S. (2007). Inference-based ambiguity management in decentralized decision-making: Decentralized control of discrete event systems. *IEEE Trans. Autom. Control*, 52(10), 1783–1794.

Rabin, M. and Scott, D. (1959). Finite automata and their decision problems. *IBM J. Res. Dev.*, 3(2), 114–125.

Ricker, S., Lidbetter, T., and Marchand, H. (2017). Inference and beyond: further adventures with parity-based architectures for decentralized discrete-event systems. *IFAC-PapersOnLine*, 50(1), 13447–13452.

Ricker, S. and Marchand, H. (2013). A parity-based architecture for decentralized discrete-event control. In *Am. Control Conf.*, 5678–5684.

Rudie, K. and Wonham, W.M. (1992). Think globally, act locally: Decentralized supervisory control. *IEEE Trans. Autom. Control*, 37(11), 1692–1708.

Takai, S. and Kumar, R. (2008). Synthesis of inference-based decentralized control for discrete event systems. *IEEE Trans. Autom. Control*, 53(2), 522–534.

Takai, S. and Kumar, R. (2017). A generalized framework for inference-based diagnosis of discrete event systems capturing both disjunctive and conjunctive decision-making. *IEEE Trans. Autom. Control*, 62(6), 2778–2793.

Takai, S. and Kumar, R. (2018). Implementation of inference-based diagnosis: computing delay bound and ambiguity levels. *Discrete Event Dyn. Syst.*, 28(2), 315–348.

Yoo, T.S. and Lafortune, S. (2004). Decentralized supervisory control with conditional decisions: supervisor existence. *IEEE Trans. Autom. Control*, 49(11), 1886–1904.

Yoon, S.H. and Stairs, M. (2015 - 2024). JDec. URL https://github.com/Summer2023SHY/JDec.
<caption>**Algorithm 1** Verifying state-based inference-observability using a bipartite graph</caption>

1: **procedure** ISINFOBS($\Sigma_c$, {$I_c(\sigma)$}$_{\sigma \in \Sigma_c}$, {$\langle V_{D_\sigma}(\mathcal{U}), V_{E_\sigma}(\mathcal{U}) \rangle$}$_{\sigma \in \Sigma_c}$, {$\sim_i$}$_{i \in I_c(\sigma)}$)
2: &nbsp;&nbsp;&nbsp;&nbsp;**for all** $\sigma \in \Sigma_c$ **do**
3: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;▷ Initialize the value of $N$ for each $\sigma \in \Sigma_c$ ▷
4: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**N**($\sigma$) $\leftarrow$ -1
5: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;▷ For each agent $i$, initialize the set of adjacent vertices for all $v \in V_{D_\sigma}(\mathcal{U}) \cup V_{E_\sigma}(\mathcal{U})$: $A_{i,v}$ The loop below runs in $O((|E_\sigma(\mathcal{U})| + |D_\sigma(\mathcal{U})|) \cdot |I_c(\sigma)|)$ time. ▷
6: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**for all** $i \in I_c(\sigma)$ **do**
7: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**for all** $v \in V_{D_\sigma}(\mathcal{U}) \cup V_{E_\sigma}(\mathcal{U})$ **do**
8: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**A**$_{i,v}$ $\leftarrow$ ∅
9: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;▷ Building edges of bipartite graph. This can be achieved in $O(|E_\sigma(\mathcal{U})| \cdot |D_\sigma(\mathcal{U})| \cdot |I_c(\sigma)|)$ time. ▷
10: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**for all** $d \in V_{D_\sigma}(\mathcal{U})$ **do**
11: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**for all** $e \in V_{E_\sigma}(\mathcal{U})$ **do**
12: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**for all** $i \in I_c(\sigma)$ **do**
13: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**if** $d \sim_i e$ **then**
14: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**A**$_{i,d}$ $\leftarrow$ **A**$_{i,d}$ $\cup$ {e}
15: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**A**$_{i,e}$ $\leftarrow$ **A**$_{i,e}$ $\cup$ {d}
16: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;▷ $V_{dist}$ is the set of vertices in $V_{D_\sigma}(\mathcal{U}) \cup V_{E_\sigma}(\mathcal{U})$ that can be distinguished by at least one $i \in I_c(\sigma)$ ▷
17: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**V**$_{dist}$ $\leftarrow$ ∅
18: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**infLevel** $\leftarrow$ 0
19: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;▷ Identify vertices that are immediately distinguishable before checking for cycles. This can be done in $O((|E_\sigma(\mathcal{U})| + |D_\sigma(\mathcal{U})|) \cdot |I_c(\sigma)|)$ time. ▷
20: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**for all** $v \in V_{D_\sigma}(\mathcal{U}) \cup V_{E_\sigma}(\mathcal{U})$ **do**
21: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**for all** $i \in I_c(\sigma)$ **do**
22: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**if** $A_{i,v}$ $\leftarrow$ ∅ $\wedge$ $v \notin V_{dist}$ **then**
23: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**V**$_{dist}$ $\leftarrow$ **V**$_{dist}$ $\cup$ {v}
24: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**N**($\sigma$) $\leftarrow$ **infLevel**
25: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**prev**$_{dist}$ $\leftarrow$ **V**$_{dist}$
26: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;▷ Loop to detect cycles in the bipartite graph $G_\sigma$, If $G_\sigma$ has $t_\sigma$ edges, then the complexity is $O(\sum_{\sigma \in \Sigma_c} (|E_\sigma(\mathcal{U})| + |D_\sigma(\mathcal{U})| + t_\sigma))$ because each vertex and edge can be removed at most once. ▷
27: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**while** $\text{prev}_{\text{dist}} \neq \emptyset$ **do**
28: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**infLevel** $\leftarrow$ **infLevel** +1
29: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**curr**$_{dist}$ $\leftarrow$ ∅
30: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**for all** $v \in \text{prev}_{\text{dist}}$ **do**
31: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**for all** $i \in I_c(\sigma)$ **do**
32: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**if** $A_{i,v}$ $\leftarrow$ ∅ $\wedge$ $v \notin V_{\text{dist}}$ **then**
33: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**curr**$_{dist}$ $\leftarrow$ **curr**$_{dist}$ $\cup$ {v}
34: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**if** **infLevel** $> N(\sigma)$ **then**
35: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**N**($\sigma$) $\leftarrow$ **infLevel**
36: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**else**
37: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**for all** $v' \in A_{i,v}$ **do**
38: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;▷ Removing $v$ from $A_{i,v'}$ effectively removes the edge with label $i$ between $v$ and $v'$ ▷
39: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**A**$_{i,v'}$ $\leftarrow$ **A**$_{i,v'}$ $\setminus$ {v}
40: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**if** $A_{i,v'}$ $\leftarrow$ ∅ $\wedge$ $v' \notin V_{\text{dist}}$ **then**
41: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**curr**$_{dist}$ $\leftarrow$ **curr**$_{dist}$ $\cup$ {v'}
42: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**if** **infLevel** $> N(\sigma)$ **then**
43: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**N**($\sigma$) $\leftarrow$ **infLevel**
44: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**V**$_{dist}$ $\leftarrow$ **V**$_{dist}$ $\cup$ **curr**$_{dist}$
45: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**prev**$_{dist}$ $\leftarrow$ **curr**$_{dist}$
46: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**if** $V_{\text{dist}} \neq (V_{D_\sigma}(\mathcal{U}) \cup V_{E_\sigma}(\mathcal{U}))$ **then** **return** False
47: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;▷ Find the overall upper bound across $\Sigma_c$ ▷
48: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**N** $\leftarrow$ $\max_{\sigma \in \Sigma_c}$ **N**($\sigma$)
49: &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**return** True

Algorithm 1 and have examined various examples, including examples with more than two inferencing agents. Our implementation, along with a variety of solved examples, can be found in Yoon and Stairs (2015 - 2024).

## 5. CONCLUSION

We have presented a new way of thinking about inferencing in decentralized discrete-event systems. Specifically, we explored the idea of inferencing cycles and their role in determining when an inferencing solution exists. We proposed an algorithm for verifying this interpretation of inferencing observability. Most notably, when an inferencing solution exists, our algorithm computes the upper bound $N$. Note that Takai and Kumar (2017, 2018) verify $N$ but do not compute it, so our algorithmic results are incomparable. Future work includes extending Algorithm 1 to compute the local and global control decisions when the system is inference observable. Finally, our new understanding of inferencing cycles opens up new avenues we began to explore in decentralized architectures beyond inferencing (Ricker et al., 2017).

## REFERENCES

* Arnold, A. (1994). *Finite Transition Systems*. Masson.

* Kumar, R. and Takai, S. (2007). Inference-based ambiguity management in decentralized decision-making: Decentralized control of discrete event systems. *IEEE Trans. Autom. Control*, 52(10), 1783–1794.

* Rabin, M. and Scott, D. (1959). Finite automata and their decision problems. *IBM J. Res. Dev.*, 3(2), 114–125.

* Ricker, S., Lidbetter, T., and Marchand, H. (2017). Inference and beyond: further adventures with parity-based architectures for decentralized discrete-event systems. *IFAC-PapersOnLine*, 50(1), 13447–13452.

* Ricker, S. and Marchand, H. (2013). A parity-based architecture for decentralized discrete-event control. In *Am. Control Conf.*, 5678–5684.

* Rudie, K. and Wonham, W.M. (1992). Think globally, act locally: Decentralized supervisory control. *IEEE Trans. Autom. Control*, 37(11), 1692–1708.

* Takai, S. and Kumar, R. (2008). Synthesis of inference-based decentralized control for discrete event systems. *IEEE Trans. Autom. Control*, 53(2), 522–534.

* Takai, S. and Kumar, R. (2017). A generalized framework for inference-based diagnosis of discrete event systems capturing both disjunctive and conjunctive decision-making. *IEEE Trans. Autom. Control*, 62(6), 2778–2793.

* Takai, S. and Kumar, R. (2018). Implementation of inference-based diagnosis: computing delay bound and ambiguity levels. *Discrete Event Dyn. Syst.*, 28(2), 315–348.

* Yoo, T.S. and Lafortune, S. (2004). Decentralized supervisory control with conditional decisions: supervisor existence. *IEEE Trans. Autom. Control*, 49(11), 1886–1904.

* Yoon, S.H. and Stairs, M. (2015 - 2024). JDec. URL https://github.com/Summer2023SHY/JDec.