Information Technology Reference
In-Depth Information
3.2
Binary Decision Diagrams (BDD)
Binary decision diagrams (BDD), used for representing Boolean functions, can be ex-
tended to symbolically represent states, events and transitions of automata. In contrast
to explicit representations, which might be computationally expensive in terms of time
and memory, BDDs often generate compact and operation-efficient representations.
A binary decision diagram is a directed acyclic graph (DAG) consisting of two kinds
of nodes: decision nodes and terminal nodes . Given a set of Boolean variables V ,a
BDD is a Boolean function f :2 V
which can be recursively expressed using
Shannon's decomposition [10]. Besides, a variable v 1 has a lower (higher) order than
variable v 2 if v 1 is closer (further) to the root and is denoted by v 1
→{
0 , 1
}
v 2 .Thevariable
ordering will impact the number of BDD nodes. However, finding an optimal variable
ordering of a BDD is a NP-complete problem [11]. In this paper, a simple but powerful
heuristic based on Aloul's Force algorithm [12] is used to compute a suitable static
variable ordering.
Symbolic Representation of Automata. The BDD data structure can be extended to
also represent models such as automata. The key point is to make use of characteristic
functions .
Given a finite state set U as universe, for every S ⊆ U , the characteristic function
can be defined as follows:
χ S ( α )= 1 α∈S
0 α∈S.
(1)
Set operations can be equivalently carried on corresponding characteristic functions.
For example, S 1
S 2 , ( S 1 ,S 2
U ) can be mapped equivalently to χ S 1
χ S 2 ,since
S 1
.
The elements of a finite set can be expressed as a Boolean vector. So a set with n
elements, requires a Boolean vector of length
S 2 =
{
α
U
|
α
S 1
α
S 2 }
. Just like the case of coding the
states in a set, binary encoding of the transition function δ follows the same rule but with
the difference that the transition function distinguishes between source-states and target
states. Hence, we need two Boolean vectors with different sets of Boolean variables to
express the domain of source-states and target-states respectively.
log 2 n
4
BDD-Based Partitioning Computation
The safe-state algorithm, an efficient supervisor synthesis algorithm, formally defined
in [13], is used in this paper. The algorithm creates the supervisor by first building the
candidate S 0 = P
Sp , then removing states from Q S 0 until the remaining safe states
are both non-blocking and controllable.
As Algorithm 1 shows, given a set of forbidden states Q x , the algorithm computes the
set of safe states Q S by iteratively removing the blocking states (RestrictedBackward
in line 5 ) and the uncontrollable states (UncontrollableBackward in line 6 ). Note that
after the termination of the algorithm, not all of the safe states are reachable from the
initial state. Therefore, a forward reachability search is needed to exclude the safe states
which are not reachable. The safe-state algorithm is discussed in more detail in [13].
 
Search WWH ::




Custom Search