lu-1993 / Diagnosability

We show how to encode bounded diagnosability problem for finite automata in smt with the files available here
1 stars 0 forks source link

Does theoritical bound depend on the number of observable events? #2

Open jm62300 opened 3 years ago

jm62300 commented 3 years ago

@all Do you have some ideas about this question? Actually I don't know what is the theoretical bound, and if this bound is tight. If you have answers please use this issue to discuss about this point. JM

phdague commented 3 years ago

Sorry, I did not see your post. A critical pair is a path (from initial state) in the synchronized (on observable events) product of the fautly and correct parts of the automaton. If this one has N states, this product has a maximum of N^2 states. If we check standard diagnosability, i.e., for k = +infinity, a critical pair has to be a lasso (end by a cycle), which is necessarily the case if its length is equal to the number of states. So the theoretical bound TB is N^2 (take care that this is the bound for the length of the pair of paths in the product, not for the length of each individual path that we use in our coding (if I call it B, we have B≤TB≤2B, where the lower bound corresponds to none unobservable event in the critical pair and the upper bound to none observable event). Whatever, N^2 is thus also a theoretical bound for B. For k-diagnosability with k finite the theoretical bound for the length of the faulty path in the k-critical pair is equal to min(B^2, lF+k) where lF is the maximum length of a path from the initial state to the first occurrence of a fault in the automaton (I take the min with B^2 because if we discover a lasso, we can stop even if k is not reached). So it depends not only on k but how far can be a first fault from the initial state. Again the theoretical bound is thus N^2. So the theoretical bound does not depend on the number of observable events (except if this one is zero where the existence of a critical pair is guaranteed as far as there exists at least a faulty behavior and a correct behavior). I think that we can build example where N^2 is reached whatever is the nonnull ratio of observable events on total events.