ABSTRACT. A probabilistic loop is a programming control flow structure whose  behavior depends on random variables' assignments and probabilistic  conditions. One challenging problem is quantifying automatically the  uncertainty of the probabilistic loop behavior for a potentially unbounded number of iterations. Although this problem is generally highly undecidable, we have explored the necessary restrictions enabling the automated analysis of probabilistic loops without user intervention.  Our symbolic approach leverages algebraic methods and the statistical properties of well-defined probability distributions to derive closed-form expressions of the higher-order statistical moments  for the program's random variables at each loop iteration. In this talk, we demonstrate the application of our methodology through a series of examples.

ABSTRACT. We study the problem of computing the reachable principals of the simulation preorder and the reachable blocks of simulation equivalence. Following a theoretical investigation of this problem, which %, in particular, highlights a sharp contrast with the already settled case of bisimulation, we design algorithms to solve this problem by leveraging the idea of interleaving reachability and simulation computation while possibly avoiding the computation of all the reachable states or the whole simulation preorder. In particular, we put forward a symbolic algorithm processing state partitions and, in turn, relations between their blocks, which is suited for processing infinite-state systems.

ABSTRACT. We present a theory of rewriting a word into a given target language. We show that the natural notion of equivalence between cor- rections as sequences of edit operations can be captured syntactically by means of a rather simple rewrite system. Completeness relies on a normal form for corrections that is then also used to develop a notion of mini- mality for corrections. This is not based on edit distance between words and languages but on a subsequence order on corrections, capturing the intuitive notion of doing a minimal number of rewriting steps. We show that the number of minimal corrections is always finite, and that they are computable for context-free languages.

ABSTRACT. Logically constrained term rewrite systems are useful models of not only sequential but also concurrent programs. We have proposed a framework to soundly reduce starvation freedom of a concurrent program to an all-path reachability problem of the corresponding logically constrained term rewrite system, where process fairness is not considered. In this paper, we show a disproof criterion for starvation freedom and then extend the framework to starvation freedom under process fairness.

ABSTRACT. In this paper we investigate the problem of detecting, counting, and enumerating (generating) all maximum length plateau-$k$-roller\-coasters appearing as a subsequence of some given word (sequence, string), while allowing for plateaus. We define a plateau-$k$-rollercoaster as a word consisting of an alternating sequence of (weakly) increasing and decreasing \emph{runs}, with each run containing at least $k$ \emph{distinct} elements, allowing the run to contain multiple copies of the same symbol consecutively. This differs from previous work, where runs within rollercoasters have been defined only as sequences of distinct values. Here, we are concerned with rollercoasters of \emph{maximum} length embedded in a given word $w$, that is, the longest rollercoasters that are a subsequence of $w$. We present algorithms allowing us to determine the longest plateau-$k$-roller\-coasters appearing as a subsequence in any given word $w$ of length $n$ over an alphabet of size $\sigma$ in $O(n \sigma k)$ time, to count the number of plateau-$k$-roller\-coasters in $w$ of maximum length in $O(n \sigma k)$ time, and to output all of them with $O(n)$ delay after $O(n \sigma k)$ preprocessing. Furthermore, we present an algorithm to determine the longest common plateau-$k$-rollercoaster within a set of words in $O(N k \sigma)$ where $N$ is the product of all word lengths within the set.

ABSTRACT. Given a finite set of matrices with integer entries, the matrix mortality problem asks if there exists a product of these matrices equal to the zero matrix. We consider a special case of this problem where all entries of the matrices are nonnegative. This case is equivalent to the NFA mortality problem, which, given an NFA, asks for a word $w$ such that the image of every state under $w$ is the empty set. The size of the alphabet of the NFA is then equal to the number of matrices in the set. We study the length of shortest such words depending on the size of the alphabet. We show that this length for an NFA with $n$ states can be at least $2^n - 1$, $2^{(n - 4)/2}$ and $2^{(n - 2)/3}$ if the size of the alphabet is, respectively, equal to $n$, three and two.

ABSTRACT. The busy beaver value BB(n) is the maximum number of steps made by any n-state, 2-symbol deterministic halting Turing machine starting on blank tape. The busy beaver function n → BB(n) is uncomputable and, from below, only 4 of its values, BB(1) ... BB(4), are known to date. This leads one to ask: from above, what is the smallest BB value that encodes a major mathematical challenge? Knowing BB(4,888) has been shown by Yedidia and Aaronson [28] to be at least as hard as solving Goldbach’s conjecture, with a subsequent improvement, as yet unpublished, to BB(27) [4,1]. We prove that knowing BB(15) is at least as hard as solving the following Collatz-related conjecture by Erdős, open since 1979 [9]: for all n > 8 there is at least one digit 2 in the base 3 representation of 2^n. We do so by constructing an explicit 15-state, 2-symbol Turing machine that halts if and only if the conjecture is false. This 2-symbol Turing machine simulates a conceptually simpler 5-state, 4-symbol machine which we construct first. This makes, to date, BB(15) the smallest busy beaver value that is related to a natural open problem in mathematics, bringing to light one of the many challenges underlying the quest of knowing busy beaver values.

ABSTRACT. We devise a policy-iteration algorithm for deterministic two-player discounted and mean-payoff games, that runs in polynomial time with high probability, on any input where each payoff is chosen independently from a sufficiently random distribution. This includes the case where an arbitrary set of payoffs has been perturbed by a Gaussian, showing for the first time that deterministic two-player games can be solved efficiently, in the sense of smoothed analysis. More generally, we devise a condition number for deterministic discounted and mean-payoff games, and show that our algorithm runs in time polynomial in this condition number. Our result confirms a previous conjecture of Boros et al., which was claimed as a theorem and later retracted. It stands in contrast with a recent counter-example by Christ and Yannakakis, showing that Howard's policy-iteration algorithm does not run in smoothed polynomial time on stochastic single-player mean-payoff games. Our approach is inspired by the analysis of random optimal assignment instances by Frieze and Sorkin, and the analysis of bias-induced policies for mean-payoff games by Akian, Gaubert and Hochart.

ABSTRACT. A linear constraint loop is specified by a system of linear inequalities that define the relation between the values of the program variables before and after a single execution of the loop body. In this paper we consider the problem of determining whether such a loop terminates, i.e., whether all maximal executions are finite, regardless of how the loop is initialised and how the non-determinism in the loop body is resolved. We focus on the variant of the termination problem in which the loop variables range over $\mathbb{R}$. Our main result is that the termination problem is decidable over the reals in dimension~2. A more abstract formulation of our main result is that it is decidable whether a binary relation on $\mathbb{R}^2$ that is given as a conjunction of linear constraints is well-founded.

ABSTRACT. The computational problem of deciding the winner in two player games on finite graphs with parity and Rabin objectives is a fundamental problem with applications to program verification, and synthesis, and it is closely linked to problems in automata theory and logic.  We focus on understanding the structural properties of these games and devising algorithms that harness these properties.

At the core of these games is the concept of an attractor decomposition, a structured representation of a parity game that serves as a witness of winning for a player and that naturally corresponds to a tree. It has been established that universal trees---trees capable of embedding all possible trees emerging from an input parity game---play a pivotal role in serving as a search space for all known algorithms designed to solve parity games. We survey these techniques and further, we also discuss the extensions to these universal trees that help efficiently solve Rabin games, as well as Strahler universal trees that solve parity games efficiently for certain parameter settings.