On Parametric DBMs and Their Applications to Time Petri Nets

In the early stages of development, parameters are useful to verify timed systems that are not fully specified and symbolic algorithms or semi-algorithms are known to compute (integer) values of the parameters ensuring some properties. They rely on the representation of the reachable state-space as convex polyhedra. In the case of Parametric Timed Automata or Parametric Time Petri Nets (PTPN), those convex polyhedra have a special form that can be represented with a dedicated data structure called Parametric Difference Bound Matrices (PDBM). Surprisingly few results are available for PDBMs, so we take a fresh look at them and show how they can be computed efficiently in PTPNs. In the process, we define tropical PDBMs (tPDBMs) that generalize the original definition and allows, in contrast to that former definition, to avoid splitting the represented polyhedra. We argue in particular that while tPDBMs are more costly to handle than their split counterpart, they allow for better convergence. We have implemented both versions in Roméo, our tool for model-checking time Petri nets, and we compare the performance of the different polyhedron and (t)PDBM-based representations of symbolic states on several classical examples from the literature.