Algebraic Invariants for Linear Hybrid Automata
Rupak Majumdar Joël Ouaknine Amaury Pouly James Worrell


Aspects of quarkonium propagation in a thermal medium as seen by string models
    Oleg Andreev
    December 30, 2023
==============================================================================




  We exhibit an algorithm to compute the strongest algebraic (or
  polynomial) invariants that hold at each location of a given
  unguarded linear hybrid automaton (i.e., a hybrid automaton
  having only unguarded transitions, all
  of whose assignments are given by affine expressions, and all of
  whose continuous dynamics are given by linear differential
  equations).  Our main tool is a control-theoretic result of
  independent interest: given such a linear hybrid automaton, we show
  how to discretise the continuous dynamics in such a way that the
  resulting automaton has precisely the same algebraic invariants.




§ INTRODUCTION


Invariants are one of the most fundamental and useful
notions in the quantitative sciences, appearing in a wide range of
contexts, from gauge theory, dynamical systems, and control theory
in physics, mathematics, and engineering to program verification,
static analysis, abstract interpretation, and programming language
semantics (among others) in computer science. In spite of decades of
scientific work and progress, automated invariant synthesis remains
a topic of active research, particularly in the fields of computer-aided
verification and program analysis, and plays a central role in methods
and tools seeking to establish correctness properties of computer
systems; see, e.g., <cit.>, and particularly Sec. 8 therein.

In this paper, we consider the task of computing strongest
  algebraic inductive invariants for unguarded linear
  hybrid automata. Hybrid automata are a formalism for describing
systems or processes that combine discrete and continuous evolutions
over their state variables. A hybrid automaton is therefore equipped
with a finite set of real-valued variables, as well as a finite set of
control location (or modes). In each location, the variables evolve according to
some differential dynamics. Transitions between control locations may
effect discrete updates (also known as resets) to these
variables. A hybrid automaton is unguarded if the
transitions do not have any guards, or preconditions, in order to be
fired, and it is linear if the discrete updates on the
variables consist entirely of affine transformations, and the
continuous dynamics within each control location are defined by
linear differential equations.

An invariant assigns to each control location a fixed set of real
values in such a way that through any trajectory of the hybrid
automaton, the values of the variables always remain within the
invariant. The invariant is inductive provided, informally
speaking, that it is itself preserved by the (continuous and discrete)
dynamics of the hybrid automaton. Finally, an invariant is
algebraic (or polynomial) if it consists in a collection of varieties (or
algebraic sets), i.e., positive Boolean combination of polynomial
equalities. As it happens, the strongest polynomial invariant (i.e.,
smallest variety with respect to set inclusion) is obtained by taking
the Zariski closure of the set of reachable configurations in each
control location; such an invariant is always inductive provided that
the dynamics are Zariski continuous.

There is a rich history of research into the computation of algebraic
invariants for various classes of (discrete) computer programs; we
refer the reader to our recent paper <cit.> and references
therein. There has also been a substantial amount of work on algebraic
invariant generation for hybrid systems, albeit in more recent years.
One of the earliest pieces of work on this topic is by
Rodrígez-Carbonell and Tiwari <cit.>, who consider linear
dynamical systems (i.e., linear hybrid automata with a single discrete
location and no transition) and show how to compute strongest
algebraic invariants for these. They then leverage
abstract-interpretation techniques to derive algebraic invariants for
linear hybrid automata, however without guarantees on the strength of
the invariants. In <cit.>, Sankaranarayanan et al. compute
algebraic invariants for polynomial hybrid systems directly using
constraint solving over template invariants (without however
guaranteeing to obtain the strongest invariant). In subsequent work,
Sankaranarayanan shows how to compute strongest algebraic invariants
up to a fixed degree <cit.> for the same class of
automata. Using different analytic techniques, Ghorbal and Platzer
show in <cit.> how to compute algebraic invariants and
differential invariants for polynomial hybrid automata; more
precisely, they show that deciding whether a collection of algebraic
sets forms an algebraic invariant is decidable; they do not however
provide a procedure to guarantee that a given invariant is the
strongest possible.

Main results. 
Our contributions in the present paper are threefold. First, for the
class of unguarded linear hybrid automata, building on our
recently developed invariant-generation techniques for affine
programs <cit.>, we show how to compute strongest algebraic
invariants. Our main technical tools come from linear algebra, algebraic
geometry, and Diophantine geometry.
Second, we show how one can discretise an unguarded
linear hybrid automaton in such a way that the discretised version has
precisely the same algebraic invariants as the original one; we are
not aware of any such result in the extant control-theoretic and
cyber-physical systems literature. And
third, we show that as soon as equality guards are allowed, even for
the restricted class of linear switching systems, there cannot
exist an algorithm for computing strongest algebraic invariants,
thereby establishing clearly a hard theoretical limit on how far the
work presented here can be extended.

We now provide a sightly more detailed overview of our approach and results.
In Section <ref> we consider a simple class
of hybrid systems, with
purely continuous dynamics, called switching systems.  A switching
system can transition arbitrarily between modes, but the variables are
not reset when changing mode.  It is natural to think of mode switches
as being determined by an external controller which provides inputs to
the system.  We show that for a switching system, the Zariski closure
of the set of reachable configurations is an irreducible variety.  We
exploit this feature to give a conceptually simple algorithm to
compute the strongest algebraic invariant of a given switching system.

