A Decompositional Approach for Computing Least Fixed-Points of Datalog Programs with Z-Counters

. We present a method for characterizing the least fixed-points of a certain class of Datalog programs in Presburger arithmetic. The method consists in applying a set of rules that transform general computation paths into "canonical" ones. We use the method for treating the problem of reachability in the field of Petri nets, thus relating some unconnected results and extending them in several directions. Keywords: decomposition, linear arithmetic, least fixed-point, Petri nets, reachability set 1. Introduction The problem of computing fixpoints for arithmetical programs has been investigated from the seventies in an imperative framework. A typical application was to check whether or not array bounds were violated. A pionneering work in this field is the work by Cousot-Halbwachs (Cousot, 78). The subject has known a renewal of interest with the development of logic programming and deductive databases with arithmetical constraints. Several new applications were then possible in these f..