SAMSA Workshop

Abstract: I will talk about our failed attempt to solve the path equivalence problem (given two systems, do they have the same number of accepting paths for each input word) for any nontrivial extension of finite automata. Although we did not obtain any algorithm we found interesting connections with Laurent polynomials and some mysterious connections with functional analysis, I will show you that.

I believe that this direction of research is an important and fundamental one and should be pursued, but at the moment I have no clue how to attack it.

Abstract: It is well-known that a lot of algorithmic problems for matrix semigroups are undecidable. For example, when given a finitely generated matrix semigroup $S=\{M_1,\ldots,M_k\}$ and a matrix M one could ask whether the given matrix belongs to the generated semigroup, i.e., whether $M\in\langle S\rangle$ holds or not? The undecidability results in the literature tend to utilise embeddings from $\{a,b\}^*\times\{a,b\}^*$ into the desired matrix semigroup whilst ensuring that the structural constraints of the semigroup are preserved. In this talk, I will give a brief overview of some existence and non-existence results for embeddings and show how a non-standard embedding can lead to an undecidability result where a Turing machine is simulated using matrices.

Abstract: There is a number of important combinatorial matrix classes such as indecomposable matrices, primitive matrices, scrambling matrices, chainable matrices, etc., that are useful both in fundamental investigations and in applications. The central approach to study these classes is via certain their numerical invariants. To list a few of them, we mention matrix exponent, scrambling index and solidarity index.

In the talk we give a short exposition of these notions and their applications to the theory of non-negative matrix semigroups and theory of finite automata.

We illustrate the importance of this approach by presenting several recent results related to the extensions of classical results due to Perron, Frobenius and Wielandt to matrix semigroups. This is a joint work with Yu.A. Alpin, A.M. Maksaev, E.R. Shafeev.

Abstract: For an alphabet $\Sigma$, a formal power series over a semiring $R$ is a function $f: \Sigma^* \to R$. Weighted automata over $R$ are used to recognize such series. The well-known Fliess' theorem states that when $R$ is a field, the minimal automaton recognizing $f$ has a size equal to the rank of its associated Hankel matrix $H_f$. Given a weighted automaton over $R$ recognizing a formal power series $f$, and a subsemiring $S$ of $R$, we investigate the question of whether $f$ is also rational over $S$. This means determining if there exists a weighted automaton with entries in $S$ that also recognizes $f$, under the promise that the image of $f$ is contained within $S$, i.e., $f(\Sigma^*) \subseteq S$.

In this talk, we primarily consider the cases when $R = \mathbb{R}$ is the real field and $S = \mathbb{R}_{\geq 0}$ is the set of non-negative reals. We discuss the challenges and adaptations involved in relating the size of weighted automata over $\mathbb{R}_{\geq 0}$ to specific factorizations of the Hankel matrix, such as non-negative and residual factorizations. We will discuss some failed attempts to solve this problem and some open questions.

Abstract: The linear hull (LH) of a weighted automaton (WA) is an invariant, recently introduced by [Bell & Smertnig, 2021], that allows to decide the unambiguity or sequentiality of WA over a field. We showed in [Benalioua, Lhote & Reynier, 2024] that the LH of a WA can be used to solve the register minimization problem for cost register automata (CRA) and gave a 2EXPTIME procedure for its computation. However, the question of the tightness of this complexity bound remains open. In this talk, I will present the idea underlying this procedure, how it relates to minimization problems for CRA and I will show how its complexity is linked to bounding the number of irreducible components of the linear Zariski closure of a finitely generated group of matrices.
If time permits, I will also mention how those results generalize to weighted tree automata and the challenges faced in this setting.

Abstract: A weighted finite automata (WFA) is called residual if the cone generated by the rows of its Hankel matrix is finitely generated. Residual WFAs are better behaved than WFAs in general. For example, they admit unique conical basis as a consequence of which they are learnable. They are closed under reversal, as a consequence of which non-negativity of residual WFAs is decidable. The questions we are interested in are whether residuality is a decidable property, and whether positivity of residual automata can be decided.

Abstract: The family of semilinear sets admits several equivalent characterisations: sets definable in Presburger arithmetic, rational subsets of the monoid (N^d, +), Parikh images of regular languages. This notion can be generalised to data vectors, where coordinates are indexed by an orbit-finite set. However, in this extended setting, the classical equivalences break down. For instance, semilinear sets of data vectors form a strict subset of the family of rational sets of data vectors. The latter are conjectured to coincide with the Parikh images of languages recognised by register automata. These families remain poorly understood and continue to offer a rich source of open problems.

Abstract: Whilst N^2 is an infinite set, under bijective renamings it only consists of two orbits: the pairs with distinct entries, and those with the same entry repeated twice. As such N^2 is an orbit-finite set; in turn, the vector space with basis N^2 can be called orbit-finite-dimensional. I will show such spaces have finite length, so language equivalence for weighted register automata is decidable over many infinite alphabets. This extends the work of Bojańczyk, Fijalkow, Klin, and Moerman [LICS’21/TheoretiCS’24].

Abstract: In this talk, I will define safe and live languages and present safety-liveness decompositions. The content of this talk is mostly folklore, but it might also include results from:

• B. Alpern, F.B. Schneider: Defining liveness, Inf. Process. Lett., 1985
• T. Henzinger, N. Mazzocchi and N.E. Saraç: Quantitative Safety and Liveness, FoSSaCS, 2023

