Information Technology Reference
In-Depth Information
representing the intervals between the two consecutive sampling points (from the
time the receiver samples the signal of a code subcell to the next one. Formally,
=
a
)
(
HLS
=(
X
∧
¬
X
∧
=
b
)
,
=
a
)
(
LHS
=(
¬
X
∧
X
∧
=
b
)
,
ρ
)
(
HLR
=(
Y
∧
int
∧
1
≤
≤
¬
Y
∧
=1)
,
ρ
)
(
LHR
=(
¬
Y
∧
int
∧
1
≤
≤
Y
∧
=1)
.
Now, we are ready to formalise the BMP in DC. What we have to do is write
down the encoding function
f
and the decoding function
g
. From the informal
description of the protocol, we can define
f
inductively as follows.
1.
f
(
)
=(
¬
X
∧
=
c
)
2. If
f
(
w
)=
D
(
X
∧
=
c
), then
=
D
HLS
(
f
(
w
0)
¬
X
∧
=
c
)
=
D
HLS
(
f
(
w
1)
X
∧
=
c
)
3. If
f
(
w
)=
D
(
¬
X
∧
=
c
), then
f
(
w
0) =
D
LHS
(
X∧
=
c
)
f
(
w
1) =
D
LHS
(
¬X∧
=
c
)
For example,
f
(1) =
LHS
(
=
c
),
f
(10) =
LHS
LHS
(
¬
X
∧
X
∧
=
c
), and
f
(101) =
LHS
LHS
HLS
(
=
c
).
Because the decoding function
g
is a partial function, we have to describe its
domain first, i.e. what kind of DC formulas on the state
Y
are detected (received)
by the receiver. According to the behaviour of the receiver, first it skips
r
cycles.
Then it begins to scan for an edge (
HLR
or
LHR
). When an edge is detected,
it skips
d
cycles and repeats this procedure until it detects that the transmission
has completed (
Y
is stable for more than
ρ
cycles). Thus, a DC formula
D
is
received by the receiver iff
D
is of the form
A
0
A
1
...
A
n
,
n
X
∧
≥
1, where
-
A
0
=(1
≥
∧
>
0)
(
int
∧
(
=
r
−
1)))
(
>ρ
))
(
<
1)),
-
and either
A
n
=(
int
∧
Y
∧
(
>ρ
))
(
<
1))
or
A
n
=(
int
∧¬
Y
∧
1either
A
j
=
LHR
(
=
d
)or
A
j
=
HLR
(
=
d
)
-
and if
n
=1then
A
n
=(
int
-
and for
j
=1
,...,n
−
(
>ρ
))
(
<
1)) and if
n>
1then
A
1
=
LHR
(
=
d
) (since at the beginning the signal is low).
∧¬
Y
∧
Now, the decoding function
g
can be written as follows. Let
D
be a formula
received by the receiver.
-
If
D
=(
≤
∧
>
0)
(
int
∧
=
r
−
1)
(
¬
Y
∧
>ρ
∧
int
)
<
1then
1
g
(
D
)=
.
-
Let
g
(
D
) be defined.
•
If
D
=
D
(
ρ
)
<
1then
Y
∧
int
∧
≥
g
(
D
HLR
(
=
d
)
(
ρ
)
<
1) =
g
(
D
)1 , and
Y
∧
int
∧
≥
g
(
D
HLR
(
=
d
)
(
ρ
)
<
1) =
g
(
D
)0 .
¬
Y
∧
int
∧
≥
Search WWH ::
Custom Search