Efficient Image Computation in Infinite State Model Checking

In this paper we present algorithms for efficient image computation for systems represented as arithmetic constraints. We use automata as a symbolic representation for such systems. We show that, for a common class of systems, given a set of states and a transition, the time required for image computation is bounded by the product of the sizes of the automata encoding the input set and the transition. We also show that the size of the result has the same bound. We obtain these results using a linear time projection operation for automata encoding linear arithmetic constraints. We also experimentally show the benefits of using these algorithms by comparing our implementation with LASH and BRAIN.