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 "+ ci,j where yi is either x' or xl, the values of the counter i respectively after and before the transition, and # is any relational symbol in =, <, >, >, <. We show that the set of possible counter values which can be reached after
any number of iterations of a loop is definable in the additive theory of N (or Z or R depending on the type of the counters). This result can be used for the safety analysis of multiple counters automata.
Users
Please
log in to take part in the discussion (add own reviews or comments).