Information Technology Reference
In-Depth Information
SASs [28,29], to produce some necessary and sucient conditions; and finally
utilize the technique of quantifier elimination to handle the derived conditions
and obtain invariants with the predefined form.
Suppose an SAS S has s ( > 0) polynomial equations and m inequations and
inequalities. All polynomials are in n = t +( n − t ) indeterminates (i.e., u 1 ,...,u t ,
x 1 ,...,x n−t ) and of degree at most d where t is the dimension of the ideal
generated by the s equations. According to [3,8], directly applying the technique
of quantifier elimination of real closed fields, the cost for solving S is doubly
exponential w.r.t. n . But using our approach, the cost for the first step is almost
nothing, and the second step to apply root classification and isolation costs
singly exponential w.r.t. n plus doubly exponential w.r.t. t . The cost for the last
step is also doubly exponential w.r.t. t . Therefore, as t<n , our approach is
more ecient than the approaches directly based on the techniques of quantifier
elimination and Grobner basis, such as [17,24], in particular, when t is much
less than n . Moreover, our approach is still complete in the sense that whenever
there exist invariants of the predefined form, applying our approach can indeed
synthesize them, while [6]'s 2 is incomplete. On the other hand, similarly to
[17,6], invariants generated by our approach are more expressive, while applying
the approaches based on polynomial algebra can only produce conjunction of
polynomial equations as invariants.
The rest of this paper is organized as: Section 2 provides a brief review of
the theories and tools on solving SASs; Section 3 defines some basic notions,
including semi-algebraic transition systems, polynomial programs, invariants,
inductive properties and so on; Section 4 is devoted to illustrating our approach
in detail with a running example; We provide the complexity analysis of our
approach in Section 5; In Section 6, we compare the application of this approach
to invariant generating with the one to ranking function discovering; and Section
7 concludes the paper and discusses the future work in this direction.
2
Preliminaries: Theories on Semi-algebraic Systems
In this section, we introduce the cornerstone of our technique, i.e. theories and
tools on solving SASs, mainly the theories on root classification of parametric
SASs and the tool DISCOVERER.
2.1
Basic Notions
Let K [ x 1 , ..., x n ] be the ring of polynomials in n indeterminates, X = {x 1 , ··· ,x n } ,
with coecients in the field K . Let the variables be ordered as x 1 ≺ x 2 ≺ ··· ≺ x n .
Then, the leading variable (or main variable )ofapolynomial p is the variable
with the biggest index which indeed occurs in p . If the leading variable of a poly-
nomial p is x k , p can be collected w.r.t. its leading variable as p = c m x k + ··· + c 0
2 As far as eciency is concerned, we believe that our approach could be at least as
good as [6]'s, as the complexity of the semi-definite programming adopted in [6] is
also very high.
 
Search WWH ::




Custom Search