Reduction Operators Based on Behavioral Inheritance for Timed Petri Nets


IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences   Vol.E97-A   No.2   pp.484-489
Publication Date: 2014/02/01
Online ISSN: 1745-1337
DOI: 10.1587/transfun.E97.A.484
Print ISSN: 0916-8508
Type of Manuscript: Special Section LETTER (Special Section on Mathematical Systems Science and its Applications)
timed Petri net,  timed branching bisimulation,  behavioral inheritnce,  

Full Text: PDF>>
Buy this Article

In this paper, we proposed reduction operators of timed Petri net for efficient model checking. Timed Petri nets are used widely for modeling and analyzing systems which include time concept. Analysis of the system can be done comprehensively with model checking, but there is a state-space explosion problem. Therefore, previous researchers proposed reduction methods and translation methods to timed automata to perform efficient model checking. However, there is no reduction method which consider observability and there is a trade-off between the amount of description and the size of state space. In this paper, first, we have defined a concept of timed behavioral inheritance. Next, we have proposed reduction operators of timed Petri nets based on timed behavioral inheritance. Then, we have applied our proposed operators to an artificial timed Petri net. Moreover, the results show that the reduction operators which consider observability can reduce the size of state space of the original timed Petri nets within the experiment.