mdd_rec.h File Reference

MDD-rec: the normalising constant of a product-form model whose reachable set is held in a decision diagram. More...

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

Include dependency graph for mdd_rec.h:

Go to the source code of this file.

Namespaces
namespace	line
namespace	line::mdd

Typedefs
typedef std::vector< std::vector< bool > >	line::mdd::MddMask
	Per-level admissible local values, the restriction of Sec.

Functions
template<class T>
T	line::mdd::mdd_rec_masked (const MddStruct &mdds, const std::vector< std::vector< T > > &g, const MddMask &mask)
	Unnormalised mass of the masked subset of the reachable set (Algorithm 1).
template<class T>
T	line::mdd::mdd_rec (const MddStruct &mdds, const std::vector< std::vector< T > > &g)
	The normalising constant G = sum_{s in S} prod_l g_l(s_l).
template<class T>
std::vector< T >	line::mdd::mdd_rec_marginal (const MddStruct &mdds, const std::vector< std::vector< T > > &g, std::size_t l)
	Unnormalised masses of {s in S : s_l = k}, one per local value k of level l.

Detailed Description

MDD-rec: the normalising constant of a product-form model whose reachable set is held in a decision diagram.

S. Balsamo, A. Marin, I. Stojic, "Computation of the normalising constant for product-form models of distributed systems with synchronisation", Future Generation Computer Systems 111 (2020) 475-490, Sec. 4.

A product-form model has P(s) = (1/G) prod_k g_k(s_k) over its levels, and

G = sum_{s in S} prod_k g_k(s_k).

Summing state by state is exponential and numerically unstable. MDD-rec instead walks the diagram that already encodes S, accumulating the unnormalised mass of each node ONCE (Def. 4.4, Algorithm 1):

M(<l.p>) = sum_{v in S_l} g_l(v) * M(<l.p>[v]),   M(TRUE) = 1, M(FALSE) = 0

so the cost is O(sum_l |nodes_l| * |S_l|) rather than O(|S|), and G = M(root).

FORMALISM-AGNOSTIC. Nothing here knows what a level is: the paper's Appendix B shows that on the lattice sum_k s_k = n of a closed queueing network this collapses to Buzen's convolution, and Sec. 5 that on an S-invariant reachable Petri net it collapses to the Coleman-Henderson-Taylor convolution (spn::spn_conv). Unlike either, it needs only that the reachable set be finite and encoded – no lattice, no S-invariant reachability.

THE MASK is how Sec. 5.3 computes measures. Restricting the sum at level l to a subset of its local values gives the unnormalised mass of the corresponding subset of S, so P(m_l = k) and P(e_j >= k) are the same recursion under a different mask rather than three separate algorithms.

WHAT IS NOT HERE. The g_l themselves, and the test that the model has a product form at all, are the caller's: the paper declares that out of scope (Sec. 3.2) and refers to the per-formalism conditions instead. Passing g_l that do not describe a product-form model returns a number that is not the normalising constant of anything, and nothing here can detect it.

Definition in file mdd_rec.h.