arXiv:1709.04382v1 [] 13 Sep 2017

On the decidability of the existence of polyhedral
invariants in transition systems∗
David Monniaux
Univ. Grenoble Alpes, CNRS, Grenoble INP†, VERIMAG, 38000 Grenoble
http://www-verimag.imag.fr/~ monniaux/
September 14, 2017

Abstract
Automated program verification often proceeds by exhibiting inductive invariants entailing the desired properties. For numerical properties, a
classical class of invariants is convex polyhedra: solution sets of system of
linear (in)equalities. Forty years of research on convex polyhedral invariants have focused, on the one hand, on identifying “easier” subclasses, on
the other hand on heuristics for finding general convex polyhedra. These
heuristics are however not guaranteed to find polyhedral inductive invariants when they exist. To our best knowledge, the existence of polyhedral
inductive invariants has never been proved to be undecidable.
In this article, we show that the existence of convex polyhedral invariants is undecidable, even if there is only one control state in addition
to the “bad” one. The question is still open if one is not allowed any
nonlinear constraint.

1

Introduction

Methods for proving that a program can never enter some undesirable states
generally rely on exhibiting an inductive invariant I — a set of states containing
the initial state(s) of the system, such that there exists no transition from I to
outside of I — containing no undesirable states. If the program is safe, then the
set of its reachable states is such an inductive invariant; this set is however in
general very complex and approaches based on abstract interpretation [4] instead
seek I within a restricted class called an abstract domain. In the case of programs
defined by a control flow graph (V, E), I is typically presented as a labeling
of V . For instance, in interval analysis [4], each control location in is labeled
either with the empty set, either with an interval for each numeric variable; the
inductiveness of such a labeling may be checked by interval arithmetic.
Interval analysis however cannot express relationships between variables. In
contrast, an example of relational analysis is that of convex polyhedra [2, 3]:
∗ This work was partially supported by the European Research Council under the European
Union’s Seventh Framework Programme (FP/2007-2013) / ERC Grant Agreement nr. 306595
“STATOR”.
† Institute of Engineering Univ. Grenoble Alpes

1

each control location is labeled with a set of linear (in)equalities over the program variables. An important question is: given a transition system, and an
undesirable control location (for instance, expressing that arithmetic overflow or
out-of-bound access has occurred), is there any inductive invariant defined by labeling each control location with a convex polyhedron such that the undesirable
location is labeled with the empty set, and thus proved to be inaccessible?
To our best knowledge, all the literature on the inference of polyhedral
invariants has focused on two issues: identifying “simpler” classes of convex
polyhedra (the intervals form such a subclass), and heuristics for finding suitable (in)equalities. Cousot & Halbwachs’ seminal work on polyhedral invariants
[2, 3] proposed three such heuristics: i) propagating polyhedra along the edges
(computing their image by the transition on the edge), ii) computing the convex
hull of all incoming polyhedra if there are several incoming edges, iii) “widening” polyhedra by discarding unstable (in)equalities, ensuring termination of
the analysis. Further work included extracting potentially useful (in)equalities
from the program, and less aggressive widening operators, in the hope of finding
good invariants that coarser methods would have missed.
Yet none of these works considered showing that heuristics were needed in
the first place, that is, showing that there is no general complete algorithm
for finding inductive polyhedral invariants — such an algorithm would, given
a transition system and an undesirable state, either find an inductive invariant
proving that this state is inaccessible, either find that such an invariant does
not exist.
In the case of some restricted classes of polyhedra, the existence or nonexistence of a suitable invariant is decidable; this is most notably the case if a
“template”, a finite catalog of possible normal vectors for the constraints, is
fixed in advance. One may then study the complexity of this decision problem.
If the program variables are real (as opposed to rational) and the transitions on
the edges are expressed by a first-order linear arithmetic formula with an existential quantifier prefix, the problem is Σp2 -complete [1]. We shall see that, even
when templates are not used, it is sufficient to bound the number of constraints
per polyhedron to make the problem decidable. The issue is then what happens
with an unbounded number of constraints.
In this article, we show that this problem is undecidable even for programs
with one control state (plus one final “bad state”), as long as one can use at
least one nonlinear (polynomial) condition.

2

