The method of stochastic state classes provides a new approach for the
analysis of non-Markovian stochastic Petri Nets, which relies on the
stochastic expansion of the graph of non-deterministic state classes based
on Difference Bounds Matrix (DBM) which is usually employed in qualitative
verification.
In so doing, the method is able to manage multiple concurrent
non-exponential (GEN) transitions and largely extends the class of models
that are amenable to quantitative evaluation.
However, its application requires that every cycle in the graph of
non-deterministic state classes visits at least a regeneration point where
all GEN transitions are newly enabled.
In particular, this rules out models whose non-deterministic class graph
includes cycles within a Continuous Time Markov Chain (CTMC) subordinated
to the activity period of one or more GEN transitions.
In this paper, we propose an extension that overcomes this
limitation by aggregating together classes that are reached
through firings that do not change the enabling status of GEN
transitions.
This enlarges the class of models that can be analysed through the
method of stochastic state classes and makes it become a proper
extension of the class of models that satisfies the so called
enabling restriction.