FAULT- AND DEFECT-TOLERANT ARCHITECTURES FOR NANOCOMPUTING - Bio-Inspired and Nanoscale Integrated Computing - page 278

gate has a failure probability of 0.001. The system is usually modeled as a state
transition system with probability values attached to the transitions. Examples of
such transition systems are discrete time Markov chains (DTMCs), continuous
time Markov chains (CTMCs) and Markov decision processes (MDPs). The
specifications or properties to be verified are specified typically in probabilistic
extensions of temporal logic. A probabilistic model checker applies algorithmic
techniques [33] to analyze the state space of the input model to verify the
probabilistic properties.
The two most common temporal logics used for specifying properties of
probabilistic systems are PCTL [34, 35] and CSL [36, 37], both extensions of the
logic CTL. PCTL is used to specify properties for DTMCs and MDPs and CSL is
used for CTMCs. One common feature of the two logics is the probabilistic P
operator. For example, the formula P 1 ½} terminate states that the system will
eventually terminate with probability 1. On the other hand, the formula
P 0 : 95 ½: repair U 200 terminate asserts that the system should terminate within
200 time steps without requiring any repairs with a probability 0.95 or greater. In
addition to the P operator, CSL also provides the S that helps in specifying
steady-state behavior. For instance, S 01 ½ queue size ¼ max states that the

probability that a queue is full is strictly less than 0.01 in the long run. Further
properties can be analyzed by introducing the notion of costs (or, conversely,
rewards). If each state of the probabilistic model is assigned a real-valued cost, one
can compute properties such as the expected cost to reach specific states, the
expected accumulated cost over some time period, or, the expected cost at a
particular time instant.
Methodologies based on PMC techniques can be applied to evaluate the
reliability of nanoarchitectures. PMC-based tools like PRISM [38] and SMART
[29] can be used for such analysis. PRISM [38, 39] is an example of model checker
that supports the analysis of three types of probabilistic models: DTMCs, CTMCs
and MDPs. DTMCs can be used to model conventional digital circuits since
DTMCs are suitable for such modeling [12]. The DTMC model of computation
specifies the probability of transitions between states such that the probabilities of
performing a transition from any given state sums up to 1. Modeling of fault-
tolerant architectures can be done as templatized DTMCs with probabilistic
assumptions about the occurrence of noise at the gates and interconnects and using
Markov analysis techniques to evaluate different properties of the architectures.
In [40, 41] PMC is used to evaluate the reliability of small circuits assuming
that each gate fails independently. Circuits are specified as DTMCs, due to their
suitability for modeling digital systems [12]. The reliability of a circuit is evaluated
by computing the probability of reaching specific DTMC states, states that
represent the correct Boolean values at the circuit outputs for a certain probability
distribution at the inputs. Below, we discuss this PMC-based reliability estimation
methodology with an illustrative example.
Figure 10.9 shows the DTMC for a NAND gate with inputs A0 and B0, and
output out. The DTMC has 15 states and 22 transitions. The state variables are s,
A0, B0 and out, where s is used to represent the level in the DTMC. Formally, each

:

o 0