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 [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 computing sound 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. © 2009 Springer Berlin Heidelberg.
CITATION STYLE
Bozga, M., Gîrlea, C., & Iosif, R. (2009). Iterating octagons. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5505 LNCS, pp. 337–351). https://doi.org/10.1007/978-3-642-00768-2_29
Mendeley helps you to discover research relevant for your work.