Information Technology Reference
In-Depth Information
Theorem 4.
1. BOUND TIMED SAFETY
(
C
timed
(
∞
,
1))
is decidable,
+
2. BOUND TIMED SAFETY
(
C
timed
(1
,
∞
))
is decidable.
Proof.
(1) The proof that BOUND TIMED SAFETY(
C
timed
(
∞
,
1)) is decidable
is an adaptation of the proof that MIN TIMED SAFETY(
C
timed
(
∞
,
1)) is solv-
able.
(2) The proof that BOUND TIMED SAFETY(
+
C
timed
(1
,
∞
)) is decidable is an
+
adaptation of the proof that MIN TIMED SAFETY(
C
timed
(1
,
∞
)) is solvable.
+
We do not know at present whether BOUND TIMED SAFETY(
C
timed
(2
,
∞
)) is
undecidable.
However,
considering
regular
timed
protection
systems
in
+
C
) makes a limited variant of the BOUND TIMED SAFETY ques-
tion decidable. A timed protection system
Π
is regular iff there exists a positive
real number
d
Π
such that for all positive real numbers
d
,if
Π
contains the timed
constraint “
since at least duration
d
”then
d
=
d
Π
.Let
timed
(
∞
,
∞
C
timed
(
∞
,
∞
)betheclass
+
of all regular timed protection systems in
C
timed
(
∞
,
∞
).
Theorem 5.
The following decision problem is decidable:
∈C
timed
(
Input:
arightr, a timed protection system Π
)
, a protection
state ∆
=(
S, O, A
)
, and a positive rational number d such that d<
2
∞
,
∞
×
d
Π
,
Output:
determine if Π is d-unsafe for r with respect to ∆.
∈C
timed
(
Proof.
Let
r
be a right,
Π
) be a timed protection system,
∆
=
(
S, O, A
) be a protection state, and
d
be a positive rational number such that
d<
2
∞
,
∞
.
If
Π
is
d
-unsafe for
r
with respect to
∆
then there exists a timed history
h
with
dynamic timed sequence (
v
0
,∆
0
,θ
0
,α
0
), (
v
1
,∆
1
,θ
1
,α
1
),
...
such that:
×
d
Π
. Without loss of generality, we may assume that
S
=
∅
and
O
=
∅
-
h
=
Π
,
-
the following conditions are satisfied for some individual
s
of type subject
and some individual
o
of type object:
•
|
if
s
is in
S
n
and
o
is in
O
n
then
r
is not in
A
n
(
s, o
),
s
is in
S
n
+1
,
o
is in
O
n
+1
,and
r
is in
A
n
+1
(
s, o
),
-
∆
0
=
∆
,
•
for some minimal non-negative integer
n
such that
v
n
+1
≤ d
. The key arguments
we need are embodied in the following lemmas.
Lemma 2.
If the sequence α
0
, ..., α
n
contains at least
1
conditional command
then the command α
n
is conditional.
Proof.
Suppose that the sequence
α
0
,
...
,
α
n
contains at least 1 conditional com-
mand. If the command
α
n
is not conditional then
n ≥
1. Moreover, there exists
atimedhistory
h
with dynamic timed sequence (
v
0
,∆
0
,θ
0
,α
0
), (
v
1
,∆
1
,θ
1
,α
1
),
...
such that:
-
h
|
=
Π
,
-
the following conditions are satisfied for some individual
s
of type subject
and some individual
o
of type object:
