Predicate Abstraction in Protocol Verification

This paper presents how predicate abstraction can be applied to protocol verification. Predicate abstraction is a method for automatic construction of abstract state graph. Basic idea is to use n predicates 1, ..., n defined on concrete state space to generate abstract state graph. Model checking is a formal verification technique which has been successfully applied to protocol verification. But model checking can only be applied to finite state systems. Many interesting systems are innite state or number of states is so large that verification becomes infeasible. Predicate abstraction can be applied in verification of infinite state systems (or large finite state systems). 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