In the rest of the paper we develop this basic result in two
directions.  In Sections <ref>
and <ref> we generalise the above analysis to
accommodate discrete transitions that may reset variables (e.g., the
bouncing ball in Example <ref>, in which the
velocity is reset on hitting a boundary, or the RC circuit in
Example <ref>, in which the electrical currents and
voltages change abruptly when a switch is turned on or off).  In this
setting the dynamics is not necessarily continuous.  In fact, our
approach here is to eliminate the continuous dynamics altogether by
introducing a discretisation construction on hybrid automata that
preserves all algebraic invariants.  More formally, given a hybrid
automaton we show how to construct a finite (discrete-time) affine
program that has the same same set of variables and the same algebraic
invariants as the original hybrid automaton.  We can then rely on a
result in <cit.> to compute strongest algebraic invariants.

In another direction, in Section <ref> we consider the
problem of computing the strongest algebraic invariant for switching
systems that are augmented with the ability to test variables for zero
on transitions.  Here again the dynamics are exclusively continuous.
We show that it is undecidable in general to compute a strongest
algebraic invariant for such systems.  Roughly speaking, we prove this
result by defining a simulation of an arbitrary Minsky machine
𝒞 by a hybrid automaton 𝒜, such that we can
effectively determine whether the set of reachable configurations of
𝒞 is infinite from the strongest algebraic invariant of
𝒜.



§ EXAMPLES




 §.§ Bouncing ball


Consider a ball that bounces on horizontal slabs, as illustrated in Figure <ref>.
The ball is moving at constant horizontal speed c and is subject to gravity along the vertical
axis. We assume that there is no friction and that collisions are perfectly elastic. We do
not want to make any assumption on the location of the slabs, to obtain the most general system.
Thus from the point of the view of system, the positions of the slabs are `nondeterministic'
and the slabs can `appear' at any moment.



We fix an arbitrary coordinate system in which the ball starts at position (0,h) with initial velocities
(c,0). The system is modelled using a single discrete location. There are three constants c
(the horizontal speed), h (the initial height), and g (approximately 9.8 ms^-2).
Technically speaking we could also include m (the mass of the ball),
but it will not feature in the final set of invariants that we derive nor in our differential equations.
There are five variables: t, x, y, v_x, and v_y, where t is the time
variable. The differential equations are simply Newton's laws of motion. There is a single reset
with no guards modelling the action of the ball bouncing on each of
the slabs (notably ensuring that the vertical velocity is instantly inverted).
We obtain the hybrid system described in Figure <ref>.

Now we come to the invariants. The most obvious is that the horizontal speed is constant:
v_x = c, which in turn entails that x = tc.
Next, consider an inertial coordinate system moving horizontally to the right at speed c.
In that system energy must be conserved. Initially there is no kinetic energy,
and all the potential energy amounts to mgh (where m is the mass of the ball).
At any subsequent time t, the sum of the kinetic and potential energy must therefore sum to
that value,  12mv_y^2 + mgy = mgh, so v_y^2 + 2g(y-h) = 0.
These must be the only invariants: the ambient space is 5-dimensional (given that our variables are
t, x, y, v_x, and v_y), and the corresponding variety (with 3 equations) is two dimensional.
But the system has indeed exactly two degrees of freedom, since t and v_y can be set to arbitrary values
(provided |v_y| ≤ gt), and once t and v_y are fixed, every other variable is fixed.
In summary, the strongest algebraic invariant is the conjunction of
the following three equations:

    v_x=c,
            
        x=tc,
            
        v_y^2 + 2g(y-h) = 0.






 §.§ RC circuit




Consider an RC circuit with a switch, as illustrated in
Figure <ref>. When the switch is on, the capacitor is
connected to a battery and charges. When the switch is off, the
capacitor discharges through the resistor. The battery has constant
voltage V, the resistor has resistance R and the capacitor has
capacity C. There are 5 variables: the current I in the wire
between the battery and the switch, the voltages V_R and V_C
across the resistor and capacitor respectively, the current I_R
flowing through the resistor, and finally the charge Q held by the
capacitor.  All derivatives are with respect to time, though this time
we choose not to include an explicit variable for the passage of
time. There are two discrete locations, open and closed, 
corresponding to the two possible positions of the switch. We assume the
switch starts in the open position. When switching from open to
closed, all variables but Q and V_C experience a reset.  We obtain
the hybrid system described in Figure <ref>.

In this example, there is one set of invariants per location. In both locations, we clearly have
the invariants associated with the passive components: Q=CV_C and V_R=RI_R.
In the open location, we further have the invariants I=0 and V_R=-V_C. On the hand,
in the closed location, we have I=I_R and V=V_R+V_C.
These must be the only invariants: once Q is fixed, all variables are uniquely determined.
In summary, the invariants are


    
        open:     Q = CV_C,     V_R = RI_R,     I = 0,     V_R = -V_C,

        closed:     Q = CV_C,     V_R = RI_R,     I = I_R,     V_R = V-V_C.
    























































§ MATHEMATICAL BACKGROUND


Let  be a field.  Given a set X⊆^n, we denote by
𝐈(X) the ideal of polynomials in [x_1,…,x_n] that
vanish on X. Given an ideal I⊆[x_1,…,x_n], we
denote by V(I) ⊆^n the set of common zeroes of the
polynomials in I.  A set X ⊆^n is said to be an
affine variety (also called an algebraic set) if
X=V(I) for some ideal I⊆[x_1,…,x_n].  By the
Hilbert Basis Theorem, every affine variety can be described as the
set of common zeroes of finitely many polynomials.  We identify
_n(), the set of n× n invertible matrices with entries
in , with the variety
{(A,y) ∈^n^2+1 : (A) · y = 1}.

Given an affine variety X⊆^n, the Zariski topology
on X has as closed sets the subvarieties of X, i.e., those sets
A⊆ X that are themselves affine varieties in ^n.  Given
an arbitrary set S⊆ X, we write S for its closure in
the Zariski topology on X.

