In this paper, we address the complexity barrier inherent in Fourier-Motzkin elimination (FME) and cylindrical algebraic decomposition (CAD) when eliminating a block of (existential) quantifiers. To mitigate this, we propose exploiting structural sparsity in the variable dependency graph of quantified formulas. Utilizing tools from parameterized algorithms, we investigate the role of treewidth , a parameter that measures the graph’s tree-likeness, in the process of quantifier elimination. A novel dynamic programming framework, structured over a tree decomposition of the dependency graph, is developed for applying FME and CAD, and is also extensible to general quantifier elimination procedures. Crucially, we prove that when the treewidth is a constant, the framework achieves a significant exponential complexity improvement for both FME and CAD, reducing the worst-case complexity bound from doubly exponential to single exponential. Preliminary experiments on sparse linear real arithmetic (LRA) and nonlinear real arithmetic (NRA) benchmarks confirm that our algorithm outperforms the existing popular heuristic-based approaches on instances exhibiting low treewidth.

Abstract Barrier certificates, serving as differential invariants that witness system safety, play a crucial role in the verification of cyber-physical systems (CPS). Prevailing computational methods for synthesizing barrier certificates are based on semidefinite programming (SDP) by exploiting Putinar Positivstellensatz. Consequently, these approaches are limited by the Archimedean condition, which requires all variables to be bounded, i.e., systems are defined over bounded domains. For systems over unbounded domains, unfortunately, existing methods become incomplete and may fail to identify potential barrier certificates. In this paper, we address this limitation for the unbounded cases. We first give a complete characterization of polynomial barrier certificates by using homogenization, a recent technique in the optimization community to reduce an unbounded optimization problem to a bounded one. Furthermore, motivated by this formulation, we introduce the definition of homogenized systems and propose a complete characterization of a family of non-polynomial barrier certificates with more expressive power. Experimental results demonstrate that our two approaches are more effective while maintaining a comparable level of efficiency.

Abstract Interpolation-based techniques become popular in recent years, as they can improve the scalability of existing verification techniques due to their inherent modularity and local reasoning capabilities. Synthesizing Craig interpolants is the cornerstone of these techniques. In this paper, we investigate nonlinear Craig interpolant synthesis for two polynomial formulas of the general form, essentially corresponding to the underlying mathematical problem to separate two disjoint semialgebraic sets. By combining the homogenization approach with existing techniques, we prove the existence of a novel class of non-polynomial interpolants called semialgebraic interpolants. These semialgebraic interpolants subsume polynomial interpolants as a special case. To the best of our knowledge, this is the first existence result of this kind. Furthermore, we provide complete sum-of-squares characterizations for both polynomial and semialgebraic interpolants, which can be efficiently solved as semidefinite programs. Examples are provided to demonstrate the effectiveness and efficiency of our approach.

A special class of univariate transcendental decision problems called “trigonometric extension” is studied in this paper. Roughly speaking, a trigonometric extension is a ring of univariate analytic functions obtained by adjoining trigonometric functions to a ring consisting of functions having only finitely many real zeros. It is shown that in this case, the decision problem can be reduced to looking for solutions in a bounded domain. Based on the reduction, several new decidability results are established when Schanuel’s Conjecture is assumed. Furthermore, for the theory of multivariate trigonometric extension, it is proved that, although a small fragment of the theory can be reduced to the univariate case, the general theory is undecidable.

Abstract Satisfiability Modulo the Theory of Nonlinear Real Arithmetic, SMT(NRA) for short, concerns the satisfiability of polynomial formulas, which are quantifier-free Boolean combinations of polynomial equations and inequalities with integer coefficients and real variables. In this paper, we propose a local search algorithm for a special subclass of SMT(NRA), where all constraints are strict inequalities. An important fact is that, given a polynomial formula with n variables, the zero level set of the polynomials in the formula decomposes the n-dimensional real space into finitely many components (cells) and every polynomial has constant sign in each cell. The key point of our algorithm is a new operation based on real root isolation, called cell-jump, which updates the current assignment along a given direction such that the assignment can ‘jump’ from one cell to another. One cell-jump may adjust the values of several variables while traditional local search operations, such as flip for SAT and critical move for SMT(LIA), only change that of one variable. We also design a two-level operation selection to balance the success rate and efficiency. Furthermore, our algorithm can be easily generalized to a wider subclass of SMT(NRA) where polynomial equations linear with respect to some variable are allowed. Experiments show the algorithm is competitive with state-of-the-art SMT solvers, and performs particularly well on those formulas with high-degree polynomials.

A decision algorithm for the first-order theory of univariate mixed trigonometric-polynomials over the reals is proposed in this paper. In the development of the decision algorithm, the concept "contraction mapping associated with an algebraic function" is introduced and a new real root isolation algorithm for univariate mixed trigonometric-polynomials is presented. The decision algorithm is implemented with Mathematica and its effectiveness is shown by some experimental results.

