This paper concerns decision problems related to finite monoids of rational matrices. We show that determining finiteness of a given finitely presented monoid is in PSpace, improving the known coNExp^NP bound. We also show that the membership problem for finite matrix monoids is PSpace-complete, improving the known NExp-upper bound. Our two complexity results are corollaries of a new polynomial bit-size bound on matrix entries in finite monoids. This is obtained by reduction to the case of matrix groups, using the structure theory of noncommutative algebras and of matrix monoids. Our techniques also give us a polynomial-time algorithm for deciding whether a monoid of rational matrices is conjugate to a monoid of integer matrices.

A rationally dynamically algebraic (RDA) power series is one that arises as (a component of) the solution of a system of differential equations of the form $\boldsymbol{y}' = F(\boldsymbol{y})$, where $F$ is a vector of rational functions that is defined at $\boldsymbol{y}(0)$. RDA power series subsume algebraic power series and are a proper subclass of differentially algebraic power series (those that satisfy a univariate polynomial-differential equation). We give a combinatorial characterisation of RDA power series in terms of exponential generating functions of regular languages of labelled trees. Motivated by this connection, we define the notion of a differential tree automaton. Differential tree automata generalise weighted tree automata by allowing the transition weights to be rational functions of the tree size. Our main result is that the ordinary generating functions of the formal tree series recognised by differential tree automata are exactly the differentially algebraic power series. The proof of this result establishes a general form of recurrence satisfied by the sequence of coefficients of a differentially algebraic power series, generalising Reutenauer's matrix representation of polynomially recursive sequences. As a corollary we obtain a procedure for determining equality of differential tree automata.

It is known how to compute the Zariski closure of a finitely generated monoid of matrices and, more generally, of a set of matrices specified by a regular language. This result was recently used to give a procedure to compute all polynomial invariants of a given affine program. Decidability of the more general problem of computing all polynomial invariants of affine programs with recursive procedure calls remains open. Mathematically speaking, the core challenge is to compute the Zariski closure of a set of matrices defined by a context-free language. In this paper, we approach the problem from two sides: Towards decidability, we give a procedure to compute the Zariski closure of sets of matrices given by one-counter languages (that is, languages accepted by one-dimensional vector addition systems with states and zero tests), a proper subclass of context-free languages. On the other side, we show that the problem becomes undecidable for indexed languages, a natural extension of context-free languages corresponding to nested pushdown automata. One of our main technical tools is a novel adaptation of Simon’s factorization forests to infinite monoids of matrices.

Computational problems concerning the orbit of a point under the action of a matrix group occur throughout computer science, including in program analysis, complexity theory, quantum computation, and automata theory. In many cases the focus extends beyond orbits proper to orbit closures under a suitable topology. Typically one starts from a group and a set of points and asks questions about the orbit closure of the set under the action of the group, e.g., whether two given orbit closures intersect. In this paper we consider a collection of what we call determination problems concerning matrix groups and orbit closures. These problems begin with a given variety and seek to understand whether and how it arises either as an algebraic matrix group or as an orbit closure. The how question asks whether the underlying group is s -generated, meaning it is topologically generated by s matrices for a given number s . Among other applications, problems of this type have recently been studied in the context of synthesising loops subject to certain specified invariants on program variables. Our main result is a polynomial-space procedure that inputs a variety and a number s and determines whether the given variety arises as an orbit closure of a point under an s -generated commutative algebraic matrix group. The main tools in our approach are structural properties of commutative algebraic matrix groups and module theory. We leave open the question of determining whether a variety is an orbit closure of a point under an s -generated algebraic matrix group (without the requirement of commutativity).

We develop a generic reduction procedure for active learning problems. Our approach is inspired by a recent polynomial-time reduction of the exact learning problem for weighted automata over integers to that for weighted automata over rationals (Buna-Marginean et al. 2024). Our procedure improves the efficiency of a category-theoretic automata learning algorithm, and poses new questions about the complexity of its implementation when instantiated to concrete categories.As our second main contribution, we address these complexity aspects in the concrete setting of learning weighted automata over number rings, that is, rings of integers in an algebraic number field. Assuming a full representation of a number ring ${{\mathcal{O}}_K}$, we obtain an exact learning algorithm of ${{\mathcal{O}}_K}$-weighted automata that runs in polynomial time in the size of the target automaton, the logarithm of the length of the longest counterexample, the degree of the number field, and the logarithm of its discriminant. Our algorithm produces an automaton that has at most one more state than the minimal one, and we prove that doing better requires solving the principal ideal problem, for which the best currently known algorithm is in quantum polynomial time.

