Region-based analysis of hybrid Petri nets with a single general one-shot transition
conference paper
Recently, hybrid Petri nets with a single general one-shot transition (HPnGs) have been introduced together with an algorithm to analyze their underlying state space using a conditioning/deconditioning approach. In this paper we propose a considerably more efficient algorithm for analysing HPnGs. The proposed algorithm maps the underlying state-space onto a plane for all possible ring times of the general transition s and for all possible systems times t. The key idea of the proposed method is that instead of dealing with in nitely many points in the ts-plane, we can partition the state space into several regions, such that all points inside one region are associated with the same system state. To compute the probability to be in a speci c system state at time τ, it suffices to nd all regions intersecting the line t = τ and decondition the ring time over the intersections. This partitioning results in a considerable speed-up and provides more accurate results. A scalable case study illustrates the efficiency gain with respect to the previous algorithm.
Topics
TNO Identifier
954343
ISSN
03029743
ISBN
9783642333644
Publisher
Springer
Source title
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 10th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2012, 18 September 2012 through 20 September 2012
Pages
139-154
Files
To receive the publication files, please send an e-mail request to TNO Repository.