Predicate abstraction in protocol verification

The paper shows how predicate abstraction can be applied to protocol verification. Predicate abstraction is a method for automatic construction of an abstract state graph. The basic idea is to use n predicates, phi₁,..., phi_n, defined on a concrete state space to generate an abstract state graph. Model checking is a formal verification technique which has been successfully applied to protocol verification. However, model checking can only be applied to finite state systems. Many interesting systems are infinite state or the number of states is so large that verification becomes infeasible. Predicate abstraction can be applied in the verification of infinite state systems (or large finite state systems). An abstract state graph created by predicate abstraction can be used for verification of safety properties using a model checker. We provide simple examples of protocol verification using predicate abstraction