Abstract
This paper concerns model-checking of fragments and extensions
of CTL* on infinite-state Presburger counter systems, where the
states are vectors of integers and the transitions are determined
by means of relations definable within Presburger arithmetic. In
general, reachability properties of counter systems are
undecidable, but we have identified a natural class of admissible
counter systems (ACS) for which we show that the quantification
over paths in CTL* can be simulated by quantification over tuples
of natural numbers, eventually allowing translation of the whole
Presburger-CTL* into Presburger arithmetic, thereby enabling
effective model checking. We provide evidence that our
results are close to optimal with respect to the class of counter
systems described above.