We study 2-player zero-sum concurrent (i.e., simultaneous move) stochastic Büchi games and Transience games on countable graphs. Two players, Max and Min, seek respectively to maximize and minimize the probability of satisfying the game objective. The Büchi objective is to visit a given set of target states infinitely often. This can be seen as a special case of maximizing the expected lim sup of the daily rewards, where all daily rewards are in {0, 1}. The Transience objective is to visit no state infinitely often, i.e., every finite subset of the states is eventually left forever. Transience can only be met in infinite game graphs.

The automatic generation of loop invariants is a fundamental challenge in software verification. While this task is undecidable in general, it is decidable for certain restricted classes of programs. This work focuses on invariant generation for (branching-free) loops with a single linear update. Our primary contribution is a polynomial-space algorithm that computes the strongest algebraic invariant for simple linear loops, generating all polynomial equations that hold among program variables across all reachable states. The key to achieving our complexity bounds lies in mitigating the blow-up associated with variable elimination and Gröbner basis computation, as seen in prior works. Our procedure runs in polynomial time when the number of program variables is fixed. We examine various applications of our results on invariant generation, focusing on invariant verification and loop synthesis. The invariant verification problem investigates whether a polynomial ideal defining an algebraic set serves as an invariant for a given linear loop. We show that this problem is coNP-complete and lies in PSPACE when the input ideal is given in dense or sparse representations, respectively. In the context of loop synthesis, we aim to construct a loop with an infinite set of reachable states that upholds a specified algebraic property as an invariant. The strong synthesis variant of this problem requires the construction of loops for which the given property is the strongest invariant. In terms of hardness, synthesising loops over integers (or rationals) is as hard as Hilbert’s Tenth problem (or its analogue over the rationals). When the constants of the output are constrained to bit-bounded rational numbers, we demonstrate that loop synthesis and its strong variant are both decidable in PSPACE, and in NP when the number of program variables is fixed.

We introduce the class of P-finite automata. These are a generalisation of weighted automata, in which the weights of transitions can depend polynomially on the length of the input word. P-finite automata can also be viewed as simple tail-recursive programs in which the arguments of recursive calls can non-linearly refer to a variable that counts the number of recursive calls. The nomenclature is motivated by the fact that over a unary alphabet P-finite automata compute so-called P-finite sequences, that is, sequences that satisfy a linear recurrence with polynomial coefficients. Our main result shows that P-finite automata can be learned in polynomial time in Angluin’s MAT exact learning model. This generalises the classical results that deterministic finite automata and weighted automata over a field are respectively polynomial-time learnable in the MAT model.

Hypergeometric sequences are rational-valued sequences that satisfy first-order linear recurrence relations with polynomial coefficients; that is, a hypergeometric sequence is one that satisfies a recurrence of the form f(n)un = g(n)un − 1 where .

In this paper we obtain complexity bounds for computational problems on algebraic power series over several commuting variables. The power series are specified by systems of polynomial equations: a formalism closely related to weighted context-free grammars. We focus on three problems—decide whether a given algebraic series is identically zero, determine whether all but finitely many coefficients are zero, and compute the coefficient of a specific monomial. We relate these questions to well-known computational problems on arithmetic circuits and thereby show that all three problems lie in the counting hierarchy. Our main result improves the best known complexity bound on deciding zeroness of an algebraic series. This problem is known to lie in PSPACE by reduction to the decision problem for the existential fragment of the theory of real closed fields. Here we show that the problem lies in the counting hierarchy by reduction to the problem of computing the degree of a polynomial given by an arithmetic circuit. As a corollary we obtain new complexity bounds on multiplicity equivalence of context-free grammars restricted to a bounded language, language inclusion of a non-deterministic finite automaton in an unambiguous context-free grammar, and language inclusion of a non-deterministic context-free grammar in an unambiguous finite automaton.

We investigate the Membership Problem for hypergeometric sequences: given a hypergeometric sequence ❬un❭∞n=0 of rational numbers and a target t∈Q, decide whether t occurs in the sequence. We show decidability of this problem under the assumption that in the defining recurrence p(n)un = q(n)un-1, the roots of the polynomials p(x) and q(x) are all rational numbers. Our proof relies on bounds on the density of primes in arithmetic progressions. We also observe a relationship between the decidability of the Membership problem (and variants) and the Rohrlich-Lang conjecture in transcendence theory.

We investigate the complexity of computing the Zariski closure of a finitely generated group of matrices. The Zariski closure was previously shown to be computable by Derksen, Jeandel, and Koiran, but the termination argument for their algorithm appears not to yield any complexity bound. In this paper we follow a different approach and obtain a bound on the degree of the polynomials that define the closure. Our bound shows that the closure can be computed in elementary time. We also obtain upper bounds on the length of chains of linear algebraic groups, where all the groups are generated over a fixed number field.

We study the Radical Identity Testing problem (RIT): Given an algebraic circuit representing a polynomial and nonnegative integers a1, …, ak and d1, …, dk, written in binary, test whether the polynomial vanishes at the real radicals , i.e., test whether . We place the problem in coNP assuming the Generalised Riemann Hypothesis (GRH), improving on the straightforward PSPACE upper bound obtained by reduction to the existential theory of reals. Next we consider a restricted version, called 2-RIT, where the radicals are square roots of prime numbers, written in binary. It was known since the work of Chen and Kao [16] that 2-RIT is at least as hard as the polynomial identity testing problem, however no better upper bound than PSPACE was known prior to our work. We show that 2-RIT is in coRP assuming GRH and in coNP unconditionally. Our proof relies on theorems from algebraic and analytic number theory, such as the Chebotarev density theorem and quadratic reciprocity.

We consider Pareto analysis of multi-priced timed automata (MPTA) having multiple observers recording costs (to be minimised) and rewards (to be maximised) along a computation. We study the Pareto Domination Problem, which asks whether it is possible to reach a target location such that the accumulated costs and rewards Pareto dominate a given vector. We show that this problem is undecidable in general, but decidable for MPTA with at most three observers. We show the problem to be PSPACE-complete for MPTA recording only costs or only rewards. We also consider an approximate Pareto Domination that is decidable in exponential time with no restrictions on types and number of observers. We develop connections between MPTA and Diophantine equations. Undecidability of the Pareto Domination Problem is shown by reduction from Hilbert's 10th Problem, while decidability for three observers entails translation to a decidable fragment of arithmetic involving quadratic forms.

International audience

We consider the cyclotomic identity testing (CIT) problem: given a polynomial f(x1,…,xk), decide whether f(ζne1, …,ζnek) is zero, where ζn = e2π i/n is a primitive complex n-th root of unity and e1,…,ek are integers, represented in binary. When f is given by an algebraic circuit, we give a randomized polynomial-time algorithm for CIT assuming the generalised Riemann hypothesis (GRH), and show that the problem is in NP unconditionally. When f is given by a circuit of polynomially bounded degree, we give a randomized NC algorithm. In case f is a linear form we show that the problem lies in NC. Towards understanding when CIT can be solved in deterministic polynomial-time, we consider so-called diagonal depth-3 circuits, i.e., polynomials f ∑mi=1 g+idi, where gi is a linear form and di a positive integer given in unary. We observe that a polynomial-time algorithm for CIT on this class would yield a sub-exponential-time algorithm for polynomial identity testing. However, assuming GRH, we show that if the linear forms gi are all identical then CIT can be solved in polynomial time. Finally, we use our results to give a new proof that equality of compressed strings, i.e., strings presented using context-free grammars, can be decided in randomized NC.

We study a class of reachability problems in weighted graphs with constraints on the accumulated weight of paths. The problems we study can equivalently be formulated in the model of vector addition systems with states (VASS). We consider a version of the vertex-to-vertex reachability problem in which the accumulated weight of a path is required always to be non-negative. This is equivalent to the so-called control-state reachability problem (also called the coverability problem) for 1-dimensional VASS. We show that this problem lies in NC: the class of problems solvable in polylogarithmic parallel time. In our main result we generalise the problem to allow disequality constraints on edges (i.e., we allow edges to be disabled if the accumulated weight is equal to a specific value). We show that in this case the vertex-to-vertex reachability problem is solvable in polynomial time even though a shortest path may have exponential length. In the language of VASS this means that control-state reachability is in polynomial time for 1-dimensional VASS with disequality tests.

We study countably infinite MDPs with parity objectives. Unlike in finite MDPs, optimal strategies need not exist, and may require infinite memory if they do. We provide a complete picture of the exact strategy complexity of $\varepsilon$-optimal strategies (and optimal strategies, where they exist) for all subclasses of parity objectives in the Mostowski hierarchy. Either MD-strategies, Markov strategies, or 1-bit Markov strategies are necessary and sufficient, depending on the number of colors, the branching degree of the MDP, and whether one considers $\varepsilon$-optimal or optimal strategies. In particular, 1-bit Markov strategies are necessary and sufficient for $\varepsilon$-optimal (resp. optimal) strategies for general parity objectives.

Markov decision processes (MDPs) are a standard model for dynamic systems that exhibit both stochastic and nondeterministic behavior. For MDPs with finite state space it is known that for a wide range of objectives there exist optimal strategies that are memoryless and deterministic. In contrast, if the state space is infinite, optimal strategies may not exist, and optimal or ε-optimal strategies may require (possibly infinite) memory. In this paper we consider qualitative objectives: reachability, safety, (co-)Büchi, and other parity objectives. We aim at giving an introduction to a collection of techniques that allow for the construction of strategies with little or no memory in countably infinite MDPs.

Given two labelled Markov decision processes (MDPs), the trace-refinement problem asks whether for all strategies of the first MDP there exists a strategy of the second MDP such that the induced labelled Markov chains are trace-equivalent. We show that this problem is decidable in polynomial time if the second MDP is a Markov chain. The algorithm is based on new results on a particular notion of bisimulation between distributions over the states. However, we show that the general trace-refinement problem is undecidable, even if the first MDP is a Markov chain. Decidability of those problems was stated as open in 2008. We further study the decidability and complexity of the trace-refinement problem provided that the strategies are restricted to be memoryless.

Value iteration is a fundamental algorithm for solving Markov Decision Processes (MDPs). It computes the maximal $n$-step payoff by iterating $n$ times a recurrence equation which is naturally associated to the MDP. At the same time, value iteration provides a policy for the MDP that is optimal on a given finite horizon $n$. In this paper, we settle the computational complexity of value iteration. We show that, given a horizon $n$ in binary and an MDP, computing an optimal policy is EXP-complete, thus resolving an open problem that goes back to the seminal 1987 paper on the complexity of MDPs by Papadimitriou and Tsitsiklis. As a stepping stone, we show that it is EXP-complete to compute the $n$-fold iteration (with $n$ in binary) of a function given by a straight-line program over the integers with $\max$ and $+$ as operators.

We study countably infinite Markov decision processes with Büchi objectives, which ask to visit a given subset F of states infinitely often. A question left open by T.P. Hill in 1979 [Theodore Preston Hill, 1979] is whether there always exist epsilon-optimal Markov strategies, i.e., strategies that base decisions only on the current state and the number of steps taken so far. We provide a negative answer to this question by constructing a non-trivial counterexample. On the other hand, we show that Markov strategies with only 1 bit of extra memory are sufficient.

Register automata (RAs) are finite automata extended with a finite set of registers to store and compare data from an infinite domain. We study the concept of synchronizing data words in RAs: does there exist a data word that sends all states of the RA to a single state? For deterministic RAs with k registers ( k -DRAs), we prove that inputting data words with 2 k +1 distinct data from the infinite data domain is sufficient to synchronize. We show that the synchronization problem for DRAs is in general PSPACE-complete, and it is NLOGSPACE-complete for 1-DRAs. For nondeterministic RAs (NRAs), we show that Ackermann( n ) distinct data (where n is the size of the RA) might be necessary to synchronize. The synchronization problem for NRAs is in general undecidable; however, we establish Ackermann-completeness of the problem for 1-NRAs. Another main result is the NEXPTIME-completeness of the length-bounded synchronization problem for NRAs, where a bound on the length of the synchronizing data word, written in binary, is given. A variant of this last construction allows to prove that the length-bounded universality problem for NRAs is co-NEXPTIME-complete.

International audience

We study countably infinite MDPs with parity objectives, and special cases with a bounded number of colors in the Mostowski hierarchy (including reachability, safety, Büchi and co-Büchi).

We study 2-player turn-based perfect-information stochastic games with countably infinite state space. The players aim at maximizing/minimizing the probability of a given event (i.e., measurable set of infinite plays), such as reachability, Büchi, ω-regular or more general objectives. These games are known to be weakly determined, i.e., they have value. However, strong determinacy of threshold objectives (given by an event ε and a threshold c ∈ [0,1]) was open in many cases: is it always the case that the maximizer or the minimizer has a winning strategy, i.e., one that enforces, against all strategies of the other player, that ε is satisfied with probability ≥ c (resp. <; c)? We show that almost-sure objectives (where c = 1) are strongly determined. This vastly generalizes a previous result on finite games with almost-sure tail objectives. On the other hand we show that ≥ 1/2 (co-)Biichi objectives are not strongly determined, not even if the game is finitely branching. Moreover, for almost-sure reachability and almost-sure Biichi objectives in finitely branching games, we strengthen strong determinacy by showing that one of the players must have a memory less deterministic (MD) winning strategy.

We revisit a fundamental result in real-time verification, namely that the binary reachability relation between configurations of a given timed automaton is definable in linear arithmetic over the integers and reals. In this paper we give a new and simpler proof of this result, building on the well-known reachability analysis of timed automata involving difference bound matrices. Using this new proof, we give an exponential-space procedure for model checking the reachability fragment of the logic parametric TCTL. Finally we show that the latter problem is NEXPTIME-hard.

Nonnegative matrix factorization (NMF) is the problem of decomposing a given nonnegative n × m matrix M into a product of a nonnegative n × d matrix W and a nonnegative d × m matrix H. NMF has a wide variety of applications, including bioinformatics, chemometrics, communication complexity, machine learning, polyhedral combinatorics, among many others. A longstanding open question, posed by Cohen and Rothblum in 1993, is whether every rational matrix M has an NMF with minimal d whose factors W and H are also rational. We answer this question negatively, by exhibiting a matrix M for which W and H require irrational entries. As an application of this result, we show that state minimization of labeled Markov chains can require the introduction of irrational transition probabilities. We complement these irrationality results with an NP- complete version of NMF for which rational numbers suffice.

Nonnegative matrix factorization (NMF) is the problem of decomposing a given nonnegative n*m matrix M into a product of a nonnegative n*d matrix W and a nonnegative d*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.

Register automata (RAs) are finite automata extended with a finite set of registers to store and compare data. We study the concept of synchronizing data words in RAs: Does there exist a data word that sends all states of the RA to a single state? For deterministic RAs with k registers (k-DRAs), we prove that inputting data words with 2k+1 distinct data, from the infinite data domain, is sufficient to synchronize. We show that the synchronizing problem for DRAs is in general PSPACE-complete, and is NLOGSPACE-complete for 1-DRAs. For nondeterministic RAs (NRAs), we show that Ackermann(n) distinct data (where n is the size of RA) might be necessary to synchronize. The synchronizing problem for NRAs is in general undecidable, however, we establish Ackermann-completeness of the problem for 1-NRAs. Our most substantial achievement is proving NEXPTIME-completeness of the length-bounded synchronizing problem in NRAs (length encoded in binary). A variant of this last construction allows to prove that the bounded universality problem in NRAs is co-NEXPTIME-complete.

The problem of synchronizing automata is concerned with the existence of a word that sends all states of the automaton to one and the same state. This problem has classically been studied for complete deterministic finite automata, with the existence problem being NLOGSPACE-complete. In this paper we consider synchronizing-word problems for weighted and timed automata. We consider the synchronization problem in several variants and combinations of these, including deterministic and non-deterministic timed and weighted automata, synchronization to unique location with possibly different clock valuations or accumulated weights, as well as synchronization with a safety condition forbidding the automaton to visit states outside a safety-set during synchronization (e.g. energy constraints). For deterministic weighted automata, the synchronization problem is proven PSPACE-complete under energy constraints, and in 3-EXPSPACE under general safety constraints. For timed automata the synchronization problems are shown to be PSPACE-complete in the deterministic case, and undecidable in the non-deterministic case.