Information Technology Reference
In-Depth Information
compute a
border polynomial
(BP) from the triangularized systems through re-
sultant computation. Because the polynomials in the first computed characteris-
tic sets are of degree
(
s
(
d
+1)
O
(
n
2
)
) by [12], the polynomials in the computed
triangular sets are of degree
O
(
s
n
O
(1)
(
d
+1)
n
O
(1)
). Thus, the complexity of com-
O
(
s
3
s
+
sn
O
(1)
(
d
+1)
sn
O
(1)
) because the complexity
of computing the resultant of two polynomials with degree
d
is at most
puting BP is at most (
s
+
m
)
O
(
d
3
).
O
(
s
O
(
s
2
+
s
2
n
O
(1)
)
(
d
+1)
O
(
s
2
n
O
(1)
)
)
.
Finally, we use a partial CAD algorithm with BP to obtain real solution clas-
sification. The complexity of this step is at most the complexity of performing
quantifier elimination on BP using CAD. Suppose the dimension of the ideal
generated by the
s
polynomial equations is
t
, then BP has at most
t
indetermi-
nates. Thus, by [3], the complexity of this step is at most
O
(2
D
2
2
t
+8
)
,whichis
double exponential with respect to
t
. In a word, the cost for this part is singly
exponential in
n
and doubly exponential in
t
.
As the biggest degree of polynomials in the generated necessary and sucient
condition from the above is at most
D
, the cost for the second part is
O
(2
D
2
2
t
+8
)
as well, which is doubly exponential in
t
, according to [3].
So, compared to directly applying quantifier elimination, our approach can
dramatically reduce the complexity, in particular when
t
is much less than
n
.
Moreover, the degree of BP is at most
D
=
O
6
Generating Invariants vs. Discovering Ranking
Functions
In [2], we showed how to apply the approach to discovering non-linear ranking
functions. Although invariants and ranking functions both have inductive prop-
erties, the former is inductive w.r.t. a small step, i.e. each of single transitions of
the given program in contrast that the latter is inductive w.r.t. a big step, that
is each of circle transition at the initial location of the program. The difference
results that as far as invariant generation is concerned, our approach can be
simply applied to single loop programs as well as nested loop programs, without
any change; but regarding the discovery of ranking functions, we have to develop
the approach in order to handle nested loop programs, although it works well
for single loop programs.
7
Conclusions and Future Work
In this paper, we reduced the polynomial invariant generation of polynomial
programs to solving semi-algebraic systems, and theoretically analyzed why our
approach is more ecient and practical than that of [17] directly applying the
technique of first-order quantifier elimination. Compared to the well-established
approaches in this field, the invariants generated with our approach are more
expressive.
How to further improve the eciency of our approach is still a big challenge
as well as our main future work, as the complexity is still single exponential
Search WWH ::
Custom Search