使用多值 DD 求解多状态可靠性量化
Using multivalue DDs to solve multistate reliability quantification
@DCTLib,你还记得下面的讨论吗?你提出了一个递归方程,这是正确的方法。
现在,我正在考虑多状态可靠性,在这种情况下,我们可以不失败或失败 n-1 个不同的状态,其中 n >= 2。Tulip-dd 实现 MDD,如中所述:
https://github.com/tulip-control/dd/blob/master/doc.md#multi-valued-decision-diagrams-mdd
https://github.com/tulip-control/dd/issues/71
https://github.com/tulip-control/dd/issues/66
在下面的图表中,我们定义了一个 MDD,声明为:
aut.declare_variable(x=(0,3))
u = aut.add_expr(‘x=i’)
多值变量 (MSV) x、x=0、x=1、x=2 或 x=3 的每个 value/state 都导致特定的 BDD,如图表所示底部,这里以一个四态变量 x 为例。符号是状态 0 表示正常状态,x 可以失败到不同的状态 1、2 和 3。失败概率在下面的 table 中指定。在下面的 BDD 中,我们(以及郁金香)使用具有两位 x_1 和 x_0 的二进制编码来表示 MSV 的每个 state/value。最低有效位 (LSB),即 x_0,始终是祖先。下面的每个 BDD 图都是特定值或状态的表示。
为了量化特定状态(即顶级节点)的 BDD,我们必须知道二进制变量 x_0 和 x_1 在 BDD 中采用不同分支(then 或 else)的概率。这些分支概率并没有直接给出,需要根据BDD结构计算
这里的关键是在计算父节点概率之前,必须知道子节点概率和父节点的分支概率。
在前面的BDD量化中,我们在计算节点x_1概率时,知道了从节点x_1分支到叶子节点的概率。我们不需要知道节点 x_1 是如何连接到节点 x_0 的。
现在,对于这个四态变量 x,我们需要知道节点 x_1 是如何连接到节点 x_0 的,二进制变量表示最低有效位,以确定从节点 [= 分支的概率48=] 到叶节点。问题是如何实现?
Here’s one attempt that falls short:
import numpy as np
from omega.symbolic import temporal as trl
aut = trl.Automaton()
# Example of function that returns branch probabilities
def prntr(v, pvars):
assert sum(pvars)==1.0,"Probs must add to 1!"
if (v.high).var == 'x_1':
if (v.low) == aut.true:
return pvars[1] + pvars[3], pvars[1]
else:
return pvars[1] + pvars[3], pvars[3]
if (v.low).var == 'x_1':
if (v.low).negated:
return pvars[1] + pvars[3], pvars[0]
else:
return pvars[1] + pvars[3], pvars[2]
aut.declare_variables(x=(0, 3))
u=aut.add_expr('x = 3')
pvars = np.array([0.1, 0.2, 0.3, 0.4])
prntr(u,pvars)
The key here is that the child node probabilities and the branch probabilities of the parent node must be known prior to the calculation of the parent node probability.
是的,没错。在这种情况下,由于您编写的原因,完全递归的自下而上计算(如通常使用 BDD 所做的那样)将不起作用。
但是,当您将一起构成一个状态的变量视为一个块时,该方法将再次开始起作用。所以在你的概率计算的递归函数中,每当你遇到一个块的变量时,你将相同状态分量的节点和后继节点视为一个块,并且只有在遇到不属于该块的节点时才递归。
请注意,此方法要求状态变量连续出现在变量排序中。对于 CUDD 库,您可以限制自动变量重新排序以保证这一点。
以下代码是您实现此想法的修改:
#!/usr/bin/env python3
import numpy as np
from omega.symbolic import temporal as trl
aut = trl.Automaton()
# Example of function that returns branch probabilities
# Does not yet use result caching and does not yet support assigning probabilities
# to more than one state variable set
def prntr(v, pvars):
assert abs(sum(pvars)-1.0)<=0.0001,"Probs must add to 1!"
if v == aut.true:
return 1.0
elif v == aut.false:
return 0.0
if v.var in ["x_0","x_1"]:
thisSum = 0.0
# Compute probabilities
for i,p in enumerate(pvars):
# Find successor
# Assuming that x_2 always comes after x_1
thisV = v
negate = thisV.negated
if thisV.var == 'x_0':
if i & 1:
thisV = thisV.high
else:
thisV = thisV.low
negate = negate ^ thisV.negated
if thisV.var == 'x_1':
if i & 2:
thisV = thisV.high
else:
thisV = thisV.low
if negate:
thisSum += p*prntr(~thisV, pvars)
else:
thisSum += p*prntr(thisV, pvars)
return thisSum
# TODO: What is the semantics for variables outside of the current block?
return 0.5*prntr(v.high, pvars) + 0.5*prntr(v.low, pvars)
pvars = np.array([0.1, 0.2, 0.3, 0.4])
aut.declare_variables(x=(0, 3))
u= aut.add_expr('x = 0')
print(prntr(u,pvars))
u2 = aut.add_expr('x = 3') | aut.add_expr('x = 2')
print(prntr(u2,pvars))
@DCTLib,你还记得下面的讨论吗?你提出了一个递归方程,这是正确的方法。
现在,我正在考虑多状态可靠性,在这种情况下,我们可以不失败或失败 n-1 个不同的状态,其中 n >= 2。Tulip-dd 实现 MDD,如中所述:
https://github.com/tulip-control/dd/blob/master/doc.md#multi-valued-decision-diagrams-mdd
https://github.com/tulip-control/dd/issues/71
https://github.com/tulip-control/dd/issues/66
在下面的图表中,我们定义了一个 MDD,声明为:
aut.declare_variable(x=(0,3)) u = aut.add_expr(‘x=i’)
多值变量 (MSV) x、x=0、x=1、x=2 或 x=3 的每个 value/state 都导致特定的 BDD,如图表所示底部,这里以一个四态变量 x 为例。符号是状态 0 表示正常状态,x 可以失败到不同的状态 1、2 和 3。失败概率在下面的 table 中指定。在下面的 BDD 中,我们(以及郁金香)使用具有两位 x_1 和 x_0 的二进制编码来表示 MSV 的每个 state/value。最低有效位 (LSB),即 x_0,始终是祖先。下面的每个 BDD 图都是特定值或状态的表示。
为了量化特定状态(即顶级节点)的 BDD,我们必须知道二进制变量 x_0 和 x_1 在 BDD 中采用不同分支(then 或 else)的概率。这些分支概率并没有直接给出,需要根据BDD结构计算
这里的关键是在计算父节点概率之前,必须知道子节点概率和父节点的分支概率。 在前面的BDD量化中,我们在计算节点x_1概率时,知道了从节点x_1分支到叶子节点的概率。我们不需要知道节点 x_1 是如何连接到节点 x_0 的。 现在,对于这个四态变量 x,我们需要知道节点 x_1 是如何连接到节点 x_0 的,二进制变量表示最低有效位,以确定从节点 [= 分支的概率48=] 到叶节点。问题是如何实现?
Here’s one attempt that falls short:
import numpy as np
from omega.symbolic import temporal as trl
aut = trl.Automaton()
# Example of function that returns branch probabilities
def prntr(v, pvars):
assert sum(pvars)==1.0,"Probs must add to 1!"
if (v.high).var == 'x_1':
if (v.low) == aut.true:
return pvars[1] + pvars[3], pvars[1]
else:
return pvars[1] + pvars[3], pvars[3]
if (v.low).var == 'x_1':
if (v.low).negated:
return pvars[1] + pvars[3], pvars[0]
else:
return pvars[1] + pvars[3], pvars[2]
aut.declare_variables(x=(0, 3))
u=aut.add_expr('x = 3')
pvars = np.array([0.1, 0.2, 0.3, 0.4])
prntr(u,pvars)
The key here is that the child node probabilities and the branch probabilities of the parent node must be known prior to the calculation of the parent node probability.
是的,没错。在这种情况下,由于您编写的原因,完全递归的自下而上计算(如通常使用 BDD 所做的那样)将不起作用。
但是,当您将一起构成一个状态的变量视为一个块时,该方法将再次开始起作用。所以在你的概率计算的递归函数中,每当你遇到一个块的变量时,你将相同状态分量的节点和后继节点视为一个块,并且只有在遇到不属于该块的节点时才递归。
请注意,此方法要求状态变量连续出现在变量排序中。对于 CUDD 库,您可以限制自动变量重新排序以保证这一点。
以下代码是您实现此想法的修改:
#!/usr/bin/env python3
import numpy as np
from omega.symbolic import temporal as trl
aut = trl.Automaton()
# Example of function that returns branch probabilities
# Does not yet use result caching and does not yet support assigning probabilities
# to more than one state variable set
def prntr(v, pvars):
assert abs(sum(pvars)-1.0)<=0.0001,"Probs must add to 1!"
if v == aut.true:
return 1.0
elif v == aut.false:
return 0.0
if v.var in ["x_0","x_1"]:
thisSum = 0.0
# Compute probabilities
for i,p in enumerate(pvars):
# Find successor
# Assuming that x_2 always comes after x_1
thisV = v
negate = thisV.negated
if thisV.var == 'x_0':
if i & 1:
thisV = thisV.high
else:
thisV = thisV.low
negate = negate ^ thisV.negated
if thisV.var == 'x_1':
if i & 2:
thisV = thisV.high
else:
thisV = thisV.low
if negate:
thisSum += p*prntr(~thisV, pvars)
else:
thisSum += p*prntr(thisV, pvars)
return thisSum
# TODO: What is the semantics for variables outside of the current block?
return 0.5*prntr(v.high, pvars) + 0.5*prntr(v.low, pvars)
pvars = np.array([0.1, 0.2, 0.3, 0.4])
aut.declare_variables(x=(0, 3))
u= aut.add_expr('x = 0')
print(prntr(u,pvars))
u2 = aut.add_expr('x = 3') | aut.add_expr('x = 2')
print(prntr(u2,pvars))