Title :
Reachability Analysis of Time Basic Petri Nets: A Time Coverage Approach
Author :
Bellettini, Carlo ; Capra, Lorenzo
Author_Institution :
Dept. of Inf. & Commun., Univ. degli Studi di Milano, Milan, Italy
Abstract :
We introduce a technique for reachability analysis of Time-Basic (TB) Petri nets, a powerful formalism for real time systems where time constraints are expressed as intervals, representing possible transition firing times, whose bounds are functions of marking´s time description. The technique consists of building a symbolic reach ability graph relying on a sort of time coverage, and overcomes the limitations of the only available analyzer for TB nets, based in turn on a time-bounded inspection of a (possibly infinite) tree-tree. The graph construction algorithm has been automated by a tool-set, briefly described in the paper together with its main functionality and analysis capability. A running example is used throughout the paper to sketch the symbolic graph construction. A use case describing a small real system - that the running example is an excerpt from - has been employed to benchmark the technique and the tool-set. The main outcome of this test are also presented in the paper. Ongoing work, in the perspective of integrating with a model-checking engine, is shortly discussed.
Keywords :
Petri nets; formal verification; reachability analysis; real-time systems; graph construction algorithm; marking time description; model checking engine; possibly infinite tree-tree; reachability analysis; realtime system; symbolic graph construction; symbolic reachability graph; time basic Petri nets; time constraint; time coverage approach; time-bounded inspection; transition firing time; use case; Buildings; Fires; Ignition; Petri nets; Reachability analysis; Semantics; Time factors; linear constraints; symbolic reachability analysis; timed Petri nets;
Conference_Titel :
Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), 2011 13th International Symposium on
Conference_Location :
Timisoara
Print_ISBN :
978-1-4673-0207-4
DOI :
10.1109/SYNASC.2011.16