19.17 Existence of a universal amplifier of selection

Moran Birth-death processes are stochastic processes defined as follows. Consider a connected graph \(G\) and a parameter \(r \in \mathbb{R}\) strictly greater than \(1\). We start with a partition of the vertices of \(G\) into two types: mutant vertices, that have fitness \(r\), and resident vertices, that have fitness \(1\). At each step, a random vertex is chosen with probability proportional to its fitness, and spreads its type to an adjacent vertex chosen uniformly at random.

Continue Reading →

19.16 Weak validation of tree-languages by extended automata

The weak validation problem is an open problem stated in 2007 by Segoufin and Sirangelo. The problem is about checking if a regular langage of trees, seen as a languages of word (with an XML encoding), can be validated by a finite automaton with the assumption that the input is a correct tree encoding. More formally, let \(T\) be the set of words encoding correct trees, \(K\) be a regular language of tree with \(\text{XML}(K)\) the associate languages of words. Can we decide if there exists a regular langage of words \(L\) such that \(L\cap T =\text{XML}(K)\).

Continue Reading →

19.15 The busy beaver problem for population protocols

Population protocols are a model of distributed computation by indistinguishable agents, close to VASs. We consider population protocols with one input state. These protocols compute predicates \(\mathbb{N} \rightarrow \{0,1\}\). (For definitions see https://arxiv.org/abs/1801.00742)

For every \(n \geq 1\), let \(f(n)\) be the largest number such that some protocol with at most \(n\) states computes the predicate \(x < f(n)\).

Continue Reading →

19.14 Continuous reachability in ordered data VAS

Data VAS is a finite set of finitely supported functions from ordered data set \(\mathbb{D}\) to \(\mathbb{Z}^k\), where k is a dimension. A configuration/marking is a finitely supported function from \(\mathbb{D}\) to \(\mathbb{N}^k\).

From a configuration \(m\) there is a step to \(m'\) if there is a vector \(x\in \text{VAS}\) and \(\pi\) an ordered preserving bijection (permutation) form \(\mathbb{D}\) to \(\mathbb{D}\) such that \(m+x\circ \pi=m'\). The reachability relation is a transitive closure of the step relation. The reachability problem is undecidable, that is why we are looking for different relaxation of it.

Continue Reading →

19.13 Does a $(\textsf{min,+})$-WA preserve REG by inverse image?

We are interested in functions realized by weighted automata over the semiring \(\mathbb N_{\mathsf{ min}}=\langle \mathbb N\cup\left\{ \infty \right\} , \mathsf{ min}, +, \infty,0\rangle\). An $\mathbb N\mathsf{ min}$-weighted automaton \(\mathcal A\) over alphabet \(\Sigma\) realizes a partial function \(\llbracket \mathcal A \rrbracket:\Sigma^*\rightarrow \mathbb N\). We want to decide given such a function if it preserves ``simple'' sets by inverse image. By simple we mean regular languages (\(\mathbb N\) is viewed a the set of words over a unary alphabet, hence the regular languages are the semilinear sets). Let us state the decision problem.

Continue Reading →

19.12 Reachability for bounded branching VASS

Recall that a $d$-VASS is a finite automaton, where transitions are labelled with $d$-dimensional vectors over integers. A configuration of a $d$-VASS is a pair of a state and a $d$-dimensional vector over naturals. Bounded VASS (BoVASS) are a variant of the classic VASS model where all values in all configurations are upper bounded by a fixed natural number, encoded in binary in the input. It is easy to see that the reachability is in PSPACE for BoVASS and it is not hard to show NP-hardness.

Continue Reading →

19.11 Shortest runs in 3-D VASS

Is there a 3-D VASS with shortest run from source to target, which is longer than exponential? Best lower bound is exponential, best upper bound is tower. The case of VASSes with finite reachability set is probably the core of the problem. In my point this is one of the problems we should attack if we want to push theory of VASSes further.

19.10 Variants of one-counter systems universality

Problem 1:1 Given a 1-VASS, let \(L_n\) be its language where acceptance is by reaching a final state from a fixed initial state and initial counter value \(n\). Does there exist \(n\) such that \(\Sigma^* = L_n\) ?

Problem 2: Given a 1-VASS, let \(L^n\) be the language of the $n$-bounded system (the NFA where values 0..n are hard-coded) where acceptance is by reaching a final state from a fixed initial configuration. Does there exist \(n\) such that \(\Sigma^* \subseteq L^n\)?

Continue Reading →

19.8 Logic and automata for multiply nested-words

Nested-word automata (NWA) are essentially visibly pushdown automata with multiple stacks. They accept languages of (multiply) nested-words, which are words equipped with a fixed number of binary nesting relations, connecting matching push and pop events. In the case of a single stack (that is, a single nesting relation), NWA are equivalent to monadic second-order logic (MSO). The binary predicates used in the logic are the direct successor relation, and the nesting relations. However, in the general case, and even with only two stacks, NWA are not closed under complementation, and strictly less expressive than MSO. In fact, for two stacks, NWA are equivalent to the existential fragment of MSO (EMSO). The equivalence with MSO can be recovered when restricting the set of possible behaviors, one classical example being phase-bounded nested words.

In the general case (more than two stack, arbitrary nested words), the exact expressive power of NWA is not known. In particular, the following question is open: can every first-order formula be translated into an equivalent NWA ?

19.7 Membership in logical classes for (succinct) finite automata

Finite automata can be represented concisely in many way, including enriching their description with bounded-size stacks and registers, by allowing them to be two-way, etc…

Little is known of the complexity of checking membership of those representation of finite automaton into logical formalism (such as LTL, First-Order Logic). Most of the time, classical algorithms relies on testing algebraic properties of the transition semigroup of the automaton. The transition semigroup itself is exponential in the size of the automaton. A straight forward application of those methods to concise representation will lead to tower of exponential algorithms.

For specific kind of concise representations, smarter algorithms could lead to only an exponential blowup.