Undecidability of the separating inductive polyhedral invariant existence problem

Definition 1 (Inductive separating invariant). Let n ≥ 0 and D ⊆ P (Qn )
be a class of possible invariants and T ⊆ P (Qn × Qn ) be a class of possible
transition relations.
Let C be a set of control states (including ci and cf ) and for all i, j ∈ C let
τi,j ⊆ Qn × Qn be a transition relation defined by a formula in T ; let x0 ∈ Qn .
Decide whether there is an inductive invariant I ∈ DC such that x0 ∈ I(ci ) but
I(cf ) = ∅ — that is, I such that
∀i, j ∈ C∀x, x′ ∈ Qn x ∈ I(i) ∧ (x, x′ ) ∈ τi,j ⇒ x′ ∈ I(j)
2

(1)

Note that for D = P (Qn ), this problem is equivalent to the negation of
reachability of cf from ci , thus, if n ≥ 2 and T includes first order linear
arithmetic, this problem is undecidable, by simulation of a two-counter machine.
Remark 1. Consider the above definition with a real state x ∈ Rn . If D is the
set of convex polyhedra over Rn with at most k constraints, and the transitions contain linear arithmetic updates and polynomial guards, the inductive
separation problem is decidable.
Proof. The stability condition (1) is then a formula in the theory of real closed
fields, with free variables the coefficients of the k polyhedral constraints. We
thus reduce the problem of the existence of the invariant to that of satisfiability
of such a formula, which is decidable.
Theorem 1. If D is the set of convex polyhedra over Qn , and the transitions
contain (deterministic) linear arithmetic assignments and polynomial guards,
the inductive separation problem is undecidable.
Proof. We reduce the halting problem for a deterministic machine over m registers and s states, with linear updates and linear (or polynomial) arithmetic
constraints on the transitions, to the problem of existence of a convex polyhedral inductive separating invariant for a machine with m + 2 registers and s + 1
states, again with linear updates and polynomial guards on the transitions.
The target machine is obtained from the source as follows:
• the control states are the same, to which we add a special “bad state” σb
• the first m registers encode the registers of the source machine
• another register, called t, is a time counter: initialized to 0, it is incremented at every step
• another register, called y, is initialized to 0 and updated as y := y + t + 1
• the transitions are the same as those of the source machine, conjoined
with a y = (t2 + t)/2 guard (y ≤ (t2 + t)/2 also works), to which we add
transitions from all states to σb with the guard y < (t2 + t)/2.
If the source machine terminates, then there exists a bounded polyhedral inductive invariant Let (σi , xi )1≤i≤n be the run of the source machine,
when σi is the control state and xi the vector of registers at time i. The run of
the target machine is thus (σi , xi , i, (i + i2 )/2)1≤i≤n .
For each control state σ, consider the bounded polyhedron obtained as the
convex hull of those (σ, xi , i, (i + i2 )/2)1≤i≤n from the run (this polyhedron is
thus empty if and only if this control state is unreachable). This polyhedron
lies above the y ≥ (t2 + t)/2 parabola; its points are partitioned into, on the
one hand, the (σi , xi , i, (i + i2 )/2)1≤i≤n , on the other hand, points satisfying
y > (t2 + t)/2 and thus excluded from the transitions by the y = (t2 + t)/2
guard.
The collection of these polyhedra thus forms an inductive invariant, with σb
labeled with the empty polyhedron.

3

If there exists a polyhedral separating invariant, then the source machine terminates If any point in the polyhedra lies below y = (t2 + t)/2,
then σb is reachable and thus the invariant is not separating; and any point on
y = (t2 + t)/2 must be a vertex.
Suppose an infinite run (σi , xi , i, (i + i2 )/2)1≤i , then there exists at least one
of the control states σ that repeats infinitely. The corresponding (σi , xi , i, (i +
i2 )/2) are vertices of the polyhedron associated to σ, but there is an infinity of
them, which is absurd.
The same theorem and proof are valid for the set of bounded convex polyhedra over Qn , the sets of bounded and unbounded convex polyhedra over Zn .

3

Reduction to two control states

