Interval Weighted Automata are a modeling formalism for timed systems that can be viewed as an alternative (more algebraic) to timed automata. We present here a way of deriving a deterministic interval weighted automaton to represent any bounded T-time Petri net subject to strong and single-server semantics. This approach consequently contributes to the characterization of the expressiveness of weighted automata with respect to other formalisms for timed Discrete Event Systems. In addition, the time language of the obtained abstraction has the characteristics of being included or equal to the time language of the T-time Petri net, and, in other words, any accessible state in the obtained Interval Weighted Automaton corresponds to an equally accessible state in the T-time Petri net. This property should allow the future use of this abstraction for the verification of properties that are expressed as an accessibility issue and/or for control.

This paper aims to explore the problem of verifying detectability for unambiguous weighted automata (UWAs) through the utilization of modified self-composition. Specifically, we focus on two types of detectability: strong periodic detectability (SPD) and strong D-detectability (SDD). The problem involves periodically determining the current state or distinguishing certain state-pairs of the system, based on the occurrence of a finite number of observable events. We introduce a new polynomial-time algorithm different from the detector, called self-composition for UWAs, and prove that it can be used to verify the SPD and SDD for UWAs. Ultimately, we propose necessary and sufficient conditions based on modified self-composition techniques to verify the aforementioned detectabilities for the studied UWA.

This article investigates diagnosability and$T$-diagnosability for discrete-event systems modeled by unambiguous max-plus automata (UMPAs). More precisely, diagnosability requires that the occurrence of any fault can be detected within a finite number of events after the fault has occurred.$T$-diagnosability requires that the occurrence of any fault can be detected within a delay of at most$T$time units after its occurrence. First, we propose a polynomial-time algorithm based on the construction of a nondeterministic finite automaton over a weighted alphabet for diagnosability verification of a UMPA. Second, we prove that$T$-diagnosability of a UMPA can be studied by reducing it to the problem of diagnosability. Third, we introduce an approach to calculate the upper on the time needed for detecting fault occurrence for a diagnosable UMPA, and its complexity is of sixth order in the number of states of the UMPA.

In this paper, a two-step approach for on-line fault diagnosis of timed discrete event systems modeled with max-plus automata is presented. The set of events is divided into two disjoint subsets, i.e., observable and unobservable subsets, and failures are associated to unobservable ones. Once a sequence of pairs (event, time-instant) is observed, the fault diagnosis problem consists in detecting an abnormality of the system evolution and isolating the source of this abnormality. For a max-plus automaton, we first propose an algorithm to build its augmented version whose states are partitioned into two disjoint parts, the normal part and the faulty part, with respect to a given fault class. Then we prove that solving fault diagnosis of the original automaton is equivalent to estimating the states of the augmented automaton. Finally, an algorithm is proposed to summarize how to perform on-line fault diagnosis using a state estimation based approach.

This paper deals with a software package, called MAISTeR, that has been developed in collaboration with industry, which is concerned with the optimization of manufacturing systems that also involve human resources. A global model of the production line (or part of the line) is obtained by concatenation of sub-models, using a new approach using feedforward and feedback transfer equations based on the formal theory of (max,+) algebra.