Hardware Reference
In-Depth Information
Fig. 5.4
Nondeterministic
automaton of Example
5.8
Present
Next
Input
state
state
b
k
0
k
0
b
k
0
k
2
a
k
1
k
0
a
k
2
k
0
a
k
2
k
1
_
ŒS
1
.t/
^:
S
2
.t/
^
I.t/
^
S
1
.t
C
1/
^
S
2
.t
C
1/
_
Œ
:
S
1
.t/
^
S
2
.t/
^
I.t/
^
S
1
.t
C
1/
^:
S
2
.t
C
1/
_
Œ
:
S
1
.t/
^
S
2
.t/
^
I.t/
^
S
1
.t
C
1/
^
S
2
.t
C
1//
where I.t/ means input a,
:
I.t/ means input b, S
1
.t/
^
S
2
.t/ means state k
0
,
S
1
.t/
^:
S
2
.t/ means state k
1
and
:
S
1
.t/
^
S
2
.t/ means state k
2
.
Even though the space and time requirements to translate formulas into automata
have been shown to be bounded below by a stack of exponentials whose height
is proportional to the length of the formula, an “efficient” implementation of the
decision procedures of WS1S has been presented in the tool MONA [71], which
computes a minimum deterministic automaton whose language is the set of strings
for which the formula holds. Efficient means that a variety of interesting practical
problems have been successfully handled by the program.
The WS1S formalism enables to write down easily equations that characterize
the set of (functionally) permissible behaviors at a node for different topologies, as
pointed out by Aziz et al. in [5]. We present the equations for some FSM networks
shown in Fig. 1.1. In all equations M
C
represents the specification; in a given
equation, we label the unknown FSM by a superscript
?
. According to the WS1S
syntax, the FSMs must be encoded to appear in the equations.
1-Way Cascade (a) - Fig. 1.1c
M
A
.I
1
;U/
D
.
8
O
2
/Œ
M
B
.U;O
2
/
!
M
C
.I
1
;O
2
/:
The machine M
A
is exactly the one produced by the construction due to
Kim and Newborn [69].
1-Way Cascade (b) - Fig. 1.1c
M
B
.U;O
2
/
D
.
8
I
1
/Œ
M
A
.I
1
;U/
!
M
C
.I
1
;O
2
/:
Supervisory Control - Fig. 1.1e
M
B
.I
2
;O
1
;V/
D
M
A
.V;O
1
/
!
M
C
.I
2
;O
1
/:
The restriction to Moore solutions was investigated in [4].
2-Way Cascade (a) - Fig. 1.1b
M
A
.I
1
;V;U/
.
8
O
2
/Œ
M
B
.U;V;O
2
/
D
!
M
C
.I
1
;O
2
/:
2-Way Cascade (b) - Fig. 1.1b
M
B
.U;V;O
2
/
.
8
I
1
/Œ
M
A
.I
1
;V;U/
D
!
M
C
.I
1
;O
2
/:
Rectification (a) - Fig. 1.1d
M
B
.U;V/
.
8
I
1
;O
1
/Œ
M
A
.I
1
;V;U;O
1
/
D
!
M
C
.I
1
;O
1
/:
Rectification (b) - Fig. 1.1d
M
A
.I
1
;V;U;O
1
/
D
M
B
.U;V/
!
M
C
.I
1
;O
1
/:
Search WWH ::
Custom Search