-
Beyond Affine Loops: A Geometric Approach to Program Synthesis
Authors:
Erdenebayar Bayarmagnai,
Fatemeh Mohammadi,
Rémi Prébet
Abstract:
Ensuring software correctness remains a fundamental challenge in formal program verification. One promising approach relies on finding polynomial invariants for loops. Polynomial invariants are properties of a program loop that hold before and after each iteration. Generating polynomial invariants is a crucial task for loops, but it is an undecidable problem in the general case. Recently, an alter…
▽ More
Ensuring software correctness remains a fundamental challenge in formal program verification. One promising approach relies on finding polynomial invariants for loops. Polynomial invariants are properties of a program loop that hold before and after each iteration. Generating polynomial invariants is a crucial task for loops, but it is an undecidable problem in the general case. Recently, an alternative approach to this problem has emerged, focusing on synthesizing loops from invariants. However, existing methods only synthesize affine loops without guard conditions from polynomial invariants. In this paper, we address a more general problem, allowing loops to have polynomial update maps with a given structure, inequations in the guard condition, and polynomial invariants of arbitrary form.
In this paper, we use algebraic geometry tools to design and implement an algorithm that computes a finite set of polynomial equations whose solutions correspond to all loops satisfying the given polynomial invariants. In other words, we reduce the problem of synthesizing loops to finding solutions of polynomial systems within a specified subset of the complex numbers. The latter is handled in our software using an SMT solver.
△ Less
Submitted 1 May, 2025;
originally announced May 2025.
-
Efficient Algorithms for Minimal Matroid Extensions and Irreducible Decompositions of Circuit Varieties
Authors:
Emiliano Liwski,
Fatemeh Mohammadi,
Rémi Prébet
Abstract:
We introduce an efficient method for decomposing the circuit variety of a given matroid $M$, based on an algorithm that identifies its minimal extensions. These extensions correspond to the smallest elements above $M$ in the poset defined by the dependency order. We apply our algorithm to several classical configurations: the Vámos matroid, the unique Steiner quadruple system $S(3,4,8)$, the proje…
▽ More
We introduce an efficient method for decomposing the circuit variety of a given matroid $M$, based on an algorithm that identifies its minimal extensions. These extensions correspond to the smallest elements above $M$ in the poset defined by the dependency order. We apply our algorithm to several classical configurations: the Vámos matroid, the unique Steiner quadruple system $S(3,4,8)$, the projective and affine planes, the dual of the Fano matroid, and the dual of the graphic matroid of $K_{3,3}$. In each case, we compute the minimal irreducible decomposition of their circuit varieties.
△ Less
Submitted 23 April, 2025;
originally announced April 2025.
-
Algebraic Tools for Computing Polynomial Loop Invariants (Extended Version)
Authors:
Erdenebayar Bayarmagnai,
Fatemeh Mohammadi,
Rémi Prébet
Abstract:
Loop invariants are properties of a program loop that hold both before and after each iteration of the loop. They are often used to verify programs and ensure that algorithms consistently produce correct results during execution. Consequently, generating invariants becomes a crucial task for loops. We specifically focus on polynomial loops, where both the loop conditions and the assignments within…
▽ More
Loop invariants are properties of a program loop that hold both before and after each iteration of the loop. They are often used to verify programs and ensure that algorithms consistently produce correct results during execution. Consequently, generating invariants becomes a crucial task for loops. We specifically focus on polynomial loops, where both the loop conditions and the assignments within the loop are expressed as polynomials. Although computing polynomial invariants for general loops is undecidable, efficient algorithms have been developed for certain classes of loops. For instance, when all assignments within a while loop involve linear polynomials, the loop becomes solvable. In this work, we study the more general case, where the polynomials can have arbitrary degrees.
Using tools from algebraic geometry, we present two algorithms designed to generate all polynomial invariants within a given vector subspace, for a branching loop with nondeterministic conditional statements. These algorithms combine linear algebra subroutines with computations on polynomial ideals. They differ depending on whether the initial values of the loop variables are specified or treated as parameters. Additionally, we present a much more efficient algorithm for generating polynomial invariants of a specific form, applicable to all initial values. This algorithm avoids expensive ideal computations.
△ Less
Submitted 18 December, 2024;
originally announced December 2024.
-
Algebraic Tools for Computing Polynomial Loop Invariants
Authors:
Erdenebayar Bayarmagnai,
Fatemeh Mohammadi,
Rémi Prébet
Abstract:
Loop invariants are properties of a program loop that hold before and after each iteration of the loop. They are often employed to verify programs and ensure that algorithms consistently produce correct results during execution. Consequently, the generation of invariants becomes a crucial task for loops. We specifically focus on polynomial loops, where both the loop conditions and assignments with…
▽ More
Loop invariants are properties of a program loop that hold before and after each iteration of the loop. They are often employed to verify programs and ensure that algorithms consistently produce correct results during execution. Consequently, the generation of invariants becomes a crucial task for loops. We specifically focus on polynomial loops, where both the loop conditions and assignments within the loop are expressed as polynomials. Although computing polynomial invariants for general loops is undecidable, efficient algorithms have been developed for certain classes of loops. For instance, when all assignments within a while loop involve linear polynomials, the loop becomes solvable. In this work, we study the more general case where the polynomials exhibit arbitrary degrees.
Applying tools from algebraic geometry, we present two algorithms designed to generate all polynomial invariants for a while loop, up to a specified degree. These algorithms differ based on whether the initial values of the loop variables are given or treated as parameters. Furthermore, we introduce various methods to address cases where the algebraic problem exceeds the computational capabilities of our methods. In such instances, we identify alternative approaches to generate specific polynomial invariants.
△ Less
Submitted 15 May, 2024;
originally announced May 2024.
-
Computing roadmaps in unbounded smooth real algebraic sets II: algorithm and complexity
Authors:
Rémi Prébet,
Mohab Safey El Din,
Éric Schost
Abstract:
A roadmap for an algebraic set $V$ defined by polynomials with coefficients in some real field, say $\mathbb{R}$, is an algebraic curve contained in $V$ whose intersection with all connected components of $V\cap\mathbb{R}^{n}$ is connected. These objects, introduced by Canny, can be used to answer connectivity queries over $V\cap \mathbb{R}^{n}$ provided that they are required to contain the finit…
▽ More
A roadmap for an algebraic set $V$ defined by polynomials with coefficients in some real field, say $\mathbb{R}$, is an algebraic curve contained in $V$ whose intersection with all connected components of $V\cap\mathbb{R}^{n}$ is connected. These objects, introduced by Canny, can be used to answer connectivity queries over $V\cap \mathbb{R}^{n}$ provided that they are required to contain the finite set of query points $\mathcal{P}\subset V$; in this case,we say that the roadmap is associated to $(V, \mathcal{P})$.
In this paper, we make effective a connectivity result we previously proved, to design a Monte Carlo algorithm which, on input (i) a finite sequence of polynomials defining $V$ (and satisfying some regularity assumptions) and (ii) an algebraic representation of finitely many query points $\mathcal{P}$ in $V$, computes a roadmap for $(V, \mathcal{P})$. This algorithm generalizes the nearly optimal one introduced by the last two authors by dropping a boundedness assumption on the real trace of $V$.
The output size and running times of our algorithm are both polynomial in $(nD)^{n\log d}$, where $D$ is the maximal degree of the input equations and $d$ is the dimension of $V$. As far as we know, the best previously known algorithm dealing with such sets has an output size and running time polynomial in $(nD)^{n\log^2 n}$.
△ Less
Submitted 5 February, 2024;
originally announced February 2024.
-
Algorithm for connectivity queries on real algebraic curves
Authors:
Md Nazrul Islam,
Adrien Poteaux,
Rémi Prébet
Abstract:
We consider the problem of answering connectivity queries on a real algebraic curve. The curve is given as the real trace of an algebraic curve, assumed to be in generic position, and being defined by some rational parametrizations. The query points are given by a zero-dimensional parametrization. We design an algorithm which counts the number of connected components of the real curve under study,…
▽ More
We consider the problem of answering connectivity queries on a real algebraic curve. The curve is given as the real trace of an algebraic curve, assumed to be in generic position, and being defined by some rational parametrizations. The query points are given by a zero-dimensional parametrization. We design an algorithm which counts the number of connected components of the real curve under study, and decides which query point lie in which connected component, in time log-linear in $N^6$, where $N$ is the maximum of the degrees and coefficient bit-sizes of the polynomials given as input. This matches the currently best-known bound for computing the topology of real plane curves. The main novelty of this algorithm is the avoidance of the computation of the complete topology of the curve.
△ Less
Submitted 11 July, 2023; v1 submitted 22 February, 2023;
originally announced February 2023.
-
Deciding Cuspidality of Manipulators through Computer Algebra and Algorithms in Real Algebraic Geometry
Authors:
Damien Chablat,
Rémi Prébet,
Mohab Safey El Din,
Durgesh Salunkhe,
Philippe Wenger
Abstract:
Cuspidal robots are robots with at least two inverse kinematic solutions that can be connected by a singularity-free path. Deciding the cuspidality of generic 3R robots has been studied in the past, but extending the study to six-degree-of-freedom robots can be a challenging problem. Many robots can be modeled as a polynomial map together with a real algebraic set so that the notion of cuspidality…
▽ More
Cuspidal robots are robots with at least two inverse kinematic solutions that can be connected by a singularity-free path. Deciding the cuspidality of generic 3R robots has been studied in the past, but extending the study to six-degree-of-freedom robots can be a challenging problem. Many robots can be modeled as a polynomial map together with a real algebraic set so that the notion of cuspidality can be extended to these data. In this paper we design an algorithm that, on input a polynomial map in $n$ indeterminates, and $s$ polynomials in the same indeterminates describing a real algebraic set of dimension $d$, decides the cuspidality of the restriction of the map to the real algebraic set under consideration. Moreover, if $D$ and $τ$ are, respectively the maximum degree and the bound on the bit size of the coefficients of the input polynomials, this algorithm runs in time log-linear in $τ$ and polynomial in $((s+d)D)^{O(n^2)}$. It relies on many high-level algorithms in computer algebra which use advanced methods on real algebraic sets and critical loci of polynomial maps. As far as we know, this is the first algorithm that tackles the cuspidality problem from a general point of view.
△ Less
Submitted 25 July, 2022; v1 submitted 9 March, 2022;
originally announced March 2022.
-
Computing roadmaps in unbounded smooth real algebraic sets I: connectivity results
Authors:
Rémi Prébet,
Mohab Safey El Din,
Éric Schost
Abstract:
Answering connectivity queries in real algebraic sets is a fundamental problem in effective real algebraic geometry that finds many applications in e.g. robotics where motion planning issues are topical. This computational problem is tackled through the computation of so-called roadmaps which are real algebraic subsets of the set V under study, of dimension at most one, and which have a connected…
▽ More
Answering connectivity queries in real algebraic sets is a fundamental problem in effective real algebraic geometry that finds many applications in e.g. robotics where motion planning issues are topical. This computational problem is tackled through the computation of so-called roadmaps which are real algebraic subsets of the set V under study, of dimension at most one, and which have a connected intersection with all semi-algebraically connected components of V. Algorithms for computing roadmaps rely on statements establishing connectivity properties of some well-chosen subsets of V , assuming that V is bounded.
In this paper, we extend such connectivity statements by dropping the boundedness assumption on V. This exploits properties of so-called generalized polar varieties, which are critical loci of V for some well-chosen polynomial maps.
△ Less
Submitted 7 June, 2023; v1 submitted 8 March, 2022;
originally announced March 2022.
