Multiple counters automata, safety analysis and presburger arithmetic

Abstract

We consider automata with counters whose values are updated according to signals sent by the environment. A transition can be fired only if the values of the counters satisfy some guards (the guards of the transition). We consider guards of the form yi#yj + Cij where yi is either x′i or x i, the values of the counter i respectively after and before the transition, and # is any relational symbol in {=,≤,≥,>,