Probabilistic verification of diagnosability for a certain class of timed stochastic systems (Q6174049)

The main interest here is in introducing probabilistic information in logical systems. The focus is in providing probabilistic verification of detection and isolation of faults of interest in logical discrete event systems. These detection and isolation are known as diagnosability. In this type of system the diagnoser must detect a fault after a finite number of operations. In timed discrete event systems the diagnosability is related to delays in units of time instead of in the number of operations. The introduction of the probabilistic information in logical systems allows a refinement of the analysis of such systems. In order to address the issues mentioned above, the authors consider labeled continuous-time Markov models. Hence, a section describing continuous-time Markov models (usual and labeled versions) is given together with the basic properties and results related to them. In the same section, the authors introduce the concept of faults pattern (usual and in the context of Markov models). The authors proceed to describe verifiers of labeled continuous-time Markov models. A series of definitions and lemmas are given. The description of the logical verifier design is presented, as well as the description of the probabilistic verifier. Throughout the presentation of these concepts, comprehensive examples are also given. Finally, the results related to the definitions and propositions of conditions for weak notions of diagnosability of faults pattern in a time stochastic framework are given. These are presented in forms of lemmas and propositions. Their proofs are given in detail. At the end of the work, ideas for future work are listed.