Diagnosability of labeled $\mathfrak{D_p}$ automata

TL;DR

This paper introduces a new diagnosability concept for labeled weighted automata over dioids, along with a novel verification tool called concurrent composition, expanding diagnosability analysis to more complex weighted systems.

Contribution

It presents a new diagnosability framework for weighted automata over dioids and develops the concurrent composition method for verification, which is a novel approach in this context.

Findings

Formulated diagnosability for weighted automata over dioids.

Developed the concurrent composition verification tool.

Established the fundamental novelty over existing literature.

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.