Analyzing Automata with Presburger Arithmetic and Uninterpreted Function Symbols
Vlad Rusu, Elena L. Zinovieva · Electronic Notes in Theoretical Computer Science · 2001
We study a class of extended automata defined by guarded commands over Presburger arithmetic with uninterpreted functions. On the theoretical side, we show that the bounded reachability problem is decidable in this model. On the practical side, the class is useful for modeling programs with unbounded data structures, and the reachability procedure can be used for symbolic simulation, testing, and verification.