Constructing Coverability Graphs for Time Basic Petri Nets

TL;DR

This paper presents a novel technique for constructing coverability graphs for Time Basic Petri nets, enabling analysis of unbounded models by leveraging time anonymity and coverage concepts.

Contribution

It introduces a coverability analysis method that guarantees termination for unbounded Time-Basic Petri nets using time anonymous tokens and coverage, handling models without Zeno behavior.

Findings

Constructs coverability graphs for unbounded Time-Basic Petri nets.

Guarantees termination for models with limited token growth.

Effectively manages models without Zeno behavior.

Abstract

Time-Basic Petri nets, is a powerful formalism for modeling real-time systems where time constraints are expressed through time functions of marking's time description associated with transition, representing possible firing times. We introduce a technique for coverability analysis based on the building of a finite graph. This technique further exploits the time anonymous concept [5,6], in order to deal with topologically unbounded nets, exploits the concept of a coverage of TA tokens, i.e., a sort of {\omega} anonymous timestamp. Such a coverability analysis technique is able to construct coverability trees/graphs for unbounded Time-Basic Petri net models. The termination of the algorithm is guaranteed as long as, within the input model, tokens growing without limit, can be anonymized. This means that we are able to manage models that do not exhibit Zeno behavior and do not express actions depending on infinite past events. This is actually a reasonable limitation because, generally, real-world examples do not exhibit such a behavior.