Linear-programming bounds on the mean marking and the throughputs of a stochastic timed Petri net. More...

#include <cmath>
#include <cstddef>
#include <limits>
#include <string>
#include <vector>
#include "line/api/mam/map_moment.h"
#include "line/api/spn/spn_sinvariants.h"
#include "line/lang/distribution.h"
#include "line/lang/lang_types.h"
#include "line/lang/qn/network_struct.h"
#include "line/util/error.h"
#include "line/util/lp_highs.h"
#include "line/util/simplex.h"

Include dependency graph for spn_lpbnd.h:

Classes
struct	line::spn::SpnLpOptions
	Options of the relaxation. More...
struct	line::spn::SpnLpMode
	One (transition, mode) pair over place levels. More...
struct	line::spn::SpnLpBounds
	The brackets; each vector pair holds the minimum then the maximum. More...

Namespaces
namespace	line
namespace	line::spn

Functions
template<class T>
SpnLpBounds	line::spn::spn_lpbnd (const qn::NetworkStruct< T > &sn, const SpnLpOptions &options=SpnLpOptions())
	Bracket the mean tokens and the throughputs of a stochastic Petri net.

Detailed Description

Linear-programming bounds on the mean marking and the throughputs of a stochastic timed Petri net.

The stationary chain is relaxed to a MOMENT POLYTOPE: the uniformized evolution equation is written for E[X_p], E[X_p^2] and E[X_p1 X_p2], which gives linear equalities among the mean marking x, the enabling probabilities q and the products y(p,t) = E[X_p e_t]; behavioural and probabilistic inequalities are added on top; and every reported measure is then obtained by minimising and maximising its linear form over that polytope. Any stationary point of the true chain satisfies every row, so the two optima BRACKET the exact value whatever the polytope leaves out.

This is the Petri-net sibling of the QRF bounds in SolverBA: same technique, a different index space, and a LINEAR objective, so there is no stationary point to escape from and the answer is a property of the model alone.

VARIABLES, over place levels l and modes e: x(l) the mean tokens, q(e) the probability that mode e is enabled, th(e) its throughput, u(e) the state-equation firing counts, and y(l,e) = E[X_l e_e] on the Markovian side only. u is EXISTENTIAL and is not reported: E[X] is a convex combination of reachable markings, each of which is m0 + C h for some nonnegative integer h, so the mean satisfies m0 + C u for some nonnegative real u.

ONE LEVEL PER PLACE, NOT PER (PLACE, CLASS), and a multiclass net is REFUSED. The other three codebases carry (nnodes x nclasses) arc matrices and so give a multiclass net P*R place levels. This port reads NetworkStruct::transparam, whose arcs are per (mode, NODE) with no class dimension, the same restriction spn_mdd states and enforces. A coloured net is a different model, not an approximation of this one, so it is refused rather than collapsed. spn_sinvariants is class-summed here for the same reason, which makes the invariant family (8) below the coarser one – still a genuine invariant, just not the finest.

THE INITIAL MARKING COMES FROM THE REFERENCE STATION of each closed class, or from SpnLpOptions::init: unlike the object-graph codebases, a NetworkStruct carries no per-place state to read instead. A net whose tokens do not all start at the reference station must pass init.

THE TOKEN COUNTS CREATED BY A FIRING ARE DETERMINISTIC IN LINE, which removes a whole branch of the reference: it allows sigma_(t,p)(n) to be random and splits the covariance family into an independent case (its eq. 7) and a selective one (its eq. 8). A firing outcome is an integer weight, so E[sigma^2] = sigma^2 and E[sigma_p1 sigma_p2] = sigma_p1 sigma_p2 hold exactly and eq. (7) is the correct form. Eq. (8) has no LINE model behind it and is deliberately absent.

LIVENESS IS OFF BY DEFAULT, AND THAT IS DELIBERATE. The reference's two liveness rows (sum_t q_t >= 1 and x_p <= sum_t y_(p,t)) hold only on a live net, and liveness is not something this function can cheaply certify – an inhibitor arc alone is enough to deadlock a net that looks well formed. A bound that silently assumed it would be wrong rather than loose on exactly the models where a bound is most wanted, so the rows are opt-in.

WHAT THE ROWS ARE WORTH, MEASURED. They are the whole of the lower side. On the reference's own Table 2 (its Fig. 2b production line, five rate vectors) assumelive reproduces its published l.b. column to four decimals – 1.1653 against 1.165, 1.8288 against 1.829, 1.5814 against 1.581, 1.3592 against 1.359, 1.3497 against 1.350 – while without them the Markovian lower bound collapses onto the OPERATIONAL one on four of the five. The upper side needs neither row and matches the published u.b.2 either way.

Reference: Z. Liu, "Performance Analysis of Stochastic Timed Petri Nets Using Linear Programming Approach", IEEE Trans. Software Engineering 24(11), 1998, 1014-1030. The constraint families are its Table 1, p. 1022; the bracket statement is its Theorem 3, p. 1021.

MATLAB twin: spn_lpbnd.m. JAR twin: Spn_lpbnd.java. Python twin: api/spn/lpbnd.py.

Definition in file spn_lpbnd.h.

Classes

Namespaces

Functions

Detailed Description