spn_conv.h File Reference

Convolution algorithm for the normalising constant of an S-invariant reachable product-form stochastic Petri net. More...

#include <cstddef>
#include <map>
#include <vector>
#include "line/api/spn/spn_sinvariants.h"
#include "line/num/number.h"
#include "line/util/error.h"

Include dependency graph for spn_conv.h:

Go to the source code of this file.

Namespaces
namespace	line
namespace	line::spn

Functions
template<class T>
T	line::spn::spn_conv (const std::vector< std::vector< long long > > &S, const std::vector< long long > &V, const std::vector< std::vector< T > > &g)
	The normalising constant by convolution over the invariant load vector.
template<class T>
T	line::spn::spn_conv (const SpnInvariants &inv, const std::vector< std::vector< T > > &g)
	Convolve straight off the invariant basis spn_sinvariants returned.

Detailed Description

Convolution algorithm for the normalising constant of an S-invariant reachable product-form stochastic Petri net.

J. Coleman, W. Henderson, P. Taylor, "Product form equilibrium distributions and a convolution algorithm for stochastic Petri nets", Performance Evaluation 26(3), 1996, 159-180; presented as the point of comparison for MDD-rec in S. Balsamo, A. Marin, I. Stojic, FGCS 111 (2020), Sec. 5.1.

With S the minimal-support S-invariant matrix and V = S m0 the load vector, the reachability set of an S-INVARIANT REACHABLE net is exactly {m >= 0 : S m = V}, and conditioning on the marking of one place partitions it (Lemma 5.1). Writing G_j(W) for the mass of the markings supported on the first j places with S m = W,

G_0(W) = [W == 0],     G_j(W) = sum_i g_j(i) G_{j-1}(W - i S_j),

and G = G_n(V). On a net whose only invariant is "the tokens are conserved" this is Buzen's convolution for a closed queueing network, one place per station.

NO ILP IS SOLVED. The paper obtains the marking set M_p(P',W) from the feasibility of an integer program (Prop. 5.2) so that the sum skips the terms that contribute nothing. Here the sum simply runs over i whose residual W - i S_j stays non-negative and the recursion returns zero on an infeasible residual, which gives the same value: the ILP is an optimisation of the enumeration, not part of the definition. Memoising on (j, W) keeps the walk over the reachable residuals rather than over all of them.

S-INVARIANT REACHABILITY IS NOT CHECKED, and cannot be cheaply: no algorithm is known that decides it without generating the reachability set (FGCS, Sec. 5.1). On a net that fails it, {m : S m = V} is strictly larger than the reachable set and this returns a normalising constant over unreachable markings too, which is why mdd::mdd_rec – which walks the reachable set itself – is the general algorithm and this one the special case. Compare the two on a new net before trusting this one on it.

Definition in file spn_conv.h.