Generating Polynomial Invariants with DISCOVERER and QEPCAD - Formal Methods and Hybrid Real-Time Systems - page 78

Example 7. In Example 5, for the invariant η 1 ,wehave

x − y 2 =0 y − = eq ( x ,y )=0 . eq ( x, y )=0 ∧ x − ∧ y − 1=0 | (9)

This is equivalent to
eq ( x, y )=0 ∧ x − x − y 2 =0 ∧ y − y − 1=0 ∧ eq ( x ,y ) = 0

(10)

has no real solution. Calling
tofind ([ x − x − y 2 ,y − y − 1 ,eq ( x, y )] , [] , [] , [ eq ( x ,y )] ,
[ x ,y ,x ] , [ y, a 1 ,a 2 ,a 3 ,a 4 ] , 0) ,
it follows that (10) has no real solution iff
a 3 y 2 +3 a 1 y 2 +2 ya 2 +3 a 1 y − a 4 + a 2 + a 1 =0 ∧ (11)

a 3 ( a 1 y 2 + ya 2 − a 4 )

≤ 0 . (12)

Further by Basic Algebraic Theorem and simplifying by QEPCAD, (11) ∧ (12)
holds for all y iff

− a 4 + a 2 + a 1 =0 ∧ 3 a 1 +2 a 2 =0 ∧ a 3 +3 a 1 =0 . (13)

Regarding the invariant η 2 ,wehave
ineq ( x, y ) > 0 ∧ x − x − y 2 =0 ∧ y − y − 1=0 | = ineq ( x ,y ) > 0 . (14)

This is equivalent to
ineq ( x, y ) > 0 ∧ x − x − y 2 =0 ∧ y − y − 1=0 ∧ ineq ( x ,y ) ≤ 0

(15)

has no real solution. Calling
tofind ([ x − x − y 2 ,y − y − 1] , [ −ineq ( x ,y )] , [ ineq ( x, y )] , [] ,
[ x ,y ] , [ x, y, b 1 ,b 2 ,b 3 ,b 4 ] , 0) ,

it follows that (15) has no real solution iff
b 4 + b 3 + b 2 +2 b 2 y + b 3 y + b 2 y 2 + b 1 x + b 1 y 2 > 0 . (16)

It is easy to see that (16) should hold for all y ≥ 0 , and thus, by applying QEP-
CAD to eliminate the quantifiers ∀y ≥ 0 over (16), we get

b 1 + b 2 ≥ 0 ∧ b 1 ≥ 0 ∧ b 2 + b 3 + b 4 > 0 ∧
( b 3 +2 b 2 ≥ 0 ∨ ( b 1 b 2 + b 2 ≥ 0 ∧ 4 b 2 b 4 +4 b 1 b 4 +4 b 1 b 3 +4 b 1 b 2 − b 3 > 0)) (17)

Generating Invariant. According to the results obtained from Steps 1, 2 and
3, we can get the final necessary and sucient condition only on the parame-
ters of each of the invariant templates. If the condition is too complicated, we
can utilize the function of PCAD of DISCOVERER or QEPCAD to prove
if or not the condition is satisfied. If yes, the tool can produce the instantia-
tions of these parameters. Thus, we can get an invariant of the predetermined
form by replacing the parameters with the instantiations, respectively.