Generalizing diagnosability definition and checking for open systems: a Game structure approach

Abstract

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.