Diagnosis is Repair
Stefan Staber, Barbara Jobstmann, Roderick Bloem · 2005
We argue that for sequential circuits, fault localization and repair are one and the same problem. We assume that a specification is given in linear temporal logic and we solve the diagnosis and repair problem for finite-state programs using games. Our approach is sound and it is complete if the specification is an invariant. In contrast to known approaches, the repair we find is valid for all possible input sequences, not just for one given test case. We show the applicability of our approach, which has a complexity comparable to that of model checking, on a set of examples. 1