Information Technology Reference
In-Depth Information
variables in
V
. It is easy to see that the composition of two separable transitions is
equivalent to a single separable one. An SATS is called
separable
if each transition
of the system is separable. In a separable system, the composition of transitions
along a path of the system is also equivalent to a single separable transition.
We will only concentrate on separable SATSs as any polynomial program can
easily be represented by a separable SATS (see [18]). Any SATS in the rest of
the paper is always assumed separable, unless otherwise stated.
Informally, an
invariant
of a program at a location is an assertion that is
true
under any program state reaching the location. An invariant of a program can
be seen as a mapping to map each location to an assertion which has inductive
property, that is,
initial
and
consecutive
.
Initial
means that the image of the
mapping at the initial location holds on the loop entry, i.e. the invariant of the
initial location holds on the loop entry; whereas
consecutive
means that for any
transition the invariant at the pre-location together with the transition relation
and its guard implies the invariant at the post-location. In many cases, people
only consider an invariant at the initial location and do not care about invariants
at other locations. In this case, we can assume the invariants at other locations
are all
true
and therefore
initial
and
consecutive
mean that the invariant holds
on the entry, and is preserved under every cycle back to the initial location.
Definition 4 (Invariant at a Location).
Let
P
=
V, L, T, l
0
,Θ
be an SATS.
An invariant at a location
l ∈ L
is a conjunctive polynomial formula
φ ∈ PF
(
V
)
,
such that
φ
holds on all states that can be reached at location
l
.
Definition 5 (Invariant of a Program).
An
assertion map
for an SATS
P
=
V, L, T, l
0
,Θ
is a map
η
:
L → PF
(
V
)
that associates each location of
P
with a formula of
PF
(
V
)
. An assertion map of
P
is said to be an
invariant
of
P
iff the following conditions hold:
Initial:
Θ
(
V
0
)
|
=
η
(
l
0
)
.
Consecutive:
For each transition
τ
=
l
i
,l
j
,ρ
τ
,θ
τ
,
ρ
τ
(
V, V
)
=
η
(
l
j
)(
V
)
.
η
(
l
i
)(
V
)
∧
∧
θ
τ
(
V
)
|
4
Polynomial Invariants Generation
Similarly to [24], given an SATS
S
, we predetermine an invariant as a paramet-
ric SAS (PSAS for short) at each of the underlining locations (if no invariant
is predefined for a location, it is assumed that the mapping takes
true
as value
at the location) and therefore all these predefined PSASs form a parametric
invariant of
S
by the Definitions. Subsequently, according to the initial and con-
secutive conditions of the mapping, we can obtain a set of PSASs such that the
mapping is an invariant of the program iff each element the resulted set has no
real solution. Afterwards, we apply the algorithm on root classification of PSASs
to each of them and obtain a corresponding necessary and sucient condition
on the parameters of the PSAS such that the PSAS has no real solution. Fi-
nally, applying quantifier elimination technique, we can get the instantiations of
Search WWH ::
Custom Search