Combining Abduction and Model Checking Techniques for Repair of Concurrent Programs

Model-Based Validation of Intelligence

Volume

Papers from the 2001 AAAI Spring Symposium

Contents

Model checking is an approach to automated verification of finite-state concurrent systems such as circuit designs and communication protocols. In this approach, specifications are expressed in a temporal logic, and the concurrent system is modeled as a state transition graph which amounts to a Kripke structure for this logic. The most relevant advantage of model checking over other methods for verification of circuits and protocols is that it is efficient and highly automatic. Recent advances by using special data structures and algorithms, known as symbolic model checking, make it possible to verify systems with tremendously many states. On the other hand, various techniques for diagnostic reasoning on systems have been developed in the field of AI, including logic-based approaches like model-based diagnosis and repair. Our work approaches a new and promising field for application of AI techniques by proposing the enhancement of model checking by abductive reasoning, which is a major technique in AI and knowledge representation. We study the integration of model checking and AI principles by introducing the system repair problem in the context of Computational Tree Logic. The system repair problem amounts to an interesting abductive model revision problem: Determine by abductive reasoning a suitable change of the system (i.e., of its Kripke model) such that the specification is satisfied upon this change. We address to the issue of searching a program repair by developing optimization techniques which sensibly reduce the search space of solutions. Moreover, we formally extend the notion of counterexample which is a heuristically selected computation path from a conceptual counterexample tree (i.e., an evolving branching computation) that gives a hint at the failure of the system.