Information Technology Reference
In-Depth Information
A0
B0
Out
s=0
0
0.1
0.9
s=1, A0=0
s=1, A0=1
1
2
0.9
0.9
0.1
0.1
s=2, B0=0
s=2, B0=1
s=2, B0=0
s=2, B0=1
3
4
6
5
0.99
0.01
0.01
0.99
0.01
0.01
0.99
0.99
1.0
1.0
1.0
1.0
1.0
1.0
1.0
1.0
8
7
9
10
11
12
13
14
s=3,
Out=A0B0
s=3,
Out=1
−
A0B0
s=3,
Out=A0B0
s=3,
Out=1
−
A0B0
s=3,
Out=A0B0
s=3,
Out=1
−
A0B0
s=3,
Out=1
−
A0B0
s=3,
Out=A0B0
Each state is encoded as (s, A0, B0, out)
DTMC states = 15, DTMC transitions = 22,
MTBDD nodes = 52, terminals = 6
Figure
10.9.
DTMC of a NAND gate.
DTMC state is encoded as a quadruple
ð
s
3
g
and
A0, B0 and out are Boolean variables. The transitions in Figure 10.9 have
probability values attached to them. For instance, the probability of 0.9 for
transitioning from state 0 (encoded as (0,0,0,0)) to state 2 (encoded as (1,1,0,0))
implies that input A0 has a 0.9 probability of being stimulated, i.e., being in logic
''1'' state. Similarly, a 0.01 probability of moving from state 6 (2,1,1,0) to state 14
(3,1,1,1)
;
A0
;
B0
;
out
Þ
, where s
2f
0
;
1
;
2
;
implies that
the NAND gate can fail
independently with a 0.01
probability.
Figure 10.10 is a one step transition probability matrix of the DTMC in
Figure 10.9. Each row of the matrix represents the transition flow out of the
corresponding state. For instance, the first row of the matrix shows that there is a
probability of 0.1 for transitioning from DTMC state 0 to DTMC state 1, and a
probability of 0.9 of moving from state 0 to state 2. Since the accumulative
transition flow out of each state must be 1 in a DTMC, the rows of the matrix
must sum to 1.
Usually these probability matrices are sparse, and can hence be represented
compactly. PRISM uses multiterminal binary decision diagrams (MTBDDs) to
represent these matrices. MTBDDs were introduced in [42] as a generalization of
binary decision diagrams (BDD) [43]. Like BDDs, they are rooted directed acyclic
graphs whose non-terminal nodes are labeled with Boolean variables from an
ordered set. However, unlike BDDs, the terminal nodes are labeled with values
from a finite set M, where usually M
P, not just 0 and 1. An MTBDD with n
Boolean variables and terminals
from M can be considered as a map
n
f
: f
0
;
1
g
!
M.
Search WWH ::
Custom Search