Information Technology Reference
In-Depth Information
read as `
P
holds'. We also use a variant of this notation when
P
holds for some
time
t
0:
def
=(
R
P
=
e
t
d
P
`
)
^
(
`
=
t
)
Initialization and Invariants.
Notice that when a behaviour satises a for-
mula
D
,then
D
holds for every prex [0
t
] of time. It means that initialization
can be specied by a formula that typically has the form
;
`
_
=0
(
D
0
;
true
),
`
;
where
0], while
D
0
gives initial constraints
on the states which will hold for some arbitrarily small but positive time.
Most properties are, however,
invariants
, so we must express that they hold
in any subinterval. For this purpose, the operators \somewhere" (
3
) and its dual
\everywhere" (
2
) are introduced:
3
D
= 0 holds for the starting point [0
de
=
true
;
D
;
true
and
2
D
de
=
:
:
D
.
Proof System.
The proof system for Duration Calculus is built on four kinds
of elementary laws or rules:
Math
is a lifting rule that allows any result
R
about values or integrals which
can be proven to hold for any interval using mathematical analysis (
MA
):
`8
;
)
MA
b
e
:
Time
b
e
;
R
e
b
;
R
e
b
R
(
f
1
(
b
+)
;
f
1
(
e
−
)
f
1
(
t
)
dt
;:::;
f
n
(
b
+)
;
f
n
(
e
−
)
f
n
(
t
)
dt
)
e.
f
1
;
R
f
1
;:::;
e.
f
n
;
R
f
n
)
R
(
b.
f
1
;
b.
f
n
;
Lifting is crucial for a smooth interface to other engineering disciplines where
mathematical analysis is the standard tool.
Interval laws
deal with properties of chop. This binary operator is associative
and monotone w.r.t. implication:
D
1
D
1
)
D
2
(
D
1
;
D
2
)
D
2
)
(
D
1
;
D
2
)
)
Monotonicity is very useful in proofs, because it allows us to drop unimportant
constraints within a chopped formula.
Chop distributes over disjunction, has
false
as a zero, and a point as a unit.
Chop also distributes over conjunction when the chop-points are aligned with
each other: ((
D
1
^ `
=
r
);
D
2
)
^
((
D
3
^ `
=
r
);
D
4
)
)
((
D
1
^
D
3
); (
D
2
^
D
3
)).
The converse follows immediately from monotonicity.
Duration-Interval laws
link integrals and values over a chop. The use of integrals
(durations) is really justied by the additive properties in this link.
Integral-Chop.
(
R
f
=
v
1
); (
R
f
=
v
2
)
)
R
f
=
v
1
+
v
2
.
When the state expression
f
is restricted to a state assertion
P
with non-negative
duration, the converse also holds.
Search WWH ::
Custom Search