Delays are ubiquitous in modern hybrid systems, which exhibit both continuous and discrete dynamical behaviors. Induced by signal transmission, conversion, the nature of plants, and so on, delays may appear either in the continuous evolution of a hybrid system such that the evolution depends not only on the present state but also on its execution history, or in the discrete switching between its different control modes. In this paper we come up with a new model of hybrid systems, called delay hybrid automata, to capture the dynamics of systems with the aforementioned two kinds of delays. Furthermore, based upon this model we study the robust switching controller synthesis problem such that the controlled delay system is able to satisfy the specified safety properties regardless of perturbations. To the end, a novel method is proposed to synthesize switching controllers based on the computation of differential invariants for continuous evolution and backward reachable sets of discrete jumps with delays. Finally, we implement a prototypical tool of our approach and demonstrate it on some case studies.

Cylindrical algebraic decomposition (CAD) plays an important role in the field of real algebraic geometry and many other areas. As is well-known, the choice of variable ordering while computing CAD has a great effect on the time and memory use of the computation as well as the number of sample points computed. In this paper, we indicate that typical CAD algorithms, if executed with respect to a special kind of variable orderings (called "the perfect elimination orderings''), naturally preserve chordality, which is well compatible with an important (variable) sparsity pattern called "the correlative sparsity''. Experimentation suggests that if the associated graph of the polynomial system in question is chordal (resp., is nearly chordal), then a perfect elimination ordering of the associated graph (resp., of a minimal chordal completion of the associated graph) can be a good variable ordering for the CAD computation. That is, by using the perfect elimination orderings, the CAD computation may produce a much smaller full set of projection polynomials than by using other naive variable orderings. More importantly, for the complexity analysis of the CAD computation via a perfect elimination ordering, an (m,d)-property of the full set of projection polynomials obtained via such an ordering is given, through which the "size'' of this set is characterized. This property indicates that when the corresponding perfect elimination tree has a lower height, the full set of projection polynomials also tends to have a smaller "size''. This is well consistent with the experimental results, hence the perfect elimination orderings with lower elimination tree height are further recommended to be used in the CAD projection.

Craig interpolant generation for non-linear theory and its combination with other theories are still in infancy, although interpolation-based techniques have become popular in the verification of programs and hybrid systems where non-linear expressions are very common. In this paper, we first prove that a polynomial interpolant of the form $$h(\mathbf {x})>0$$ exists for two mutually contradictory polynomial formulas $$\phi (\mathbf {x},\mathbf {y})$$ and $$\psi (\mathbf {x},\mathbf {z})$$ , with the form $$f_1\ge 0\wedge \cdots \wedge f_n\ge 0$$ , where $$f_i$$ are polynomials in $$\mathbf {x},\mathbf {y}$$ or $$\mathbf {x},\mathbf {z}$$ , and the quadratic module generated by $$f_i$$ is Archimedean. Then, we show that synthesizing such interpolant can be reduced to solving a semi-definite programming problem ( $$\mathrm{SDP}$$ ). In addition, we propose a verification approach to assure the validity of the synthesized interpolant and consequently avoid the unsoundness caused by numerical error in $$\mathrm{SDP}$$ solving. Besides, we discuss how to generalize our approach to general semi-algebraic formulas. Finally, as an application, we demonstrate how to apply our approach to invariant generation in program verification.

Random ordinary differential equations (RODEs) are ordinary differential equations (ODEs) that contain a stochastic process in their vector field functions. They have been used for many years in a wide range of applications, but have been a shadow existence to stochastic differential equations (SDEs) despite being able to model a wider and often physically more adequate range of disturbances. In this article, we study the safety verification problem over both finite time horizons and the infinite time horizon for RODEs incorporating Wiener processes. Concretely, we investigate the p-safety problem, where we identify the set of initial states from which the probability to satisfy safety specifications is at least p. Based on identifying a set of sample paths whose probability measure is larger than p, we propose a method of reducing stochastic reachability to adversary reachability of ODEs for solving the p-safety problem over finite time horizons. This method permits an efficient lifting of reach-set computation methods for perturbed ODEs to RODEs. In this method, the p-safety problem over finite time horizons is reduced to the problem of inner-approximating robust backward reachable sets for ODEs with time-varying perturbation inputs. We then extend the method to the p-safety problem over the infinite time horizon. Finally, we demonstrate our method on several examples.

A new sparse SOS decomposition algorithm is proposed based on a new sparsity pattern, called cross sparsity patterns. The new sparsity pattern focuses on the sparsity of terms and thus is different from the well-known correlative sparsity pattern which focuses on the sparsity of variables though the sparse SOS decomposition algorithms based on these two sparsity patterns both take use of chordal extensions/chordal decompositions. Moreover, it is proved that the SOS decomposition obtained by the new sparsity pattern is always a refinement of the block-diagonalization obtained by the sign-symmetry method. %Because the new sparsity pattern covers more sparse polynomials than correlative sparsity pattern, Various experiments show that the new algorithm dramatically saves the computational cost compared to existing tools and can handle some really huge polynomials.

Computing a basis for the exponent lattice of algebraic numbers is a basic problem in the field of computational number theory with applications to many other areas. The bottleneck of the computation of a well-known algorithm \citege1993, kauers2005 solving the problem is the computation of the primitive element of the extended field generated by the given algebraic numbers. When the extended field is of large degree, the problem seems intractable by the tool implementing the algorithm. In this paper, a special kind of exponent lattice basis is introduced. An important feature of that basis is that it can be inductively constructed, which allows us to deal with the given algebraic numbers one by one and to work in smaller fields while computing the basis. Based on this, an effective framework for constructing exponent lattice basis is proposed. Through computing a so-called pre-basis first and then solving some linear Diophantine equations, the basis can be efficiently constructed. A new certificate for multiplicative independence and some techniques for decreasing degrees of algebraic numbers are provided to speed up the computation. The new algorithm has been implemented with Mathematica and its effectiveness is verified by testing various examples.

This paper presents a numerical algorithm to verify continuous-time Markov chains (CTMCs) against multi-clock deterministic timed automata (DTA). These DTA allow for specifying properties that cannot be expressed in CSL, the logic for CTMCs used by state-of-the-art probabilistic model checkers. The core problem is to compute the probability of timed runs by the CTMC $$\mathcal{C}$$ that are accepted by the DTA $$\mathcal{A}$$ . These likelihoods equal reachability probabilities in an embedded piecewise deterministic Markov process (EPDP) obtained as product of $$\mathcal{C}$$ and $$\mathcal{A}$$ ’s region automaton. This paper provides a numerical algorithm to efficiently solve the PDEs describing these reachability probabilities. The key insight is to solve an ordinary differential equation (ODE) that exploits the specific characteristics of the product EPDP. We provide the numerical precision of our algorithm and present experimental results with a prototypical implementation.

A new projection operator based on cylindrical algebraic decomposition (CAD) is proposed. The new operator computes the intersection of projection factor sets produced by different CAD projection orders. In other words, it computes the gcd of projection polynomials in the same variables produced by different CAD projection orders. We prove that the new operator still guarantees obtaining at least one sample point from every connected component of the highest dimension, and therefore, can be used for testing semi-definiteness of polynomials. Although the complexity of the new method is still doubly exponential, in many cases, the new operator does produce smaller projection factor sets and fewer open cells. Some examples of testing semi-definiteness of polynomials, which are difficult to be solved by existing tools, have been worked out efficiently by our program based on the new method.

This article is a continuation of our earlier work [3], which introduced triangular decompositions of semi-algebraic systems and algorithms for computing them. Our new contributions include theoretical results based on which we obtain practical improvements for these decomposition algorithms.

Abstract Tiwari proved that the termination of a class of linear programs is decidable in Tiwari (Proceedings of CAV’04. Lecture notes in computer science, vol 3114, pp 70–82, 2004). The decision procedure proposed therein depends on the computation of Jordan forms . Thus, people may draw a wrong conclusion from this procedure, if they simply apply floating-point computation to compute Jordan forms. In this paper, we first use an example to explain this problem, and then present a symbolic implementation of the decision procedure. Thus, the rounding error problem is therefore avoided. Moreover, we also show that the symbolic decision procedure is as efficient as the numerical one given in Tiwari (Proceedings of CAV’04. Lecture notes in computer science, vol 3114, pp 70–82, 2004). The complexity of former is max{ O ( n 6 ), O ( n m +3 )}, while that of the latter is O ( n m +3 ), where n is the number of variables of the program and m is the number of its Boolean conditions. In addition, for the case when the characteristic polynomial of the assignment matrix is irreducible, we design a more efficient symbolic algorithm whose complexity is max( O ( n 6 ), O ( mn 3 )).

Regular chains and triangular decompositions are fundamental and well-developed tools for describing the complex solutions of polynomial systems. This paper proposes adaptations of these tools focusing on solutions of the real analogue: semi-algebraic systems.

Cylindrical algebraic decomposition is one of the most important tools for computing with semi-algebraic sets, while triangular decomposition is among the most important approaches for manipulating constructible sets. In this paper, for an arbitrary finite set F ⊂ [y1,...,yn] we apply comprehensive triangular decomposition in order to obtain an F-invariant cylindrical decomposition of the n-dimensional complex space, from which we extract an F-invariant cylindrical algebraic decomposition of the n-dimensional real space. We report on an implementation of this new approach for constructing cylindrical algebraic decompositions.

This paper presents a new and general approach for analyzing the stability of a large class of biological networks, modeled as autonomous systems of differential equations, using real solving and solution classification. The proposed approach, based on the classical technique of linearization from the qualitative theory of ordinary differential equations yet with exact symbolic computation, is applied to analyzing the local stability of the Cdc2-cyclin B/Wee1 system and the Mos/MEK/p42 MAPK cascade, two well-known models for cell and protein signaling that have been studied extensively in the literature. We provide rigorous proofs and generalizations for some of the previous results established experimentally and report our new findings.