A set S ⊆ X is irreducible if
for all closed subsets A_1,A_2⊆ X such that
S⊆ A_1 ∪ A_2 we have either S⊆ A_1 or
S⊆ A_2.  It is well known that the Zariski topology on a
variety is Noetherian.  In particular, any closed subset A of X
can be written as a finite union of irreducible components,
where an irreducible component of A is a maximal irreducible closed
subset of A.

The class of constructible subsets of a variety X is obtained
by taking all Boolean combinations (including complementation) of
Zariski closed subsets.  Suppose that the underlying field  is
algebraically closed.  Since the first-order theory of algebraically
closed fields admits quantifier elimination, the constructible subsets
of X are exactly the subsets of X that are first-order definable
over .

A function f:^m→^n is said to be a polynomial
  map if there exist polynomials
p_1,…,p_n ∈[x_1,…,x_m] such that
f(a) = (p_1(a),…,p_n(a))
for all a∈^m.  



Recall that
polynomial maps are Zariski-continuous and thus
f(X)⊆f(X) for a polynomial map f.  In particular
matrix multiplication is a Zariski-continuous map 
^n^2×^n^2→^n^2.

Given a complex variety V⊆^n, the intersection
V∩^n, which is a real variety, can be computed
effectively. Indeed if V is represented by the ideal
I⊆[x_1,…,x_n], then V∩^n is represented by
the ideal generated by p_,p_i:p∈ I where p_ and
p_i respectively denote the real and imaginary parts of the
polynomial p.  Given S ⊆^n, write []S for its
real Zariski closure and S for its complex Zariski closure
(i.e., we treat the complex Zariski closure of S ⊆^n as
the default).  It is straightforward to verify that
[]S = S∩^n.













































§ ALGEBRAIC INVARIANTS FOR HYBRID AUTOMATA


