Formal Verification of Parameterized Systems based on Induction

2025-03-23T11:07:24Z

Parameterized systems play a crucial role in the computer field, and their security is of great significance. Formal verification of parameterized protocols is especially challenging due to its "parameterized" feature, which brings complexity and undecidability. Existing automated parameterized verification methods have limitations, such as facing difficulties in automatically deriving parameterized invariants constrained by mixed Forall and Exists quantifiers, or having challenges in completing the parameterized verification of large and complex protocols. This paper proposes a formal verification framework for parameterized systems based on induction, named wiseParaverifier. It starts from small concretizations of protocols, analyzes inductive counterexamples, and constructs counterexample formulas to guide the entire process of parameterized verification. It also presents a heuristic Generalize method to quickly find auxiliary invariants, a method for promoting complex mixed quantifiers and merging parameterized invariants, and uses symmetric reduction ideas to accelerate the verification process. Experimental results show that wiseParaverifier can successfully complete automatic inductive verification on 7 cache coherence protocols and 10 distributed protocols. It has strong verification capabilities and migration capabilities, and can provide concise and readable verification results, which is helpful for learners to understand protocol behaviors.

A computational approach to rational summability and its applications via discrete residues

2025-03-19T18:46:26Z

A rational function $f(x)$ is rationally summable if there exists a rational function $g(x)$ such that $f(x)=g(x+1)-g(x)$. Detecting whether a given rational function is summable is an important and basic computational subproblem that arises in algorithms to study diverse aspects of shift difference equations. The discrete residues introduced by Chen and Singer in 2012 enjoy the obstruction-theoretic property that a rational function is summable if and only if all its discrete residues vanish. However, these discrete residues are defined in terms of the data in the complete partial fraction decomposition of the given rational function, which cannot be accessed computationally in general. We explain how to efficiently compute (a rational representation of) the discrete residues of any rational function, relying only on gcd computations, linear algebra, and a black box algorithm to compute the autodispersion set of the denominator polynomial. We also explain how to apply our algorithms to serial summability and creative telescoping problems, and how to apply these computations to compute Galois groups of difference equations.

Positivity Proofs for Linear Recurrences with Several Dominant Eigenvalues

2025-03-18T13:54:46Z

Deciding the positivity of a sequence defined by a linear recurrence and initial conditions is, in general, a hard problem. When the coefficients of the recurrences are constants, decidability has only been proven up to order 5. The difficulty arises when the characteristic polynomial of the recurrence has several roots of maximal modulus, called dominant roots of the recurrence. We study the positivity problem for recurrences with polynomial coefficients, focusing on sequences of Poincaré type, which are perturbations of constant-coefficient recurrences. The dominant eigenvalues of a recurrence in this class are the dominant roots of the associated constant-coefficient recurrence. Previously, we have proved the decidability of positivity for recurrences having a unique, simple, dominant eigenvalue, under a genericity assumption. The associated algorithm proves positivity by constructing a positive cone contracted by the recurrence operator. We extend this cone-based approach to a larger class of recurrences, where a contracted cone may no longer exist. The main idea is to construct a sequence of cones. Each cone in this sequence is mapped by the recurrence operator to the next. This construction can be applied to prove positivity by induction. For recurrences with several simple dominant eigenvalues, we provide a condition that ensures that these successive inclusions hold. Additionally, we demonstrate the applicability of our method through examples, including recurrences with a double dominant eigenvalue.

LSU factorization

2025-03-17T18:43:10Z

The matrix LU factorization algorithm is a fundamental algorithm in linear algebra. We propose a generalization of the LU and LEU algorithms to accommodate the case of a commutative domain and its field of quotients. This algorithm decomposes any matrix A into a product of three matrices A=LSU, where each element of the triangular matrices L and U is a minor of matrix A. The number of non-zero elements in matrix S is equal to rank(A), and each of them is the inverse of the product of a specific pair of matrix A minors. The algorithm's complexity is equivalent to that of matrix multiplication.

MathPartner is a breakthrough technology for natural sciences education, scientic and engineering applications

2025-03-17T16:14:01Z

