Using linear algebra in decomposition of Farkas interpolants

The use of propositional logic and systems of linear inequalities over reals is a common means to model software for formal verification. Craig interpolants constitute a central building block in this setting for over-approximating reachable states, e.g. as candidates for inductive loop invariants. Interpolants for a linear system can be efficiently computed from a Simplex refutation by applying the Farkas’ lemma. However, these interpolants do not always suit the verification task—in the worst case, they can even prevent the verification algorithm from converging. This work introduces the decomposed interpolants, a fundamental extension of the Farkas interpolants, obtained by identifying and separating independent components from the interpolant structure, using methods from linear algebra. We also present an efficient polynomial algorithm to compute decomposed interpolants and analyse its properties. We experimentally show that the use of decomposed interpolants in model checking results in immediate convergence on instances where state-of-the-art approaches diverge. Moreover, since being based on the efficient Simplex method, the approach is very competitive in general.

On the Locally Polynomial Complexity of the Projection-Gradient Method for Solving Piecewise Quadratic Optimisation Problems

This paper proposes a method for solving optimisation problems involving piecewise quadratic functions. The method provides a solution in a finite number of iterations, and the computational complexity of the proposed method is locally polynomial of the problem dimension, i.e., if the initial point belongs to the sufficiently small neighbourhood of the solution set. Proposed method could be applied for solving large systems of linear inequalities.

Constructing and Adapting Technology-Infused Lessons

Design principles are used to construct and refine a technology-infused lesson for beginning algebra students learning about systems of linear inequalities.

Characterization of the conditional stationary distribution in Markov chains via systems of linear inequalities

This paper considers ergodic, continuous-time Markov chains $\{X(t)\}_{t \in (\!-\infty,\infty)}$ on $\mathbb{Z}^+=\{0,1,\ldots\}$ . For an arbitrarily fixed $N \in \mathbb{Z}^+$ , we study the conditional stationary distribution $\boldsymbol{\pi}(N)$ given the Markov chain being in $\{0,1,\ldots,N\}$ . We first characterize $\boldsymbol{\pi}(N)$ via systems of linear inequalities and identify simplices that contain $\boldsymbol{\pi}(N)$ , by examining the $(N+1) \times (N+1)$ northwest corner block of the infinitesimal generator $\textbf{\textit{Q}}$ and the subset of the first $N+1$ states whose members are directly reachable from at least one state in $\{N+1,N+2,\ldots\}$ . These results are closely related to the augmented truncation approximation (ATA), and we provide some practical implications for the ATA. Next we consider an extension of the above results, using the $(K+1) \times (K+1)$ ( $K > N$ ) northwest corner block of $\textbf{\textit{Q}}$ and the subset of the first $K+1$ states whose members are directly reachable from at least one state in $\{K+1,K+2,\ldots\}$ . Furthermore, we introduce new state transition structures called (K, N)-skip-free sets, using which we obtain the minimum convex polytope that contains $\boldsymbol{\pi}(N)$ .

The greedy strategy for optimizing the Perron eigenvalue

We address the problems of minimizing and of maximizing the spectral radius over a compact family of non-negative matrices. Those problems being hard in general can be efficiently solved for some special families. We consider the so-called product families, where each matrix is composed of rows chosen independently from given sets. A recently introduced greedy method works very fast. However, it is applicable mostly for strictly positive matrices. For sparse matrices, it often diverges and gives a wrong answer. We present the “selective greedy method” that works equally well for all non-negative product families, including sparse ones. For this method, we prove a quadratic rate of convergence and demonstrate its efficiency in numerical examples. The numerical examples are realised for two cases: finite uncertainty sets and polyhedral uncertainty sets given by systems of linear inequalities. In dimensions up to 2000, the matrices with minimal/maximal spectral radii in product families are found within a few iterations. Applications to dynamical systems and to the graph theory are considered.

Formal Chronicle Analyses and Comparisons: How to Deal with Negative Behaviors

The overall context of this paper is the event-based behavior analysis and focuses on modeling and analyzing behaviors of interest involving time information. Any behavior of interest from any time event system is concisely defined as a set of time constrained events that must occur (positive behavior) and a set of time constrained events that must not occur (negative behavior). This article proposes a formal extension of the chronicle formalism that allows for the concise description of positive and negative behaviors. Based on this new formalism, several criteria are introduced, they formally characterize and compare a set of chronicles. A fully proved implementation of the proposed criteria is then described; it relies on the use of polyhedron techniques to solve systems of linear inequalities.