View article

Knowing that a program has a bug is good, knowing its location is better, but a fix is best. We present a method to automatically locate and correct faults in a finite state system, either at the gate level or at the source level. We assume that the specification is given in Linear Temporal Logic, and state the correction problem as a game, in which the protagonist selects a faulty component and suggests alternative behavior. The basic approach is complete but as complex as synthesis. It also suffers from problems of readability: the correction may add state and logic to the system. We present two heuristics. The first avoids the doubly exponential blowup associated with synthesis by using nondeterministic automata. The second heuristic finds a memoryless strategy, which we show is an NP-complete problem. A memoryless strategy corresponds to a simple, local correction that does not add any state. The drawback of the …