Multi-state reliability with MDDs: problem statement about dd HOT 9 CLOSED

It seems that probability computations using MDDs would be similar to probability computations using BDDs, assuming that each variable takes each of its integer values with some probability that is given (similarly to how the probabilities for the Boolean-valued variables were given, with the difference that each integer value would have a probability assigned).

About the conversion from MDDs to BDDs, this is not currently implemented (the reverse conversion is implemented). If the probability is directly computed on the MDD (with a recursive function), converting to a BDD may not be needed. Also, even if the MDD is converted to a BDD, it is not clear how the probabilities would be represented there (since the BDD variables will represent bits of random variables that are integer-valued, instead of Boolean-valued random variables).

from dd.

Regarding the first paragraph, you are right that the BDD and MDD probability calculations are similar. In the former, we calculated the probability of a top Boolean expression that is a sum of products of simple independent events such as u = xyz + pqr + xp, for example.

With the multi-state, we need equally to specify a top expression such as u = (x_1)(y_2)(z_3)+(p_1)(q_2)(r_3)+(x_2)(p_2) (where the indices indicate the multiple states of each variable, each a simple event). However, in your example on MDDs, https://github.com/tulip-control/dd/blob/master/doc.md#multi-valued-decision-diagrams-mdd, there is an example where rather than defining u as Boolean expression of simple events, u is defined as a Boolean expression of bits. Is there a way I could define u as a Boolean expression of simple events, not bits?

Another way of asking is the following: Going back to the Brayton article you mentioned (below), it looks like you’re using binary encoding, whereas my use-case is more naturally dealt with one-hot encoding. Is one-hot encoding available in tulip dd?

Arvind Srinivasan, Timothy Kam, Sharad Malik, Robert K. Brayton
"Algorithms for discrete function manipulation"
IEEE International Conference on
Computer-Aided Design (ICCAD), 1990
pp.92--95

from dd.

Definition of BDDs from expressions containing equality, numerals, and integer-valued variables is possible using the package omega. These BDDs could then be converted to MDDs using the function dd.mdd.bdd_to_mdd. This approach is using a binary encoding. A one-hot encoding would need to be implemented separately, though with a one-hot encoding it seems to me that the algorithm for computing the probability over a BDD would not anymore be a recursion over single levels, but rather blocks of bit levels.

from dd.

For example:

from omega.symbolic import temporal as trl

aut = trl.Automaton()
aut.declare_variables(x=(1, 3), y=(-3, 3))
u = aut.add_expr('x = 1 /\ y \in 1..2')  # This is a `dd.autoref.Function` or a `dd.cudd.Function`,
    # depending on what parts of `dd` are installed

The ranges of the bitvectors that get created for each integer variable are between powers of 2. So appropriate constraints are needed when defining formulas that are expected to be FALSE outside a given set of values.

from dd.

Thanks for the example. Can you help me better understand the syntax? Is it as following? (I changed the code slightly, still runs).

aut.declare_variables(x=(1, 3), y=(1, 5))
u = aut.add_expr('x = 1 /\ y =3')

Variable declaration: 
        x is in {x1,x2,x3}, y is in {y1,y2,y3,y4,y5}

define u: 
       u= x1 /\ y3

Can I plot this as BDD and MDD?

If not this interpretation, is it possible to use omega to define multi-state variables as I intend?

from dd.

The declaration x=(1, 3) communicates the intention of x taking the values 1, 2, 3. To ensure this is possible, the class omega.symbolic.temporal.Automaton creates a bitfield to represent x that allows x to take the values 0, 1, 2, 3 (the bitfield is implemented using a Python list). Similarly, y=(1, 5) results in a y that can take the values 0, 1, 2, 3, 4, 5, 6, 7. These ranges of values result because the number of bits in each case is selected large enough to accommodate for the intended range of values, so the actual range is (for an intended range of positive values) 0..(2^n - 1), where n the number of bits in the bitfield.

To create a formula that describes the range x \in {1, 2, 3} (written also as x \in 1..3, which is TLA+ syntax and is understood by the method Automaton.add_expr), one would write u = aut.add_expr('x = 1 \/ x = 2 \/ x = 3') or u = aut.add_expr('x \in 1..3'). In other words, that x # 0 needs to be explicitly stated.

Plotting as a BDD can be done using the BDD manager accessible as the attribute aut.bdd, and plotting as an MDD by first converting to an MDD (having instantiated separately an MDD manager). The conversion to an MDD requires the names of bits used to represent each integer-valued variable. These bit names can be found at the attribute aut.vars, for example aut.vars['x']['bitnames'].

My understanding is that integer-valued variables can be used, with the appropriate range constraints, to represent probability distributions for events with multiple outcomes.

from dd.

I was able to plot the BDD u above to a pdf before, but had an accident and lost the code. Could you help again? Failed attempt:

from dd.bdd import BDD as bdd
from omega.symbolic import temporal as trl
aut = trl.Automaton()

aut.declare_variables(x=(0, 3), y=(0, 1))
u=aut.add_expr('x = 0 /\ y = 0')

bdd.dump('example_1.pdf',[u])

from dd.

As mentioned above (#71 (comment)), the BDD manager is aut.bdd so plotting would be aut.bdd.dump('example_1.pdf', [u]).

from dd.

It seems that probability computations using MDDs would be similar to probability computations using BDDs, assuming that each variable takes each of its integer values with some probability that is given (similarly to how the probabilities for the Boolean-valued variables were given, with the difference that each integer value would have a probability assigned).

About the conversion from MDDs to BDDs, this is not currently implemented (the reverse conversion is implemented). If the probability is directly computed on the MDD (with a recursive function), converting to a BDD may not be needed. Also, even if the MDD is converted to a BDD, it is not clear how the probabilities would be represented there (since the BDD variables will represent bits of random variables that are integer-valued, instead of Boolean-valued random variables).

This is the right approach, a recursive function that is analogous to the BDD case. In order to implement this, we need to access the children node of a given node in the MDD. Whereas in the BDD we accessed the children nodes as u.low and u.high, how do we access the children node in the MDD?

from dd.