Affiliations: Department of Computer Engineering, École
Polytechnique de Montréal P.O. Box 6079, Station Centre-ville,
Montréal, Québec,Canada, H3C 3A7. {hanifa.boucheneb,
hind.rakkay}@polymtl.ca
Note: [] Address for correspondence: Department of Computer Engineering,
École Polytechnique de Montréal, P.O. Box 6079,
Station Centre-ville, Montréal, Québec, Canada, H3C 3A7
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.
Keywords: Time Petri nets, state class graph, state explosion problem, partial order techniques, independent transitions, timed linear properties, Interval timed Büchi automata