Abstract: The complexity of the reachability problem in Vector Addition Systems with States (VASSs) remained an open question for several decades. Although the problem was eventually shown to be Ackermann-complete, many fundamental questions about VASSs are still unresolved. In fact, even the reachability problem itself is not yet fully understood. A key indication of this is the presence of significant complexity gaps for low-dimensional cases.

In this talk, I will briefly outline the current state of the art regarding the reachability problem in low-dimensional VASSs and discuss possible future research directions. The main focus will be on identifying where existing techniques fall short and why current complexity bounds remain unimproved.

Abstract: The first and best-known algorithm for the reachability problem in Vector Addition Systems (VAS) is a decomposition developed by Mayr in 1981, later simplified by Kosaraju and Lambert. In 2011, Leroux introduced a completely different approach. He showed that non-reachability can be certified by semilinear inductive invariants: if a target configuration is unreachable from the initial one, then there exists a semilinear set containing the initial configuration, closed under the VAS transitions, and excluding the target. As a consequence, VAS reachability can be decided by two semi-algorithms: one that enumerates runs, and one that searches through semilinear sets for such invariants.

Leroux’s construction of inductive invariants proceeds by alternately expanding two semilinear sets, which we refer to as the Source and the Trap, ensuring that no configuration in the Source can reach any configuration in the Trap. These sets are initially the singleton sets containing the initial and target configurations, respectively. To expand the Trap, one overapproximates the forward reachability set of the Source by a semilinear set, and adds its complement to the Trap. Symmetrically, the Source is expanded by adding the complement of a semilinear overapproximation of the Trap's backward reachability set. Once the Source and Trap become complements of each other, the Source is an inductive invariant.

This symmetric construction offers little insight into the structure of the resulting invariant. For instance, it does not guarantee that the invariant is periodic when the VAS itself is periodic. Moreover, the approach does not seem to generalize to Branching VAS, an asymetric extension of VAS where transitions may have multiple source configurations.

In this talk, I present a new, purely forward construction of inductive invariants for VAS, developed with Jérôme Leroux and Grégoire Sutre. We believe this construction constitutes a step toward decidability of reachability in Branching VAS.

Abstract: Timed automata are a widely studied model of real-time systems that extend classical finite state-automata with real-valued variables, called clocks, that evolve with derivative one and which can be queried and reset along transitions. Multi-Priced Timed Automata (MPTA) further extend timed automata with write-only variables, called observers, that have a non-negative slope that can change from one location to another. We consider the domination problem: given an MPTA and a target t, is there a run on the automata such that the value of the run is less than t pointwise? This is known to be undecidable if negative rates are allowed.

We introduce a variant of this problem by introducing a slack parameter. This allows us to transfer the problem to a Diophantine problem. While we show that this problem is still undecidable, we show decidability in the bounded case, through methods from Diophantine approximation and the geometry of numbers. In this talk, I will focus on Diophantine Approximation methods that are not in the paper, but may be able to be translated back into results on MPTA.

Abstract: Take as inputs a rational-valued recurrence sequence and a rational target, the Membership Problem asks to procedurally determine whether the specified target is a term in the input sequence. In this talk we will restrict our attention to hypergeometric sequences (the class of sequences that obey a first-order linear recurrence relation with polynomial coefficients). In this talk, we will discuss both the difficulty with settling decidability and survey results in this setting. Time permitting, we will outline the approaches in recent works as well as directions for future work.

Results surveyed in this talk are taken from collaborations with J. Konieczny, F. Luca, K. Nosan, A. Scoones, M. Shirmohammadi, and J. Worrell.

Abstract: The Skolem Problem asks whether a given linear recurrence sequence has a zero term. Decidability of this problem has famously been open for over 90 years. Special cases are known - in particular for sequences of order at most 4. By following the proof it is easy to determine that the complexity of the Skolem Problem for such sequences is in NP^{RP}. To date, this is the best known complexity upper bound.

In the talk I will discuss a soon-to-be submitted result showing the Skolem Problem at order 4 is in coRP, and directions for improvements.

Abstract: Guided by the question “What polynomial invariants can loops with linear updates have?”, we are desperately searching for methods of proving that certain d-variate polynomials cannot be loop invariants of any non-trivial linear loop with d variables. A linear loop is described by (A, x) where A is a square matrix of size d and x is a vector of size d, both having rational entries. A polynomial invariant P is a polynomial in d variables such that P vanishes on each A^nx.

Abstract: We study the algorithmic comparison of two labelled MDPs whether there exist strategies such that the MDPs become (in)equivalent in terms of trace equivalence. We provide the first polynomial-time algorithms for computing strategies to make the two labelled MDPs inequivalent if such strategies exist. This is joint work with Stefan Kiefer.

Abstract: I will describe a model of computation, which describes functions that input strings, and output elements from some domain, such as the Booleans, or strings, or a field. The idea is that there are two parties, Alice and Bob, who cooperate to compute the output of the function. For a given input string, an adversary chooses a partition w=w1w2, and sends the words w1 and w2 to Alice and Bob, respectively. Alice and Bob then exchange a constant number of messages, using some operations in the output domain, in a way that results in the output of the function. We will show that for various output domains, the model coincides with standard notions. In particular, for Boolean outputs, it gives regular languages, and for outputs in a field, it gives weighted automata. Joint work with Aliaume Lopez, Rafał Stefański, and Omid Yaghoubi.