An important effort has been devoted this year to the design of new data structures for symbolic representation of infinite state spaces. These efforts lead to the implementation of several packages allowing the representation and manipulation of sets of integer and real vectors.
The NDD and RVA packages have been developed by the group of Liège in the tool LASH. These data structures are based on finite-state automata and allow to express and manipulate efficiently linear arithmetical constraints on integers and reals.
The PDBM package has been developed by the groups of Paris (UP7) and Grenoble (UJF). PDBMs are parametric extensions of the Difference Bound Matrices used for the representation of a class of polyhedra called zones in the timed automata literature (corresponding to boolean combinations of interval constraints on differences between variables). In PDBMs, bounds of intervals can be parametric (arithmetical expressions including parameters), and parameters can be constrained using arithmetical formulas. A package allowing the manipulation of these data structures has been implemented in the tool TReX. This package uses internal decision procedures (e.g., a local implementation of the Fourier-Motzkin quantifier elimination procedure) as well as external decision procedures for arithmetics (Omega for Presburger arithmetics, and Reduce/Redlog for the arithmetics of reals).