The article provides a brief description of the MathPartner service. This freely available cloud-based Mathematics is a universal system for symbolic-numeric calculations. Its Mathpar language is a subset of the LaTeX language, but allows you to create mathematical texts that contain "computable" mathematical operators. This opens up completely new opportunities for improving the educational process for all natural science disciplines, for the use of mathematics in scientific and engineering calculations. To save and freely exchange educational and other texts in the Mathpar language, a GitHub repository has been created. It is concluded that cloud mathematics MathPartner is a new breakthrough technology for school and university natural science education, for scientific and engineering applications.

Symbolic Summation of Multivariate Rational Functions

2025-03-17T12:19:53Z

Symbolic summation as an active research topic of symbolic computation provides efficient algorithmic tools for evaluating and simplifying different types of sums arising from mathematics, computer science, physics and other areas. Most of existing algorithms in symbolic summation are mainly applicable to the problem with univariate inputs. A long-term project in symbolic computation is to develop theories, algorithms and software for the symbolic summation of multivariate functions. This paper will give complete solutions to two challenging problems in symbolic summation of multivariate rational functions, namely the rational summability problem and the existence problem of telescopers for multivariate rational functions. Our approach is based on the structure of Sato's isotropy groups of polynomials, which enables us to reduce the problems to testing the shift equivalence of polynomials. Our results provide a complete solution to the discrete analogue of Picard's problem on differential forms and can be used to detect the applicability of the Wilf-Zeilberger method to multivariate rational functions.

Frobenius method for Mahler equations

2025-03-17T09:52:41Z

Using Hahn series, one can attach to any linear Mahler equation a basis of solutions at 0 reminiscent of the solutions of linear differential equations at a regular singularity. We show that such a basis of solutions can be produced by using a variant of Frobenius method.

New Results on Periodic Golay Pairs

2025-03-16T04:09:05Z

In this paper, we provide algorithmic methods for conducting exhaustive searches for periodic Golay pairs. Our methods enumerate several lengths beyond the currently known state-of-the-art available searches: we conducted exhaustive searches for periodic Golay pairs of all lengths $v \leq 72$ using our methods, while only lengths $v \leq 34$ had previously been exhaustively enumerated. Our methods are applicable to periodic complementary sequences in general. We utilize sequence compression, a method of sequence generation derived in 2013 by Djoković and Kotsireas. We also introduce and implement a new method of "multi-level" compression, where sequences are uncompressed in several steps. This method allowed us to exhaustively search all lengths $v \leq 72$ using less than 10 CPU years. For cases of complementary sequences where uncompression is not possible, we introduce some new methods of sequence generation inspired by the isomorph-free exhaustive generation algorithm of orderly generation. Finally, we pose a conjecture regarding the structure of periodic Golay pairs and prove it holds in many lengths, including all lengths $v \lt 100$. We demonstrate the usefulness of our algorithms by providing the first ever examples of periodic Golay pairs of length $v = 90$. The smallest length for which the existence of periodic Golay pairs is undecided is now $106$.

Deciding Connectivity in Symmetric Semi-Algebraic Sets

2025-03-15T22:18:01Z

A semi-algebraic set is a subset of $\mathbb{R}^n$ defined by a finite collection of polynomial equations and inequalities. In this paper, we investigate the problem of determining whether two points in such a set belong to the same connected component. We focus on the case where the defining equations and inequalities are invariant under the natural action of the symmetric group and where each polynomial has degree at most $ d $, with $ d < n $ (where $ n $ denotes the number of variables). Exploiting this symmetry, we develop and analyze algorithms for two key tasks. First, we present an algorithm that determines whether the orbits of two given points are connected. Second, we provide an algorithm that decides connectivity between arbitrary points in the set. Both algorithms run in polynomial time with respect to $ n $.

Constraint-Generation Policy Optimization (CGPO): Nonlinear Programming for Policy Optimization in Mixed Discrete-Continuous MDPs

2025-03-14T22:23:32Z

