Iterating Octagons

Abstract. In this paper we prove that the transitive closure of a nondeterministic octagonal relation using integer counters can be expressed in Presburger arithmetic. The direct consequence of this fact is that the reachability problem is decidable for flat counter automata with octagonal transition relations. This result improves the previous results of Comon and Jurski [7] and Bozga, Iosif and Lakhnech [6] concerning the computation of transitive closures for difference bound relations. The importance of this result is justified by the wide use of octagons to comound abstractions of real-life systems [15]. We have implemented the octagonal transitive closure algorithm in a prototype system for the analysis of counter automata, called FLATA, and we have experimented with a number of test cases.

• Type: Conference
• Year: 2009
• Where: TACAS
• Authors: Marius Bozga, Codruta Gîrlea, Radu Iosif
• Keywords: Algorithms, Counter Automata, Octagonal, TACAS 2009, Transitive Closure