Faster acceleration of counter automata in practice

Abstract

We compute reachability sets of counter automata. Even if the reachability set is not necessarily recursive, we use symbolic representation and acceleration to increase convergence. For functions defined by translations over a polyhedral domain, we give a new acceleration algorithm which is polynomial in the size of the function and exponential in its dimension, while the more generic algorithm is exponential in both the size of the function and its dimension. This algorithm has been implemented in the tool FAST. We apply it to a complex industrial protocol, the TTP membership algorithm. This protocol has been widely studied. For the first time, the protocol is automatically proved to be correct for 1 fault and N stations, and using abstraction we prove the correctness for 2 faults and N stations also. Keywords: acceleration, counter automata, reachability set, convex translation, TTP protocol. © Springer-Verlag 2001.