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

Real Solution Isolation of Constant Semi-algebraic Systems
For a constant SAS T ( i.e., t =0)oftheform(1),if T has only a finite
number of real solutions, DISCOVERER can determine the number of dis-
tinct real solutions of T ,say n , and moreover, can find out n disjoint cubes
with rational vertices in each of which there is only one solution. In addi-
tion, the width of the cubes can be less than any given positive real. The
two functions are realized through calling

nearsolve ([ P ] , [ G 1 ] , [ G 2 ] , [ H ] , [ x 1 , ..., x s ]) and
realzeros ([ P ] , [ G 1 ] , [ G 2 ] , [ H ] , [ x 1 , ..., x s ] ,w ) ,
respectively, where w is optional and used to indicate the maximum size of
the output cubes.

3 Semi-algebraic Transition Systems and Invariants

In this section, we extend the notion of algebraic transition systems in [24] to
semi-algebraic transition systems (SATSs) to represent polynomial programs.
An Algebraic Transition System (ATS) is a special case of standard transition
system, in which the initial condition and all transitions are specified in terms
of polynomial equations; while in an SATS, each transition is equipped with
a conjunctive polynomial formula as guard, and its initial and loop conditions
possibly contain polynomial inequations and inequalities. It is easy to see that
ATS is a special case of SATS. Formally,

Definition 3. A semi-algebraic transition system is a quintuple V, L, T, 0 ,Θ ,
where V is a set of program variables, L is a set of locations, and T is a set of
transitions. Each transition τ ∈ T is a quadruple 1 , 2 ,ρ τ ,θ τ ,where 1 and 2
are the pre- and post- locations of the transition, ρ τ ∈ CPF ( V, V ) is the transition
relation, and θ τ ∈ CPF ( V ) is the guard of the transition. Only if θ τ holds, the
transition can take place. Here, we use V (variables with prime) to denote the
next-state variables. The location 0 is the initial location, and Θ ∈ CPF ( V ) is
the initial condition.

If a transition τ changes nothing, i.e. ρ τ

v∈V v = v ,wedenoteby skip ρ τ .
Meanwhile, a transition τ = l 1 ,l 2 ,ρ τ ,θ τ is abbreviated as l 1 ,l 2 ,ρ τ ,if θ τ is true .
Note that in the above definition, for simplicity, we require that each guard
should be a conjunctive polynomial formula. In fact, we can drop such a restric-
tion, as for any transition with a disjunctive guard we can split it into multiple
transitions with the same pre- and post- locations and transition relation, but
each of which takes a disjunct of the original guard as its guard.
A state is an evaluation of the variables in V and all states are denoted by
Val ( V ) . Without confusion we will use V to denote both the variable set and an
arbitrary state, and use F ( V ) to mean the (truth) value of function (formula)
F under the state V . The semantics of SATSs can be explained through state
transitions as usual.
A transition is called separable if its transition relation is a conjunctive formula
of equations which define variables in V equal to polynomial expressions over

≡