The model checking of counters systems often reduces to the effective computation of the set of predecessors Pre~* (X′) of a Presburger-definable set X′. Because there often exists an integer k ≥ 0 such that Pre~(≤ k)(X′) = Pre~*(X′) we will first look for an efficient algorithm to compute the set Pre(X) in function of X. In general, such a computation is exponential in the size of X. In [BB03], the computation is proved to be polynomial for a restrictive class of counters systems. In this article we show that for any counters systems, the computation is polynomial. Then we show that the computation of Pre~(≤K)(X′) is polynomial in k (and exponential in the dimension m) for effective counters systems with interval-definable sets.
展开▼
