Hardware Reference
In-Depth Information
w
ˆ
0
^
00
iff
w
ˆ
0
and
w
ˆ
00
;
w
ˆ9
P
i
iff
9
a finite M
N
such that
w
ŒP
i
7!
M
ˆ
0
,where
w
ŒP
i
7!
Mdenotes the shortest string
w
0
that interprets
all variables P
j
;i
¤
i,as
w
does, but interprets P
i
as M;
w
ˆ
P
i
P
j
iff
w
.P
i
/
w
.P
j
/;
w
ˆ
P
i
D
P
j
n
P
k
iff
w
.P
i
/
D
w
.P
j
/
n
w
.P
k
/;
w
ˆ
P
i
D
P
j
C
1
iff
w
.P
i
/
Df
k
C
1
j
k
2
w
.P
j
/
g
.
Example 5.3.
The formula
D8
p.P.p/
$:
Q.p// defines the language L./
over
2
such that if the letter
B
ˇ
ˇ
2 B
x
1
x
2
2
occurs in position j,thenj
2
P iff x
1
D
1 and j
2
Q iff x
2
D
1. The string
ˇ
ˇ
2
L./;
0110
1001
w
0
D
whereas the string
ˇ
ˇ
62
L./:
011
000
w
00
D
For a formula define the language
L
./ as the set of satisfying strings
L
./
D
f
w
ˆ
g
. Then the following result holds.
k
/
?
is regular iff there exists
a WS1S formula
with
X
1
;:::;X
k
as free variables and
Theorem 5.7 (Thatcher-Wright [132]).
L
.
f
0;1
g
L
./
D
L
.
To prove that any
L
./ is a regular language, one shows by induction on the
formula how to construct a deterministic automaton A such that
L
.A/
D
L
./,
where
L
.A/ is the language recognized by A. The atomic formulas are translated
into appropriate basic automata (see [71]). Composite formulas are handled by
well-known automata operations: negation of a form
ula co
rresp
onds to
autom
ato
n
complementation (if
D:
0
,then
L
.
:
0
/
D
L
.
0
/
D
L
.A
0
/
D
L
.A
0
/,
L
.
0
/
D
L
.A
0
/,andsoA
D
A
0
is the
automaton for ); conjunction corresponds to language intersection; existential
quantification corresponds to projection, that may introduce non-determinism and
require determinization by subset construction.
The converse statement that every regular language is representable in WS1S is
proved by encoding in WS1S the finite automaton that recognizes the given regular
language.
where A
0
is the automaton such that
Example 5.8.
[93] The nondeterministic automaton of Fig.
5.4
can be represented
by the formula in WS1S
8
t Œ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/
Search WWH ::
Custom Search