Searcharxiv⌕ Search

arXiv subjects

James Worrell

Publications and source records attributed to James Worrell.

At least 91 records · Page 5Linked to original sources
arXiv2017

Nonnegative Matrix Factorization Requires Irrationality

Nonnegative matrix factorization (NMF) is the problem of decomposing a given nonnegative $n \times m$ matrix $M$ into a product of a nonnegative $n \times d$ matrix $W$ and a nonnegative $d \times m$ matrix $H$. A longstanding open question, posed by Cohen and Rothblum in 1993, is whether a rational matrix $M$ always has an NMF of minimal inner dimension $d$ whose factors $W$ and $H$ are also rational. We answer this question negatively, by exhibiting a matrix for which $W$ and $H$ require irrational entries.

cs.CC↗
arXiv2017

On the Polytope Escape Problem for Continuous Linear Dynamical Systems

The Polyhedral Escape Problem for continuous linear dynamical systems consists of deciding, given an affine function $f: \mathbb{R}^{d} \rightarrow \mathbb{R}^{d}$ and a convex polyhedron $\mathcal{P} \subseteq \mathbb{R}^{d}$, whether, for some initial point $\boldsymbol{x}_{0}$ in $\mathcal{P}$, the trajectory of the unique solution to the differential equation $\dot{\boldsymbol{x}}(t)=f(\boldsymbol{x}(t))$, $\boldsymbol{x}(0)=\boldsymbol{x}_{0}$, is entirely contained in $\mathcal{P}$. We show that this problem is decidable, by reducing it in polynomial time to the decision version of linear programming with real algebraic coefficients, thus placing it in $\exists \mathbb{R}$, which lies between NP and PSPACE. Our algorithm makes use of spectral techniques and relies among others on tools from Diophantine approximation.

cs.CC↗
arXiv2017

Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem

The \emph{Orbit Problem} consists of determining, given a linear transformation $A$ on $\mathbb{Q}^d$, together with vectors $x$ and $y$, whether the orbit of $x$ under repeated applications of $A$ can ever reach $y$. This problem was famously shown to be decidable by Kannan and Lipton in the 1980s. In this paper, we are concerned with the problem of synthesising suitable \emph{invariants} $\mathcal{P} \subseteq \mathbb{R}^d$, \emph{i.e.}, sets that are stable under $A$ and contain $x$ and not $y$, thereby providing compact and versatile certificates of non-reachability. We show that whether a given instance of the Orbit Problem admits a semialgebraic invariant is decidable, and moreover in positive instances we provide an algorithm to synthesise suitable invariants of polynomial size. It is worth noting that the existence of \emph{semilinear} invariants, on the other hand, is (to the best of our knowledge) not known to be decidable.

cs.CC↗
arXiv2016

The Polytope-Collision Problem

The Orbit Problem consists of determining, given a matrix $A\in \mathbb{R}^{d\times d}$ and vectors $x,y\in \mathbb{R}^d$, whether there exists $n\in \mathbb{N}$ such that $A^n=y$. This problem was shown to be decidable in a seminal work of Kannan and Lipton in the 1980s. Subsequently, Kannan and Lipton noted that the Orbit Problem becomes considerably harder when the target $y$ is replaced with a subspace of $\mathbb{R}^d$. Recently, it was shown that the problem is decidable for vector-space targets of dimension at most three, followed by another development showing that the problem is in PSPACE for polytope targets of dimension at most three. In this work, we take a dual look at the problem, and consider the case where the initial vector $x$ is replaced with a polytope $P_1$, and the target is a polytope $P_2$. Then, the question is whether there exists $n\in \mathbb{N}$ such that $A^n P_1\cap P_2\neq \emptyset$. We show that the problem can be decided in PSPACE for dimension at most three. As in previous works, decidability in the case of higher dimensions is left open, as the problem is known to be hard for long-standing number-theoretic open problems. Our proof begins by formulating the problem as the satisfiability of a parametrized family of sentences in the existential first-order theory of real-closed fields. Then, after removing quantifiers, we are left with instances of simultaneous positivity of sums of exponentials. Using techniques from transcendental number theory, and separation bounds on algebraic numbers, we are able to solve such instances in PSPACE.

cs.CC↗
arXiv2016

On the Complexity of the Orbit Problem

We consider higher-dimensional versions of Kannan and Lipton's Orbit Problem---determining whether a target vector space V may be reached from a starting point x under repeated applications of a linear transformation A. Answering two questions posed by Kannan and Lipton in the 1980s, we show that when V has dimension one, this problem is solvable in polynomial time, and when V has dimension two or three, the problem is in NP^{RP}.

cs.CC↗
arXiv2016

On Restricted Nonnegative Matrix Factorization

Nonnegative matrix factorization (NMF) is the problem of decomposing a given nonnegative $n \times m$ matrix $M$ into a product of a nonnegative $n \times d$ matrix $W$ and a nonnegative $d \times m$ matrix $H$. Restricted NMF requires in addition that the column spaces of $M$ and $W$ coincide. Finding the minimal inner dimension $d$ is known to be NP-hard, both for NMF and restricted NMF. We show that restricted NMF is closely related to a question about the nature of minimal probabilistic automata, posed by Paz in his seminal 1971 textbook. We use this connection to answer Paz's question negatively, thus falsifying a positive answer claimed in 1974. Furthermore, we investigate whether a rational matrix $M$ always has a restricted NMF of minimal inner dimension whose factors $W$ and $H$ are also rational. We show that this holds for matrices $M$ of rank at most $3$ and we exhibit a rank-$4$ matrix for which $W$ and $H$ require irrational entries.

cs.FL↗
arXiv2016

Solvability of Matrix-Exponential Equations

We consider a continuous analogue of Babai et al.'s and Cai et al.'s problem of solving multiplicative matrix equations. Given $k+1$ square matrices $A_{1}, \ldots, A_{k}, C$, all of the same dimension, whose entries are real algebraic, we examine the problem of deciding whether there exist non-negative reals $t_{1}, \ldots, t_{k}$ such that \begin{align*} \prod \limits_{i=1}^{k} \exp(A_{i} t_{i}) = C . \end{align*} We show that this problem is undecidable in general, but decidable under the assumption that the matrices $A_{1}, \ldots, A_{k}$ commute. Our results have applications to reachability problems for linear hybrid automata. Our decidability proof relies on a number of theorems from algebraic and transcendental number theory, most notably those of Baker, Kronecker, Lindemann, and Masser, as well as some useful geometric and linear-algebraic results, including the Minkowski-Weyl theorem and a new (to the best of our knowledge) result about the uniqueness of strictly upper triangular matrix logarithms of upper unitriangular matrices. On the other hand, our undecidability result is shown by reduction from Hilbert's Tenth Problem.

cs.DM↗
arXiv2016

On the Skolem Problem for Continuous Linear Dynamical Systems

The Continuous Skolem Problem asks whether a real-valued function satisfying a linear differential equation has a zero in a given interval of real numbers. This is a fundamental reachability problem for continuous linear dynamical systems, such as linear hybrid automata and continuous-time Markov chains. Decidability of the problem is currently open---indeed decidability is open even for the sub-problem in which a zero is sought in a bounded interval. In this paper we show decidability of the bounded problem subject to Schanuel's Conjecture, a unifying conjecture in transcendental number theory. We furthermore analyse the unbounded problem in terms of the frequencies of the differential equation, that is, the imaginary parts of the characteristic roots. We show that the unbounded problem can be reduced to the bounded problem if there is at most one rationally linearly independent frequency, or if there are two rationally linearly independent frequencies and all characteristic roots are simple. We complete the picture by showing that decidability of the unbounded problem in the case of two (or more) rationally linearly independent frequencies would entail a major new effectiveness result in Diophantine approximation, namely computability of the Diophantine-approximation types of all real algebraic numbers.

eess.SY↗
arXiv2016

On Recurrent Reachability for Continuous Linear Dynamical Systems

The continuous evolution of a wide variety of systems, including continuous-time Markov chains and linear hybrid automata, can be described in terms of linear differential equations. In this paper we study the decision problem of whether the solution $\boldsymbol{x}(t)$ of a system of linear differential equations $d\boldsymbol{x}/dt=A\boldsymbol{x}$ reaches a target halfspace infinitely often. This recurrent reachability problem can equivalently be formulated as the following Infinite Zeros Problem: does a real-valued function $f:\mathbb{R}_{\geq 0}\rightarrow\mathbb{R}$ satisfying a given linear differential equation have infinitely many zeros? Our main decidability result is that if the differential equation has order at most $7$, then the Infinite Zeros Problem is decidable. On the other hand, we show that a decision procedure for the Infinite Zeros Problem at order $9$ (and above) would entail a major breakthrough in Diophantine Approximation, specifically an algorithm for computing the Lagrange constants of arbitrary real algebraic numbers to arbitrary precision.

eess.SY↗
arXiv2016

Proving the Herman-Protocol Conjecture

Herman's self-stabilisation algorithm, introduced 25 years ago, is a well-studied synchronous randomised protocol for enabling a ring of $N$ processes collectively holding any odd number of tokens to reach a stable state in which a single token remains. Determining the worst-case expected time to stabilisation is the central outstanding open problem about this protocol. It is known that there is a constant $h$ such that any initial configuration has expected stabilisation time at most $h N^2$. Ten years ago, McIver and Morgan established a lower bound of $4/27 \approx 0.148$ for $h$, achieved with three equally-spaced tokens, and conjectured this to be the optimal value of $h$. A series of papers over the last decade gradually reduced the upper bound on $h$, with the present record (achieved in 2014) standing at approximately $0.156$. In this paper, we prove McIver and Morgan's conjecture and establish that $h = 4/27$ is indeed optimal.

cs.DS↗
arXiv2015

Three Variables Suffice for Real-Time Specification

A natural framework for real-time specification is monadic first-order logic over the structure $(\mathbb{R},<,+1)$---the ordered real line with unary $+1$ function. Our main result is that $(\mathbb{R},<,+1)$ has the 3-variable property: every monadic first-order formula with at most 3 free variables is equivalent over this structure to one that uses 3 variables in total. As a corollary we obtain also the 3-variable property for the structure $(\mathbb{R},<,f)$ for any fixed linear function $f:\mathbb{R}\rightarrow\mathbb{R}$. On the other hand, we exhibit a countable dense linear order $(E,<)$ and a bijection $f:E\rightarrow E$ such that $(E,<,f)$ does not have the $k$-variable property for any $k$.

cs.LO↗
arXiv2014

Complexity of Equivalence and Learning for Multiplicity Tree Automata

We consider the complexity of equivalence and learning for multiplicity tree automata, i.e., weighted tree automata over a field. We first show that the equivalence problem is logspace equivalent to polynomial identity testing, the complexity of which is a longstanding open problem. Secondly, we derive lower bounds on the number of queries needed to learn multiplicity tree automata in Angluin's exact learning model, over both arbitrary and fixed fields. Habrard and Oncina (2006) give an exact learning algorithm for multiplicity tree automata, in which the number of queries is proportional to the size of the target automaton and the size of a largest counterexample, represented as a tree, that is returned by the Teacher. However, the smallest tree-counterexample may be exponential in the size of the target automaton. Thus the above algorithm does not run in time polynomial in the size of the target automaton, and has query complexity exponential in the lower bound. Assuming a Teacher that returns minimal DAG representations of counterexamples, we give a new exact learning algorithm whose query complexity is quadratic in the target automaton size, almost matching the lower bound, and improving the best previously-known algorithm by an exponential factor.

cs.LG↗
arXiv2014

On Termination of Integer Linear Loops

A fundamental problem in program verification concerns the termination of simple linear loops of the form x := u ; while Bx >= b do {x := Ax + a} where x is a vector of variables, u, a, and c are integer vectors, and A and B are integer matrices. Assuming the matrix A is diagonalisable, we give a decision procedure for the problem of whether, for all initial integer vectors u, such a loop terminates. The correctness of our algorithm relies on sophisticated tools from algebraic and analytic number theory, Diophantine geometry, and real algebraic geometry. To the best of our knowledge, this is the first substantial advance on a 10-year-old open problem of Tiwari (2004) and Braverman (2006).

cs.CC↗
arXiv2014

The Polyhedron-Hitting Problem

We consider polyhedral versions of Kannan and Lipton's Orbit Problem (STOC '80 and JACM '86)---determining whether a target polyhedron V may be reached from a starting point x under repeated applications of a linear transformation A in an ambient vector space Q^m. In the context of program verification, very similar reachability questions were also considered and left open by Lee and Yannakakis in (STOC '92). We present what amounts to a complete characterisation of the decidability landscape for the Polyhedron-Hitting Problem, expressed as a function of the dimension m of the ambient space, together with the dimension of the polyhedral target V: more precisely, for each pair of dimensions, we either establish decidability, or show hardness for longstanding number-theoretic open problems.

cs.CC↗
arXiv2014

On the Positivity Problem for Simple Linear Recurrence Sequences

Given a linear recurrence sequence (LRS) over the integers, the Positivity Problem} asks whether all terms of the sequence are positive. We show that, for simple LRS (those whose characteristic polynomial has no repeated roots) of order 9 or less, Positivity is decidable, with complexity in the Counting Hierarchy.

cs.DM↗
arXiv2013

Positivity Problems for Low-Order Linear Recurrence Sequences

We consider two decision problems for linear recurrence sequences (LRS) over the integers, namely the Positivity Problem (are all terms of a given LRS positive?) and the Ultimate Positivity Problem} (are all but finitely many terms of a given LRS positive?). We show decidability of both problems for LRS of order 5 or less, with complexity in the Counting Hierarchy for Positivity, and in polynomial time for Ultimate Positivity. Moreover, we show by way of hardness that extending the decidability of either problem to LRS of order 6 would entail major breakthroughs in analytic number theory, more precisely in the field of Diophantine approximation of transcendental numbers.

cs.DM↗
arXiv2013

A Static Analysis Framework for Livelock Freedom in CSP

In a process algebra with hiding and recursion it is possible to create processes which compute internally without ever communicating with their environment. Such processes are said to diverge or livelock. In this paper we show how it is possible to conservatively classify processes as livelock-free through a static analysis of their syntax. In particular, we present a collection of rules, based on the inductive structure of terms, which guarantee livelock-freedom of the denoted process. This gives rise to an algorithm which conservatively flags processes that can potentially livelock. We illustrate our approach by applying both BDD-based and SAT-based implementations of our algorithm to a range of benchmarks, and show that our technique in general substantially outperforms the model checker FDR whilst exhibiting a low rate of inconclusive results.

cs.LO↗