Abstract: Timed continuous Petri nets with infinite server semantics is a subclass of piecewise linear systems in which some state variables are redundant due to the P-flows. When the order of the system is reduced according to these conservation laws we obtain piecewise affine systems with continue flow at the borders. For these systems we offer a formal analysis technique abstracting the continuous behavior to a discrete representation in a transitions system. Two software packages have been developed. The first one takes an initial region and computes the safety regions, i.e., the region that cannot be reached starting from any point in the initial one while the second one accepts as input some regions and a formula in linear temporal logic (LTL) and computes the initial regions from which we can start and the formula is satisfied over the evolution. We will see how we can refine the abstraction hoping that at the next step the result is improved.