Effective Verification of Weak Diagnosability
Résumé
The diagnosability problem can be stated as follows: does a given labeled Discrete Event System allow for an outside observer to determine the occurrence of the "invisible" fault, no later than a bounded number of events after that unobservable occurrence, and based on the partial observation of the behaviour? When this problem is investigated in the context of concurrent systems, partial order semantics induces a separation between classical or strong diagnosability on the one hand, and weak diagnosability on the other hand. The present paper presents the first solution for checking weak diagnosability, via a verifier construction.