For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
Reduction Operators Based on Behavioral Inheritance for Timed Petri Nets
Ichiro TOYOSHIMA Shota NAKANO Shingo YAMAGUCHI
IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 2014/02/01
Online ISSN: 1745-1337
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>>
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.