In Model Based Diagnosis, diagnosing a situation consists in comparing the behavior of the system within its fault (or correct) model in order to find explanation(s). In the case of discrete systems, the model is usually an automaton labeled by two types of actions: the observed ones and the unobserved ones. When dealing with fault model we distinguish among the unobserved events a set of fault events. Diagnosability is the study of the capability of the model to detect faults and also discriminate between different types of faults within.
The observation of an infinite iteration of (ab) on the system, can be explained, according to the model A, either by the run u1 or by u2f followed by an infinity of (ab). We can deduce that this model do not have the capability to discriminate between a correct execution and a faulty execution (two ambiguous runs), we say that the fault f is nondiagnosable in A. A formal definition of diagnosability was given in (Sampath et al., 1995). The definition stands that a fault in a system is diagnosable if and only if, we can not find two infinite runs that produces the same observable and one contains the fault on other not. Many works other than (Sampath et al., 1995) proposed solutions to check the diagnosability, (Cimatti et al., 2003)etc.
Let we now consider the same fault model but we change slightly the meaning of the events. All the internal events are considered controllable by the system. A part of the observable ones are no longer controlled by the system (e.g commands).
sider that b and c are now uncontrollable. Even by making this modification, the classical diagnosability definition and methods still consider f as non diagnosable. But, we can observe that infinitely often, for the ambiguous observation (ab)∞, one can give the system the event c instead of b and then within finite steps of observations (here one) we can say without ambiguity that f did (by observing d) or did not (by observing a) happen. In fact f is diagnosable. This toy example shows the limit of the classical definition of diagnosability to cover some types of systems.
Let AE be a transition system which has the same observable events as A but with inverse controllability labels, call AE an environment of A. Let we consider asynchronous interaction between the system and the environment on the observable events. We can consider this interaction as a game between the two systems. The system wins if it has a strategy (by choosing its controllable moves) to control the interaction in order to keep infinitely the ambiguity. In the opposite the environment wins if each time an ambiguity appears then it has a strategy to resolve it within a finite set of moves.
In this work we generalize the definition of diagnosability by using game structures and strategies framework. We give a method to synthesis the environment and generate the game structure. Then we use Alternating-Time Temporal Logic to check the existence of wining strategies for the environment in order to decide whether a system is diagnosable or not.
How to Cite
discrete-event systems, diagnosability analysis, controllability, game structure, Alternating-time Temporal Logic
(Sampath et al., 1995) M. Sampath, R. Sengupta, S. Lafortune, K. Sinnamohideen, and D. Teneket- zis. Diagnosability of discrete event systems. IEEE Trans. on Automatic Control, 40(9):1555–1575, September 1995.
The Prognostic and Health Management Society advocates open-access to scientific data and uses a Creative Commons license for publishing and distributing any papers. A Creative Commons license does not relinquish the author’s copyright; rather it allows them to share some of their rights with any member of the public under certain conditions whilst enjoying full legal protection. By submitting an article to the International Conference of the Prognostics and Health Management Society, the authors agree to be bound by the associated terms and conditions including the following:
As the author, you retain the copyright to your Work. By submitting your Work, you are granting anybody the right to copy, distribute and transmit your Work and to adapt your Work with proper attribution under the terms of the Creative Commons Attribution 3.0 United States license. You assign rights to the Prognostics and Health Management Society to publish and disseminate your Work through electronic and print media if it is accepted for publication. A license note citing the Creative Commons Attribution 3.0 United States License as shown below needs to be placed in the footnote on the first page of the article.
First Author et al. This is an open-access article distributed under the terms of the Creative Commons Attribution 3.0 United States License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original author and source are credited.