Diagnosability of labeled $\mathfrak{D_p}$ automata

TL;DR

This work defines diagnosability for labeled weighted automata over progressive dioids, capturing both time elapse and spatial deviations through weight semantics. It introduces concurrent composition as a core verification tool and derives a necessary and sufficient condition for diagnosability, plus detailed complexity results: computing concurrent composition for $ ext{underline}{rak{Q}}$-automata is $ ext{NP}$-complete and diagnosing such automata is $ ext{coNP}$-complete, with the hardness persisting in deterministic, deadlock-free, and divergence-free cases; these results extend to vector progressive dioids $ ext{underline}{rak{Q}^k}$ and suggest a pathway to coNP membership for labeled real-time automata. The framework unifies time-like and space-like interpretations within a single algebraic setting and yields algorithmically implementable checks for diagnosability via CC_A, enabling analysis of systems with both negative weights and multi-dimensional coordinates. The findings advance diagnosability theory beyond classical LFSAs and timed automata, offering practical verification tools for complex discrete-event systems with rich weight structures.

Abstract

In this paper, we formulate a notion of diagnosability for labeled weighted automata over a class of dioids which admit both positive and negative numbers as well as vectors. The weights can represent diverse physical meanings such as time elapsing and position deviations. We also develop an original tool called concurrent composition to verify diagnosability for such automata. These results are fundamentally new compared with the existing ones in the literature.

Figures (7)

• Figure 1: A labeled $\underline{\mathbb{N}}$-automaton $\mathcal{A}_1^{\underline{\mathbb{N}}}$, where dioid $\underline{\mathbb{N}}$ is shown in \ref{['eqn27_diag_LMPautomata']}, $q_0$ is the unique initial state, $a$ is the observable event, $u,{\color{cyan} f}$ are unobservable events, i.e., $\ell(a)=a$, $\ell(u)=\ell({\color{cyan} f})=\epsilon$. $\color{cyan} f$ is the unique faulty event. The natural numbers after "$/$" denote the weights of the corresponding transitions.
• Figure 2: $\mathcal{A}_{1\mathsf{f}}^{\underline{\mathbb{N}}}$ (above) and $\mathcal{A}_{1\mathsf{n}}^{\underline{\mathbb{N}}}$ (below) corresponding to automaton $\mathcal{A}_1^{\underline{\mathbb{N}}}$ in Fig. \ref{['fig3_diag_LMPautomata']}.
• Figure 3: Illustration of diagnosability. Each line represents a path starting from an initial state, where the weighted label sequences of all dashed lines are the same as that of the solid line at the instant when the last event of the solid line occurs. Bullets denote faulty events. The circle denotes a stuck state.
• Figure 4: $\mathop{\mathrm{CC_A}}\nolimits(\mathcal{A}_{1\mathsf{f}}^{\underline{\mathbb{N}}},\mathcal{A}_{1\mathsf{n}}^{\underline{\mathbb{N}}})$ corresponding to automaton $\mathcal{A}_1^{\underline{\mathbb{N}}}$ in Fig. \ref{['fig3_diag_LMPautomata']}.
• Figure 5: A labeled $\underline{\mathbb{Q}}$-automaton $\mathcal{A}_2^{\underline{\mathbb{Q}}}$, where $\ell(a)=a$, $\ell({\color{cyan} f})=\ell(u)=\epsilon$, only $\color{cyan} f$ is faulty.

Theorems & Definitions (39)

• Lemma 2.1: Nykanen2002ExactPathLength
• Definition 2.2
• Lemma 2.3
• Example 1
• Example 2
• Definition 2.4
• Lemma 2.5
• proof
• Remark 1
• Example 3