A More Efficient Time Petri Net State Space Abstraction Useful to Model Checking Timed Linear Properties

Abstract

We consider here time Petri nets (TPN model). We first propose an abstraction to its generally infinite state space which preserves linear properties of the TPN model. Comparing with TPN abstractions proposed in the literature, our abstraction produces graphs which are both smaller and faster to compute. In addition, our characterization of agglomerated states allows a significant gain in space. Afterwards, we show how to apply Yoneda's partial order reduction technique to construct directly reduced graphs useful to verify LTL _{-X} properties of the model. Using our approach, both time and space complexities are reduced.

Finally, we propose a time extension for Büchi automata which is useful to model checking timed linear properties of the model, using the abstraction proposed here.