Verification of Reachability Problems for Time Basic Petri Nets

TL;DR

This paper presents a novel symbolic reachability analysis technique for Time-Basic Petri nets, enabling finite state space construction and overcoming limitations of previous methods, with an automated tool and real-world benchmarking.

Contribution

It introduces the Time Anonymous concept and a finite contraction method for reachability analysis, improving over existing time-bounded approaches.

Findings

Successfully constructed finite symbolic reachability graphs

Automated the analysis with a Java tool-set

Validated effectiveness with real-world case study

Abstract

Time-Basic Petri nets, is a powerful formalism for model- ing 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 reachability analysis based on the building of finite contraction of the infinite state space associated with such a models. The technique constructs a finite symbolic reachability graph relying on a sort of time coverage, and over- comes the limitations of the existing available analyzers for Time-Basic nets, based in turn on a time-bounded inspection of a (possibly infinite) reachability-tree. A key feature of the technique is the introduction of the Time Anonymous concept, which allows the identification of components not influencing the evolution of a model. A running example is used throughout the paper to sketch the symbolic graph construction. The graph construction algorithm has been automated by a Java tool-set, described in the paper together with its main functionality and analysis capability. A use case describing a real-world example has been employed to benchmark the technique and the tool-set. The main outcome of this test are also presented in the paper.