We propose the Constraint-Generation Policy Optimization (CGPO) framework to optimize policy parameters within compact and interpretable policy classes for mixed discrete-continuous Markov Decision Processes (DC-MDP). CGPO can not only provide bounded policy error guarantees over an infinite range of initial states for many DC-MDPs with expressive nonlinear dynamics, but it can also provably derive optimal policies in cases where it terminates with zero error. Furthermore, CGPO can generate worst-case state trajectories to diagnose policy deficiencies and provide counterfactual explanations of optimal actions. To achieve such results, CGPO proposes a bilevel mixed-integer nonlinear optimization framework for optimizing policies in defined expressivity classes (e.g. piecewise linear) and reduces it to an optimal constraint generation methodology that adversarially generates worst-case state trajectories. Furthermore, leveraging modern nonlinear optimizers, CGPO can obtain solutions with bounded optimality gap guarantees. We handle stochastic transitions through chance constraints, providing high-probability performance guarantees. We also present a roadmap for understanding the computational complexities of different expressivity classes of policy, reward, and transition dynamics. We experimentally demonstrate the applicability of CGPO across various domains, including inventory control, management of a water reservoir system, and physics control. In summary, CGPO provides structured, compact and explainable policies with bounded performance guarantees, enabling worst-case scenario generation and counterfactual policy diagnostics.

On the Computation of Newton Polytopes of Eliminants

2025-03-14T10:49:48Z

For systems of polynomial equations, we study the problem of computing the Newton polytope of their eliminants. As was shown by Esterov and Khovanskii, such Newton polytopes are mixed fiber polytopes of the Newton polytopes of the input equations. We use their results in combination with mixed subdivisions to design an algorithm computing these special polytopes. We demonstrate the increase in practical performance of our algorithm compared to existing methods using tropical geometry and discuss the differences that lead to this increase in performance. We also demonstrate an application of our work to differential elimination.

Positivity sets of hinge functions

2025-03-14T10:26:24Z

In this paper we investigate which subsets of the real plane are realisable as the set of points on which a one-layer ReLU neural network takes a positive value. In the case of cones we give a full characterisation of such sets. Furthermore, we give a necessary condition for any subset of $\mathbb R^d$. We give various examples of such one-layer neural networks.

Super-Linear Speedup by Generalizing Runtime Repeated Recursion Unfolding in Prolog

2025-03-13T14:36:48Z

Runtime repeated recursion unfolding was recently introduced as a just-in-time program transformation strategy that can achieve super-linear speedup. So far, the method was restricted to single linear direct recursive rules in the programming language Constraint Handling Rules (CHR). In this companion paper, we generalize the technique to multiple recursion and to multiple recursive rules and provide an implementation of the generalized method in the logic programming language Prolog. The basic idea of the approach is as follows: When a recursive call is encountered at runtime, the recursive rule is unfolded with itself and this process is repeated with each resulting unfolded rule as long as it is applicable to the current call. In this way, more and more recursive steps are combined into one recursive step. Then an interpreter applies these rules to the call starting from the most unfolded rule. For recursions which have sufficiently simplifyable unfoldings, a super-linear can be achieved, i.e. the time complexity is reduced. We implement an unfolder, a generalized meta-interpreter and a novel round-robin rule processor for our generalization of runtime repeated recursion unfolding with just ten clauses in Prolog. We illustrate the feasibility of our technique with worst-case time complexity estimates and benchmarks for some basic classical algorithms that achieve a super-linear speedup.

Parsing the Language of Expression: Enhancing Symbolic Regression with Domain-Aware Symbolic Priors

2025-03-12T17:57:48Z

Symbolic regression is essential for deriving interpretable expressions that elucidate complex phenomena by exposing the underlying mathematical and physical relationships in data. In this paper, we present an advanced symbolic regression method that integrates symbol priors from diverse scientific domains - including physics, biology, chemistry, and engineering - into the regression process. By systematically analyzing domain-specific expressions, we derive probability distributions of symbols to guide expression generation. We propose novel tree-structured recurrent neural networks (RNNs) that leverage these symbol priors, enabling domain knowledge to steer the learning process. Additionally, we introduce a hierarchical tree structure for representing expressions, where unary and binary operators are organized to facilitate more efficient learning. To further accelerate training, we compile characteristic expression blocks from each domain and include them in the operator dictionary, providing relevant building blocks. Experimental results demonstrate that leveraging symbol priors significantly enhances the performance of symbolic regression, resulting in faster convergence and higher accuracy.

Isotropic vectors over global fields

2025-03-12T09:03:57Z

We present a complete suite of algorithms for finding isotropic vectors of quadratic forms (of any dimension) over an arbitrary global field of characteristic different from 2. This is a new version with numerous changes and improvements.