School of
Information Technology and Electrical Engineering

Model Checking and Counterexample Generation

Sentot KromodimoeljoWed, 16/01/2013 - 09:30
Prof Peter Lindsay and Ian Hayes

Existing model checkers focus on the verification problem where counterexamples are of secondary importance. They usually stop after finding the first counterexample. In this presentation, I will describe a prototype LTL model checker for Behavior Trees that will be able to generate a collection of counterexamples, where each counterexample is a representative of a class and the classes are exhaustive. Such a feature will increase the utility of a model checker since often we would like to know all ``interesting'' counterexamples. For example, in safety analysis, we might know that hazardous conditions cannot be completely eliminated, but we would like to know the situations that can lead to them. The prototype generates the set of counterexample states that corresponds to a Generalised Buchi automaton that is the intersection of the model automaton and the automaton for the negation of the property checked. The prototype uses an adaptation of Kildall's algorithm to compute reachable states.

Seminar Type: 

Mid-Candidature Review