Constructing Coverability Graphs for Time Basic Petri Nets
This work addresses a specific challenge in formal verification for real-time systems, representing an incremental advancement in handling unbounded nets.
The paper tackles the problem of coverability analysis for unbounded Time-Basic Petri nets, a formalism for modeling real-time systems, by introducing a technique that constructs finite coverability trees/graphs, with termination guaranteed under conditions like no Zeno behavior.
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 ω 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.