Marius Bozga, Codruta Girlea and Radu Iosif
Iterating Octagons (2008)
Iterating Octagons (2008)
TR-2008-16.ps
Keywords: dbm,octagons,transitive closure
Abstract: In this paper we prove that the transitive closure of a non-deterministic 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 cite{comon-jurski98} and Bozga, Iosif and Lakhnech cite{icalp06} concerning the computation of transitive closures for difference bound relations. The importance of this result is justified by the wide use of octagons to computing sound abstractions of real-life systems cite{mine}. 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.
