Stochastic Time Petri Nets

Model Features

STPNs also define a probability density function (PDF) over the interval [a,b] of required values for the firing of each transition.

Initially, each enabled transition samples a firing time according to its PDF. The firing time acts as a "timeout": the transition with firing time is selected. Its firing time is equal to the sojourn time in the current state.

After the firing, the marking is updated according to the usual token moves (and PostUpdater function).

• Newly-enabled or reset transitions sample a new firing time
• Persistent transitions (enabled before the firing and during token moves) have a firing time reduced by the sojourn time in the previous state.

A firing time PDF is added to a transition as a StochasticTransitionFeature:

t3.addFeature(StochasticTransitionFeature.newUniformInstance("5", "15"));

Static factory methods are available in StochasticTransitionFeature to to create firing times with many PDF, such as uniform, deterministic, exponential, expolynomial (among others).

Analysis Engines

The library supports many analysis methods, for both transient and steady-state probabilities (and rewards). The applicability of these methods depends on the properties of the underlying stochastic process.

TreeTransient

The most general (but also computationally expensive) analysis method is TreeTransient, which builds a tree of transient stochastic state classes. Each node encodes a marking and the joint PDF of enabled transitions. These are used to compute the probability that the STPN is in any node of the tree (and thus it has its marking) at a given time instant.

The analysis can be configure through the builder of TreeTransient objects:

TreeTransient analysis = TreeTransient.builder()
    .timeBound(new BigDecimal("5"))
    .timeStep(new BigDecimal("0.1"))
    .build();

TransientSolution<Marking, Marking> result = analysis.compute(pn, marking);

System.out.println("The transient probabilities at time 1.0:");
for (int j = 0; j < result.getColumnStates().size(); j++) {
    System.out.printf("%1.6f -- %s%n", result.getSolution()[10][0][j],
            result.getColumnStates().get(j));
}

The available options when building TreeTransient are:

• timeBound(BigDecimal): specifies the maximum time used to select the time points where transient probabilities are computed (required).
• timeStep(BigDecimal): specifies the time step used to select time points in [0, timeBound] (required).
• policy(Supplier<EnumerationPolicy>): to use a custom policy to select the next state to explore in the tree (FIFO by default).
• stopOn(Supplier<StopCriterion>): to stop the analysis on some nodes (never by default).
• stopOn(MarkingCondition): to use a simple MarkingCondition as stop criterion.

Note that FIFO and LIFO policies expand all transition firings in the tree until an absorbing state (where no transition is enabled) is reached. In most circumstances, it is useful to exclude nodes that can be reached only after timeBound, or to ensure that the probability of reaching unexplored nodes before timeBound is lower than some error.

You can easily select this policy using the builder method greedyPolicy(timeBound, error):

TreeTransient analysis = TreeTransient.builder()
    .greedyPolicy(new BigDecimal("5"), BigDecimal.ZERO)
    .timeStep(new BigDecimal("0.1"))
    .build();

Nodes with higher reaching probability (the probability of the firing sequence from the root node) are explored first; the analysis ends when the total reaching probability of unexplored nodes is lower than the allowed error.

RegTransient

The analysis method RegTransient can be applied when the underlying stochastic process finds regenerations (i.e., states where all general timers are newly-enabled or with deterministic enabling time).

This method builds a tree of transient stochastic state classes from each regeneration until the next reachable regeneration. Each node of the tree encodes a marking and the joint PDF of enabled transitions. These are used to compute the global and local kernels of the underlying Markov regenerative process.

In turn, the kernels are used to solve (numerically) Markov renewal equations that provide the transient probability of all markings.

The analysis can be configured through the builder of RegTransient objects:

RegTransient analysis = RegTransient.builder()
    .timeBound(new BigDecimal("5"))
    .timeStep(new BigDecimal("0.1"))
    .build();

TransientSolution<DeterministicEnablingState, Marking> result =
    analysis.compute(pn, marking);

System.out.println("The transient probabilities at time 1.0:");
for (int j = 0; j < result.getColumnStates().size(); j++) {
    System.out.printf("%1.6f -- %s%n", result.getSolution()[10][0][j],
            result.getColumnStates().get(j));
}

The available options when building RegTransient are:

• timeBound(BigDecimal): specifies the maximum time used to select the time points where transient probabilities are computed (required).
• timeStep(BigDecimal): specifies the time step used to select time points in [0, timeBound] (required).
• policy(Supplier<EnumerationPolicy>): to use a custom policy to select the next state to explore in the tree (FIFO by default).
• stopOn(Supplier<StopCriterion>): to stop the analysis on some nodes (never by default).
• stopOn(MarkingCondition): to use a simple MarkingCondition as stop criterion.
• normalizeKernels(boolean): whether to normalize of global kernel (false by default). Without normalization, defective kernel rows produce probabilities that sum to less than 1, but they are guaranteed to be lower bounds of the exact values. With normalization, the output probabilities always sum to 1, but they can include an error (increasing over time) that overestimate or underestimate the exact values.

To exclude nodes that can be reached only after timeBound in each tree, or to ensure that the probability of reaching unexplored nodes before timeBound is lower than some error, you can select a greedy policy using the builder method greedyPolicy(timeBound, error):

RegTransient analysis = TreeTransient.builder()
    .greedyPolicy(new BigDecimal("5"), BigDecimal.ZERO)
    .timeStep(new BigDecimal("0.1"))
    .build();

Nodes with higher reaching probability (the probability of the firing sequence from the root node) are explored first; the analysis ends when the total reaching probability of unexplored nodes is lower than the allowed error.

RegSteadyState

The analysis method RegSteadyState can be applied when the underlying stochastic process finds regenerations in a bounded number of discrete events (e.g., within at most 20 transition firings).

This method builds a tree of transient stochastic state classes from each regeneration until the next reachable regeneration. Each node of the tree encodes a marking and the joint PDF of enabled transitions. The DTMC embedded at regeneration points is solved to find equilibrium probabilities of regenerations; these are combined through sojourn times in each marking to compute the final result.

Note that the current implementation assumes that the state space is irreducible.

The analysis can be launched using instances of RegSteadyState (in most cases, without any configuration):

RegSteadyState analysis = RegSteadyState.builder().build();

SteadyStateSolution<Marking> result = analysis.compute(pn, marking);
Map<Marking, BigDecimal> probs = result.getSteadyState();

System.out.println("Steady-state probabilities:");
for (Marking m : probs.keySet()) {
    System.out.printf("%1.6f -- %s%n", probs.get(m), m);
}

OneGenTransient: Analysis under enabling restriction

The analysis method OneGenTransient can be applied when the STPN has at most one general transition enabled in each state.

This method builds a the CTMC subordinated to each general transition; transient probabilities are then computed using uniformization and combined with the firing PDF of general transitions.

The analysis can be launched using instances of OneGenTransient:

OneGenTransient analysis = OneGenTransient.builder()
    .timeBound("5")
    .timeStep("0.1")
    .error("0.001")
    .build();

TransientSolution<DeterministicEnablingState, Marking> solution =
    analysis.compute(pn, m);

System.out.println("The transient probabilities at time 1.0:");
for (int j = 0; j < result.getColumnStates().size(); j++) {
    System.out.printf("%1.6f -- %s%n", result.getSolution()[10][0][j],
            result.getColumnStates().get(j));