Model Checking and Artificial Intelligence

Abstract

Exploration of very large search spaces lies at the heart of many disciplines in computer science and engineering, especially systems verification and artificial intelligence. In particular, the technique of model checking is used to automati- cally verify the properties of a system. In the model checking approach, verifying that a system S satisfies a property P is investigated by automatically checking the satisfiability of the expression MS |= φP,where MS is a suitable model rep- resenting all evolutions of S,and φP is a logical formula capturing the property P to be checked. Model checking and artificial intelligence have enjoyed a healthy interchange of ideas over the past few years. On the one hand, model checking techniques have benefited from efficient search algorithms developed in artificial intelligence thereby increasing their efficiency, on the other, model checking techniques have been extended to deal with typical artificial intelligence formalisms, such as epistemic logics, thereby permitting the verification of systems based on artificial intelligence concepts. In addition to this, there remains a keen interest among researchers to use model checking to solve planning problems.