Abstraction from counters: an application on real-time systems

We present abstraction techniques for systems containing counters, which allow us to significantly reduce their state spaces for their efficient verification. In contrast to previous approaches, our abstraction technique lifts the entire verification problem, i.e., also the specification, to the abstract level. As an application, we consider the reduction of real-time systems by replacing discrete clocks of timed automata with abstract counters. The presented method allows the reduction of such systems to very small state spaces. As benchmark examples, we consider the generalized railroad crossing and Fischer´s mutual exclusion protocol