We consider a transition system operating over d ≥ 1 integer (resp. rational)
variables and N ≥ 1 control points. 0 shall be the initial control point and N −1
is the final “bad state”.
The state of the system consists in hq, x1 , . . . , xd i where 0 ≤ q < N is a
control state and x1 , . . . , xd are integer (resp. rational) variables. The initial
△

state is σ0 = h0, 0, . . . , 0i. The set of states Σ is thus {0, . . . , N − 1} × Zd (resp.
{0, . . . , N − 1} × Qd ). In the τ and B formula, we request, without loss of
generality, the only atomic propositions involving q to be of the form q = k
where 0 ≤ k < N is a constant.
Theorem 2. The inductive separating polyhedral invariant problem for N control states in dimension d reduces to the inductive separating polyhedral invariant
problem for 2 control states in dimension d + (N − 1).
Proof. In the new system of transitions, a state consists in hx1 , . . . , xd , y1 , . . . , yN −1 i.
The variables x1 , . . . , xd encode the registers of the original system. The variables y1 , . . . , yN −1 indicate which control state q of the original system is simulated by encoding it into a vertex of a simplex: q = 0 is encoded as h0, . . . , 0i,
and q > 0 is encoded into eq = h 0, . . . , 0 , 1, 0, . . . , 0i.
| {z }
q−1 times

The transition relation τ ′ the new system is obtained by replacing q = k in
each formula by hy1 , . . . , yN −1 i = eq where eq is the encoding of control state q.
The target system simulates concretely the source system, and conversely;
the concrete reachability problems are equivalent.
Let us now see that any polyhedral inductive invariant within the source
system (one polyhedron per control location) can be translated into a polyhedral invariant within the target system (one polyhedron, for the single control
location), and the converse.
A polyhedral inductive invariant within the source system consists in one
polyhedron Pq per control
S location q; it is translated into a polyhedron obtained
as the convex hull of q Pq × {eq }. Conversely, a polyhedral invariant P in
the target system is translated into the polyhedral invariant defined as Pq =
{hx1 , . . . , xd i | (hx1 , . . . , xd i, eq ) ∈ P }.

4

4

Perspectives

Most studies of the computability and complexity issues in hardware and software verification have focused on the (concrete) reachability problem for various classes of transition systems. Here, we instead consider the problem that
abstract interpreters (or other classes of tools, for instance those based on
counterexample-guided abstraction refinement) solve heuristically: finding an
invariant within a given class; or, to make it a decision problem, deciding the
existence of such an invariant.1
We started this work hoping to vindicate forty years of research on heuristics
by showing that the existence of polyhedral inductive separating invariants in
a system with transitions in linear arithmetic (integer or rational) is undecidable; we had to settle for a weaker result (involving nonlinear arithmetic). The
original question is still open; we have discussed it with experts, to no avail.

References
[1] Thomas Gawlitza and David Monniaux. “Invariant Generation through
Strategy Iteration in Succinctly Represented Control Flow Graphs”. In:
Logical Methods in Computer Science (Sept. 2012). issn: 1860-5974 . doi:
10.2168/LMCS-8(3:29)2012 . arXiv: 1209.0643 .
[2] Nicolas Halbwachs. “Détermination automatique de relations linéaires vérifiées
par les variables d’un programme”. French. PhD thesis. Université Scientifique et Médicale de Grenoble & Institut National Polytechnique de
Grenoble, Mar. 1979. hal: tel-00288805 .
[3] Patrick Cousot and Nicolas Halbwachs. “Automatic Discovery of Linear
Restraints Among Variables of a Program”. In: POPL. Ed. by Alfred V.
Aho, Stephen N. Zilles, and Thomas G. Szymanski. ACM Press, 1978,
pp. 84–96. doi: 10.1145/512760.512770 .
[4] Patrick Cousot and Radhia Cousot. “Abstract Interpretation: A Unified
Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints”. In: Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California,
USA, January 1977. Ed. by Robert M. Graham, Michael A. Harrison, and
Ravi Sethi. ACM, 1977, pp. 238–252. doi: 10.1145/512950.512973 .

1 For most abstract domains, it is possible to find a suitable invariant if one is known to
exist, by enumerating all candidate invariants and stopping when an inductive separating one
is found. This justifies the use of the existence decision problem for the purposes of theoretical
computability studies.

5