We are concerned with computing strongest algebraic invariants for
the subclass of hybrid automata that has no guards, linear discrete
updates, and linear continuous dynamics.  Each location of such an
automaton specifies a linear differential equation (x'=Ax), and each
transition between states (nondeterministic choices are allowed)
specifies a linear transformation (x↦ Bx).  Such a hybrid
automaton can be pictured as follows:



[
        mynode/.style=fill=blue!30!white,circle,draw,
        mynode final/.style=mynode,double, double distance=0.5mm,
        myarrow/.style=->,thick,
    ]
    [mynode] at (0,0) (n1) x'=A_ix;
    [mynode] at (4,0) (n2) x'=A_jx;
    (n1) ++(20:-2) edge[myarrow] (n1);
    (n1) ++(0:-2) edge[myarrow] (n1);
    (n1) ++(-20:-2) edge[myarrow] (n1);
    (n2) edge[myarrow] ++(-20:2);
    (n2) edge[myarrow] ++(0:2);
    (n2) edge[myarrow] ++(20:2);
    [myarrow] (n1) edge[bend left=15] node[midway,above] B^ij_1 (n2);
    (n1) edge[opacity=0] node[opacity=1,midway] … (n2);
    [myarrow] (n1) edge[bend right=15] node[midway,below] B^ij_k (n2);



Formally, such an automaton 𝒜 in dimension d is a tuple
(Q,A,E,T), where Q is a finite set of locations,
A = {A_q:q ∈ Q} is a family of real d× d matrices,
E⊆ Q×^d× d× Q is a set of transitions
labelled by real d× d matrices, and { T_q : q ∈ Q} is a
family of algebraic subsets of ^d.  Matrix A_q∈^d× d
describes the continuous dynamics at location q∈ Q and
T_q ⊆^d is the set of initial states in location q.  We
assume that the entries of all matrices are algebraic numbers and that
the polynomials defining T_q have algebraic coefficients.

We will consider the subclasses of automata with the following
restrictions:


  * affine programs: A_q=0 for all q∈ Q, and E is finite,

  * constructible affine programs: A_q=0 for all q∈, and E is constructible,

  * switching systems: E={(p,I_n,q):p,q∈ Q}, i.e., every pair of locations is connected by an edge that does not update the variables,

  * linear hybrid automata: E is finite.

In affine programs, variables are only updated on discrete edges: there
is no continuous evolution within locations.  At the other end of the
spectrum, in switching systems variables only evolve continuously, and
there are no discrete updates.  The full class of linear hybrid
automata accommodate both discrete an continuous updates to the
variables.


The collecting semantics of 𝒜 assigns to each
location q∈ Q the set S_q⊆^d of states that can occur
in location q during a run of the automaton, starting from a
configuration (q, a) for some a ∈
T_q. Formally, this is the smallest family (with respect to set inclusion)
such that

    [                 S_q                   ⊇                 T_q       for all q∈ Q,;                 S_q                   ⊇                BS_p for all (p,B,q)∈ E,;                 S_q                   ⊇           e^A_qtS_q      for all t∈_⩾0.;                     ]

Equivalently, let the operator Φ_𝒜:𝒫(^d)^Q→𝒫(^d)^Q be defined by

    Φ_𝒜(S)_q=T_q∪⋃_t⩾0e^A_qtS_q∪⋃_(p,B,q)∈ EBS_p.

Then S is the least fixed-point of Φ_𝒜 with respect 
to set inclusion.
Such a least fixed-point exists because
Φ_𝒜 is monotone.

  In general we say that a family of set { S'_q }_q ∈ Q, with
  S'_q ⊆^d is an inductive invariant if
  Φ_𝒜(S') ⊆ S', i.e., the family is
  pre-fixed-point of Φ_𝒜.  If each set S'_q is
  algebraic then we moreover say that { S'_q }_q ∈ Q is an
  inductive algebraic invariant.

Given P∈[x_1,…,x_d], we say that the relation P=0 holds
at location q if P vanishes on S_q. We are interested in
computing at each location q∈ a finite set of polynomials that
generates the ideal I_q:=𝐈(S_q)⊆[x_1,…,x_d]
of all polynomial relations that hold at location q.  The real
variety V_q:=V(I_q)=[]S_q corresponding to I_q is the
Zariski closure of S_q viewed a subset of the affine space ^d.

Note that the collection V(𝒜):=V_q:q∈ Q defines an
inductive algebraic invariant.  Inductiveness amounts to the following
two claims:


  * for every edge (p,B,q)∈ E, we have BV_p⊆ V_q,

  * for every q∈ Q and t∈, we have e^A_qtV_q⊆ V_q.

The first point follows from the fact that x↦ Bx is Zariski-continuous; the second point
likewise follows from the fact that for every t∈ the map  x↦ e^A_qtx
is Zariski-continuous. 




The discussion above shows that V(𝒜), the Zariski closure
of the collecting semantics, is the least inductive invariant of
𝒜.  Previously we have shown how to compute the Zariski
closure of the collecting semantics of an affine program:


  There is an algorithm that given a
  constructible affine program 𝒜 computes
  V(𝒜)=V_q:q∈—the real Zariski closure of its
  collecting semantics.

Note that this theorem also works for (finite) affine programs since
those are a particular case of constructible affine programs. 




The main result of the current paper extends the above result by
accommodating the continuous dynamics of hybrid automata:


There is an algorithm that given a linear hybrid automaton 𝒜
computes V_q:q∈ Q—the real Zariski closure of
its collecting semantics.




§ LINEAR CONTINUOUS DYNAMICS AND SWITCHING SYSTEMS


The first step towards computing Zariski closure in the general case
is to be able to handle the case of one differential equation.  Write
 for the field of algebraic numbers.  Let A∈^d×
  d and x_0∈^d× d, then the solution to x(0)=x_0,
x'(t)=Ax(t) is given by x(t)=e^Atx_0. We are interested in
computing the Zariski closure of the orbit
x(t):t∈. Since the map ϕ:M↦ Mx_0 is
Zariski-continuous, we have that

    x(t):t∈
        =e^Atx_0:t∈
        =ϕ(e^At:t∈)
        =ϕ(e^At:t∈)

and thus it suffices to compute e^At:t∈.
Furthermore, let 𝒪_A:=e^At:t∈, which is a commutative group. Then
e^At:t∈=𝒪_A: the left-to-right inclusion is clear.
The converse inclusion comes from the fact that an exponential polynomial (in one variable), being an analytic function,
vanishes over  if and only if it vanishes over . Thus it suffices
to compute 𝒪_A.

The following lemma gives a description of the ideal of the variety 𝒪_A
when A is diagonal.


    Let A=(λ_1,…,λ_d)∈^d× d be a diagonal matrix,
    then 
    𝒪_A=(z_1,…,z_d):∀ p∈ I,p(z_1,…,z_d)=0  ,

    where I=⟨ z^a-z^b:a-b∈ L⟩ and L=n∈^d:n_1λ_1+⋯+n_dλ_d=0.
    Furthermore, one can compute a basis for L considered as an abelian group under addition.


Clearly e^At=(e^λ_1t,…,e^λ_dt). Since the set of diagonal matrices is closed,
then the closure is of the form 
    𝒪_A=(z_1,…,z_n):p_1(z)=⋯=p_k(z)=0

for some polynomials p_1,…,p_k. Thus, the ideal I of the closure is generated by all polynomials
p such that p(e^λ_1t,…,e^λ_dt)=0 for all t∈. Let J be the ideal of
all polynomials x^a-x^b with a,b∈^d such that λ· a=λ· b.
Clearly J⊆ I since if λ· a=λ· b, then
(e^λ_1 t)^a_1⋯(e^λ_d t)^a_d-(e^λ_1 t)^b_1⋯(e^λ_d t)^b_d=e^(λ· a)t-e^(λ· b)t=0 for all t∈.
Conversely, assume by contradiction that p∈ I∖ J and write
p=∑_i=1^rb_im_i
for some b_i∈ and monomials m_1,…,m_r. Further choose p so that r is minimal.
For each monomial m_i(x)=x_1^a_1⋯ x_d^a_d, let μ_i:=λ· a. Then we must have
μ_i≠μ_j for i≠ j because otherwise m_i-m_j∈ J and p-b_i(m_i-m_j)∈ I∖ J
would have fewer terms than p. Since the maps t↦ e^μ_1 t,…,t↦ e^μ_d t
are linearly independent, it follows that b_1=⋯=b_r=0 which is contradiction.
Thus we must have have I=J. It is immediate to see that J is generated by all polynomials x^a-x^b
such that λ·(a-b)=0, thus it suffices to compute L=a∈^d:λ· a=0,
the set of additive relations of λ. Notice that L is an additive subgroup of ^d and
as such must be finitely generated. An upper bound on the size of the elements of a basis of L
can be found in <cit.> and therefore we can compute a basis for L and thus J, I and 𝒪_A.


A corollary of this result is that we can compute 𝒪_A by separating
the diagonal and nilpotent parts of A. The fact that this closure is computable is
not new, a similar result exists in the litterature, although without proof <cit.>.


There is an algorithm that given A∈^d× d, computes e^At:t∈.


We can write A=P(D+N)P^-1 where P is invertible, D is diagonal, N
is nilpotent, and D and N commute. Notice that 𝒪_D only consists of diagonal matrices
and 𝒪_N of unipotent matrices. Since 𝒪_A is a commutative group,
and D and N commute, we have that 𝒪_A=P(𝒪_D·𝒪_N)P^-1,
and thus 𝒪_A=P𝒪_D·𝒪_NP^-1. All the
operations in this equation are effective thus it suffices to compute 𝒪_D as
explained above, and 𝒪_N. But since N is nilpotent, q_n(t):=e^Nt is really a polynomial
in Nt and thus in t. It follows that 𝒪_N=q_n()=q_n()=q_n()
which we know how to compute.


Next we consider the class of switching systems, that is,
hybrid systems in which every pair of locations is connected by an
edge and in which variables are no updated on discrete edges.  It is
known that reachability is undecidable even for this restricted
class <cit.> of systems.  However, as we show below, building
on Proposition <ref>, one can compute
computing strongest algebraic invariants in this setting.

ruled

A_1,…,A_k∈^d× d
H:={I_d}    
G_1:={ e^A_1t:t≥ 0} ; … ; G_k:={ e^A_1t:t≥ 0}  
H_old=H 
    H_old:=H 
    i ∈{1,…,k}
        H:=H·  G_i   
    


H
Semigroup-Closure(A_1,…,A_k)




  Algorithm <ref> (shown below) terminates and outputs the
  Zariski closure of the sub-semigroup of GL_d()
  generated by { e^A_1t ,…, e^A_kt: t≥ 0}.

 
  First note that the effectiveness of Line <ref>
  relies on Proposition <ref>.

  Now we argue that H in the algorithm is always an irreducible
  variety.  For this it suffices to show that if
  X ⊆GL_d() is an irreducible variety then so
  is Y:=X ·{e^At : t≥ 0} for any matrix
  A ∈^d× d. First observe that if X and Z are
  irreducible sets then so is X· Z, thus is it enough to
  show that G=S is irreducible, where S={e^At : t≥ 0}.
  But S is a semigroup, thus G is a group. This makes G a linear
  algebraic group, which is therefore irreducible if and only if it
  is (Zariski-)connected. But G being the closure of S means it is
  enough to show that S is Zariski-connected, and hence enough to show
  that it is Euclidean-connected. The latter is trivial since every element
  of S is path-connected to I_d.

Now a strictly increasing chain H_1⊆ H_2⊆⋯ of
irreducible sub-varieties of GL_d() has length at most
the dimension of GL_d(), which is d^2.  Thus
Algorithm <ref> terminates after at most d^2 iterations
of the outer loop.  It is clear that the terminating value of the
algorithm is the Zariski closure of the sub-semigroup of
GL_d() generated by
{ e^A_1t ,…, e^A_kt: t≥ 0}.


Now consider a switching system 𝒜=(Q,A,E,T).  Let G be
the Zariski closure of the semigroup generated by the matrices
e^A_qt, for q∈ Q and t≥ 0, which can be computed by
Proposition <ref>.  Then V(𝒜)={V_q:q∈
Q}, the real Zariski closure of the collecting semantics of
𝒜, is such that V_q = G· X∩GL_d(ℝ) for every q∈ Q, where X=⋃_q∈
  Q T_q.  But then V(𝒜) is computable from G and T.


  Given a switching system 𝒜, one can compute
  V(𝒜).




§ REDUCING CONTINUOUS DYNAMICS TO CONSTRUCTIBLE DISCRETE DYNAMICS



Let 𝒜 be an automaton, then V(𝒜) is the least fixpoint
of the map X↦Φ_𝒜(X).


Let S denotes the collecting semantics of 𝒜, then

    V(𝒜)
           =S      by definition of V(𝒜)
       =Φ_𝒜(S)      by definition of S
       =Φ_𝒜(S)      by Zariski-continuity of Φ_𝒜
       =Φ_𝒜(V(𝒜))

thus V(𝒜) is indeed a fixed-point.
Conversely, let X be such that X=Φ_𝒜(X). Then X is closed and clearly
Φ_𝒜(X)⊆Φ_𝒜(X)=X so it is a pre-fixpoint of Φ_𝒜.
By virtue of S being the least (pre-)fixpoint of Φ_𝒜 we must have S⊆ X.
But then S⊆ X  V(𝒜)⊆ X.



  Given a linear hybrid automaton 𝒜, one can compute a
  constructible affine program 𝒜' that has the same
  algebraic invariants,  V(𝒜)=V(𝒜').


The idea is to replace each continuous dynamics x'=A_qx by a closed (and thus constructible)
set of discrete transitions: e^A_qt:t∈, which we know how to compute thanks
to Proposition <ref>
. Graphically:


[
        mynode/.style=fill=blue!30!white,circle,draw,
        mynode final/.style=mynode,double, double distance=0.5mm,
        myarrow/.style=->,thick,
        scale=0.7
    ]
    [mynode] at (0,0) (n1) x'=Ax;
    (n1) ++(20:-2) edge[myarrow] (n1);
    (n1) ++(0:-2) edge[myarrow] (n1);
    (n1) ++(-20:-2) edge[myarrow] (n1);
    (n1) edge[myarrow] ++(-20:2);
    (n1) edge[myarrow] ++(0:2);
    (n1) edge[myarrow] ++(20:2);
    (3,0) edge[very thick,decorate, decoration=snake,amplitude=0.5ex,post=lineto,post length=1ex,-Straight Barb[width=2ex]] ++(1,0);
    [shift=(7,0)]
    [mynode] at (0,0) (n1) x'=0;
    (n1) ++(20:-2) edge[myarrow] (n1);
    (n1) ++(0:-2) edge[myarrow] (n1);
    (n1) ++(-20:-2) edge[myarrow] (n1);
    (n1) edge[myarrow] ++(-20:2);
    (n1) edge[myarrow] ++(0:2);
    (n1) edge[myarrow] ++(20:2);
    (n1) edge[myarrow,loop,in=80,out=100,min distance=5ex] node[midway,above=-1ex] e^At:t∈ (n1);
    



Formally, let 𝒜=(Q,A,E,T) be a linear hybrid automaton. Define the constructible
affine program 𝒜'=(Q,A',E',T) where A'_q=0 for all q∈ and

    E'=E∪(q,X,q):q∈,X∈𝒪_A_q

where 𝒪_A:=e^At:t∈. Note that it is constructible because 𝒪_A_q
is closed (and thus constructible). We will now relate Φ_𝒜 and Φ_𝒜':
let X∈𝒫(^d)^Q and observe that

    Φ_𝒜(X)_q
           =T_q∪(𝒪_A_q· X_q)∪⋃_(p,B,q)∈ EBX_q
       ⊆ T_q∪(𝒪_A_q· X_q)∪⋃_(p,B,q)∈ EBX_q
       =Φ_𝒜'(X)_q.

Let S^𝒜 (resp. S^𝒜') denote the collecting semantics of 𝒜 (resp. 𝒜'),
that is S^𝒜 is the least fixpoint of Φ_𝒜.
It follows that

    Φ_𝒜(S^𝒜')⊆Φ_𝒜'(S^𝒜')=S^𝒜',

 S^𝒜' is a pre-fixpoint of Φ_𝒜 and thus it must be the case that
S^𝒜⊆ S^𝒜'. It immediately follows that V(𝒜)⊆ V(𝒜').
Conversely, we also have that

    Φ_𝒜(S)_q   =T_q∪(𝒪_A_q· S_q)∪⋃_(p,B,q)∈ EBS_q
       =T_q∪𝒪_A_q· S_q∪⋃_(p,B,q)∈ EBS_q
       =T_q∪(𝒪_A_q· S_q)∪⋃_(p,B,q)∈ EBS_q
       =Φ_𝒜'(S)_q

and similarly for 𝒜'.
It follows that

    V(𝒜)_q
        =Φ_𝒜(S^𝒜)_q
        =Φ_𝒜'(S^𝒜)_q
        =Φ_𝒜'(S^𝒜)_q=Φ_𝒜'(V(𝒜))_q.

Thus V(𝒜) is a fixpoint of X↦Φ_𝒜'(X). But V(𝒜')
is the least fixpoint of this map by Lemma <ref> and thus V(𝒜')⊆ V(𝒜).




§ REDUCING CONTINUOUS DYNAMICS TO FINITE DISCRETE DYNAMICS


In the previous section, we saw that given a linear hybrid automaton
one can compute a constructible affine program with the same set of
algebraic invariants.  In this section we show how to compute a
finite affine program with the same set of algebraic
invariants.  The idea is to replace the continuous evolution of the
variables in each location of a hybrid automaton with a finite set of
discrete transitions.  Graphically this corresponds to rewriting the
automaton as follows:


[
        mynode/.style=fill=blue!30!white,circle,draw,
        mynode final/.style=mynode,double, double distance=0.5mm,
        myarrow/.style=->,thick,
        scale=0.7
    ]
    [mynode] at (0,0) (n1) x'=Ax;
    (n1) ++(20:-2) edge[myarrow] (n1);
    (n1) ++(0:-2) edge[myarrow] (n1);
    (n1) ++(-20:-2) edge[myarrow] (n1);
    (n1) edge[myarrow] ++(-20:2);
    (n1) edge[myarrow] ++(0:2);
    (n1) edge[myarrow] ++(20:2);
    (3,0) edge[very thick,decorate, decoration=snake,amplitude=0.5ex,post=lineto,post length=1ex,-Straight Barb[width=2ex]] ++(1,0);
    [shift=(7,0)]
    [mynode] at (0,0) (n1) x'=0;
    (n1) ++(20:-2) edge[myarrow] (n1);
    (n1) ++(0:-2) edge[myarrow] (n1);
    (n1) ++(-20:-2) edge[myarrow] (n1);
    (n1) edge[myarrow] ++(-20:2);
    (n1) edge[myarrow] ++(0:2);
    (n1) edge[myarrow] ++(20:2);
    (n1) edge[myarrow,loop,in=120,out=140,min distance=7ex] node[midway,above] B_1 (n1);
    (n1) edge[myarrow,loop,in=80,out=100,min distance=5ex] node[midway,above] … (n1);
    (n1) edge[myarrow,loop,in=40,out=60,min distance=7ex] node[midway,above] B_k (n1);
    




Mathematically, the task is as follows: Given
  A∈^d× d, find B_1,…,B_k∈^d× d
  such that e^At:t∈=B_1,…,B_k.
There is a conceptually simple approach to this problem: namely for
every matrix A∈𝔸^d× d and rational number τ
we have e^At:t∈=e^Aτ (see
Section <ref>).  But this does not fulfil our
desiderata, since it is not possible in general to find τ∈
such that e^Aτ has exclusively algebraic entries.  Nevertheless
given A∈𝔸^d× d it is possible to find
B∈𝔸^d× d such that
e^At:t∈=B.  The idea is to construct
B such that there is a correspondence between the set of additive
relations satisfied by the eigenvalues of A and the multiplicative
relations satisfied by the eigenvalues of B.


Let a_1,…,a_d∈ℂ be algebraic numbers.  Then we can
compute rational numbers  λ_1,…,λ_d
such that a_1n_1+⋯+a_dn_d=0 iff λ_1^n_1⋯λ_d^n_d=1 for all n_1,…,n_d ∈ℤ.


  Let s be the dimension of the ℚ-vector space spanned by
  a_1,…,a_d.  By computing a basis over ℚ for the number
  field ℚ(a_1,…,a_d) and the respective rational coordinates 
of a_1,…,a_d with respect to this basis, we obtain an s× d integer matrix
A such that for every integer vector
x=(n_1,…,n_d) ∈ℤ^d we have n_1a_1+
⋯ +n_da_d = 0 iff Ax=0.  

Now write A=PBQ, where
B is an s× d matrix in Smith normal form and P,Q are
unimodular square matrices.  Since B has rank s it has the form
B=[ D 0 ] for D an s× s diagonal
matrix of full rank.

We define positive integers μ_1,…,μ_d as follows.
Choose μ_1,…,μ_s to be the first s prime numbers 
and let
μ_s+1=…=μ_d=1.  Write Q = (q_ij) and define
λ_i = μ_1^q_1i⋯μ_d^q_di for i∈{1,…,d}.  

Then for all n_1,…,n_d ∈ℤ we have

    λ_1^n_1⋯λ_d^n_d =1   ⇔   μ_1^(Qx)_1⋯μ_d^(Qx)_d = 1
       ⇔    (Qx)_1=0,…,(Qx)_s=0 
       ⇔    BQx = 0   (since B=[ D 0 ])
       ⇔    PBQx = 0  (since P is invertible)
       ⇔    Ax = 0
       ⇔    a_1n_1+⋯+a_dn_d=0   .




  Let D be a d× d diagonal matrix with algebraic entries.
  Then there exists a diagonal matrix D', of the same dimension and
  with rational entries, such that e^D = D'.


Write D=diag(a_1,…,a_d) and let rational numbers
λ_1,…,λ_d be chosen as in Proposition <ref>, i.e.,
such that a_1n_1+⋯+a_dn_d=0 iff λ_1^n_1⋯λ_d^n_d=1 for all n_1,…,n_d ∈ℤ.  
Define D'=diag(λ_1,…,λ_d).
By Lemma <ref>, the ideal of the variety e^D
is generated by z^n-z^m such that (n_1-m_1)a_1+⋯+(n_d-m_d)a_d=0.
On the other hand, it follows from <cit.> that
the ideal of the variety D' is generated
by z^n-z^m such that λ_1^n_1-m_1⋯λ_d^n_d-m_d=1.
But by construction the additive relations of a are the same
as the multiplicative relations of λ, therefore the ideals are the same.
It follows e^D = D'.



Let A∈ℚ^d× d be a rational matrix.
Then there exists an algebraic matrix B such that
⟨ B ⟩ = ⟨ e^A ⟩ = {e^At:t∈ℝ}. 


  Let P be an invertible matrix such that A = P^-1(D+N)P with
  D=diag(a_1,…,a_d) diagonal and N a nilpotent
  Jordan matrix.  By Corollary <ref> there exists a
  rational diagonal matrix D' such that
  ⟨ D'⟩ = ⟨ e^D⟩.  We
  now define B := P^-1(D'e^N)P where
  D'=diag(λ_1,…,λ_d).  Note that e^N
  is a matrix of rational numbers.  Then we have:
  
    ⟨ e^A ⟩
        = P^-1⟨ e^De^N⟩ P
        = P^-1⟨ e^D⟩·⟨ e^N⟩ P 
        = P^-1⟨ D' ⟩·⟨ e^N⟩ P
        = P^-1⟨ D'e^N⟩ P
    
        = ⟨ B ⟩  .




  Given a linear hybrid automaton 𝒜, one can compute a
  finite affine program 𝒜' that the same algebraic
  invariants, i.e., V(𝒜)=V(𝒜').


Suppose that 𝒜=(Q,A,E,T). We define
𝒜'=(Q,A',E',T), where
A'_q=0 for all q∈ Q and

    E'=E∪{ (q,B_q,q) : q ∈ Q}  ,

with B_q is an algebraic matrix such that
e^A_q = B_q for all q ∈ Q.
The existence of the matrices B_q is guaranteed by
Proposition <ref>.  In other words, we 
obtain 𝒜' from 𝒜 by setting the derivative of all variables to 0
in every location and by adding a compensatory selfloop edge to every location.

The reasoning that V(𝒜)=V(𝒜') is entirely
analogous to that in the proof of
Proposition <ref>.













§ SWITCHING SYSTEMS WITH GUARDS


In this section we consider linear hybrid automata with no discrete
updates on the variables but with equality guards on the discrete mode
changes.  For such systems there is a smallest algebraic inductive
invariant, which can be obtained as the (location-wise) intersection
of the family of all algebraic inductive invariants.  However, as we
show in this section, this invariant is no longer computable.  In
other words, in the presence of equality guards the analog of
Theorem <ref> fails.  (As an aside we remark that the
discrete mode changes no longer induce Zariski continuous maps on
configurations if there are equality guards.  Hence we cannot
necessarily recover the smallest algebraic inductive invariant as the
Zariski closure of the collecting semantics).


  There is no algorithm that computes the strongest algebraic
  inductive invariant for the class of switching systems with equality
  guards.


 The idea is to simulate
a 2-counter machine in such a way that if the machine has an infinite
run then the strongest invariant has dimension 2, and otherwise it
has dimension 1. Since the dimension of an algebraic set can be effectively
determined; this concludes the sketch.


plainurl







































§ TIME DISCRETISATION

































For a rational matrix A ∈ℚ^d × d we have

    { e^At : t ∈ℝ} =
       ⟨ e^A ⟩  .
 


Suppose that A is diagonalisable—say A=U^-1DU for some invertible matrix U and D=diag(a_1,…,a_d).
It suffices to prove that 
 { e^Dt : t ∈ℝ} =
   ⟨ e^D ⟩.

  Consider a
  multiplicative relationship among the eigenvalues of e^D—say
  (e^a_1)^n_1⋯ (e^a_d)^n_d=1, where
  n_1,…,n_d ∈ℤ.
Then a_1n_1+⋯ + a_dn_d ∈ (2π i)ℤ.
But since a_1,…,a_d are algebraic numbers, we must in fact have
a_dn_d+⋯ + a_dn_d=0.  
It follows that a_1tn_1+⋯ +a_dtn_d =0 for all t∈ℝ
and hence (e^a_1t)^n_1⋯ (e^a_dt)^n_d=1 for all
t∈ℝ, i.e., the same multiplicative relation also holds among the eigenvalues of e^Dt.

Since the ideal of all polynomial relations satisfied by
⟨ e^D⟩ is generated by the multiplicative relations
satisfied by the eigenvalues of e^D, we have that for any
t∈ℝ, matrix e^Dt satisfies all polynomial relations
satisfied by ⟨ e^D ⟩.  This proves the proposition in
case A is diagonalisable.

Next, suppose that A is nilpotent.  The fact that
{e^At:t∈ℝ} = ⟨ e^A⟩
is already shown in Section 3.3 of Derksen, Jeandel, and Koiran.  

The general case can by handled by reduction to the
diagonalisable and nilpotent cases as in Proposition <ref>.


Proposition <ref> crucially relies on the fact that π
does not appear in the description of A.  Indeed, consider the case
that A=[ 2π i ]∈^1×1. Then
e^At:t∈=z∈:|z|=1 is the unit circle. However
e^An:n∈=1 is a singleton.  Such an example is
possible because the map z∈↦ e^Az is not
Zariski-continuous in general.



§ PROOF OF THEOREM <REF>


Recall that a non-deterministic 2-counter machine M consists of two
counters C and D and a list of n instructions.  Each instruction
increments one of the counters, decrements one of the counters, or
tests one of the counters for zero.  After executing a counter update
or a successful test, the machine proceeds nondeterministically to one
of two specified instructions.  The machine halts if it executes a
test instruction whose condition is false.  Given an instruction i,
if j is one of the two possible successors of i then we call the
pair (i,j) a transition of M.  Initially M starts with both
counters zero and instruction 1 is the first to be executed.  A
configuration of M is a triple consisting of the current instruction
and the current counter values.  The problem of whether such a machine
M can reach infinitely many configurations from its initial
configuration is undecidable.

Corresponding to such a 2-counter machine M we define a linear
hybrid automaton 𝒜=(Q,A,E,q) in dimension 3.  We think
of 𝒜 as having continuous variables c,d,t, where c and
d respectively correspond to the counters of M.  Each variable has
constant derivative in each location, which is zero unless otherwise
specified.  For each instruction i of M we postulate a location
q_i of 𝒜 and for each transition (i,j) of M we
postulate a location q_i,j of 𝒜.  
Variable t has slope 1 in each location q_i and slope -1 in
each location q_i,j.  For every transition(i,j) of M,
automaton 𝒜 has an edge from q_i to q_i,j with guard
t=1 and an edge from q_i,j to q_j with guard t=0.
Intuitively, if an execution of 𝒜 correctly simulates a
run of M then 𝒜 spends one time unit in each location,
alternating between locations q_i that correspond to instructions of
M and locations q_i,j that correspond to transitions of M.

Suppose that the i-th instruction of M performs an incrementation
C:=C+1.  Then variable C has slope 1 in location q_i.
Likewise if the i-th instruction if C:=C-1, then variable c has
slope -1 in location q_i.  If the i-th instruction of M is the
zero test C=0, then the edge from location q_i to q_i,j in A
has guard c=0.  There are corresponding constructions for counter
operations and tests on counter D.

This completes the description of 𝒜.
We now claim that:


  * If M can only reach finitely many configurations from the
  initial configuration then V(𝒜)={ V_q : q ∈ Q}, the
  Zariski closure of the collecting semantics, is an
  inductive invariant that has dimension one.

  * If infinitely many configuration are reachable from the initial configuration of M
then the smallest inductive invariant has dimension strictly greater than one.


To prove the claim, note that for each reachable configuration
(i,z_1,z_2) of M, the collecting semantics
Φ(𝒜)_q_i contains a half-line L containing the
point (z_1,z_2,0), whose direction is determined by the slopes of
the respective variables of 𝒜 in location q_i.  The
Zariski closure of L is the affine hull of L, i.e., the
corresponding full line containing L.  Crucially, the points added
to L to obtain the full line are all predecessors of L under the
flow relation of 𝒜.  In particular the Zariski closure is
inductive: it remains closed under the transition relation of
𝒜.  In particular, if M can only reach finitely many
configurations, then the Zariski closure of the collecting semantics
consists of finitely many lines in each location (and so has dimension
one) and is moreover an inductive invariant.

Suppose M can reach infinitely many configurations.  Since any
algebraic inductive invariant must in particular contain the Zariski
closure of the collecting semantics, it follow that any algebraic
inductive invariant must contain infinitely many lines in some
location and thus must have dimension strictly greater than one.

Since the dimension of an algebraic set can be effectively determined,
we conclude that it is not possible to compute the smallest algebraic
invariant of a linear hybrid automaton with equality guards (even with
a no discrete updates of the variables).

