20.8 Good games for good-for-games automata

Given an automaton \(A\), consider the following two games:

Game I. At each turn \(i\):

  • Adam plays a letter \(a_i\)
  • Eve plays a transition \(r_i\) over \(a_i\)

A play is the infinite word \(w=a_0a_1\ldots\) and the sequence of transitions \(r=r_0r_1\ldots\) Eve wins if either \(w\) is not in \(L(A)\) or \(r\) is an accepting run over \(w\) in \(A\).

Game II. At each turn turn \(i\):

  • Adam plays a letter \(a_i\)
  • Eve plays a transition \(r_i\) over \(a_i\)
  • Adam plays a pair of transitions \(s_i\) and \(t_i\)

A play is the triple of sequences of runs \(r=r_0r_1\ldots, s=s_0s_1\ldots\) and \(t=t_0t_1\ldots\) Eve wins if either \(r\) is an accepting run of \(A\) or both \(s\) and \(t\) are not accepting runs of \(A\).

Continue Reading →

20.2 Deterministic separability of nondeterministic timed languages

  • Input: two timed languages \(L\), \(M\) represented as nondeterministic timed automata.
  • Question: decide whether there exists a deterministic timed automaton recognising a timed language \(S\) which separates \(L\), \(M\), in the sense that \(L\) is included in \(S\) and \(S\) is disjoint from \(M\).

The version of the problem when we fix in advance the number of clocks of the separating deterministic timed automaton is decidable. The open problem is then when the number of clocks is not fixed (and thus quantified existentially).

20.5 Regular antichain subset of the iteration of a regular language

This problem comes from a typing problem (non structural subtype assignment).

Given a regular language R, does there exist a regular language U such that:

  • U is an antichain for the prefix ordering
  • \(\forall u \in U, \exists r \in R, r < u < r^\omega\)
  • \(\exists u \in U, r \in R, r < u < r^\omega \wedge |r^{-1}u| > ||U||\)

where \(||U||\) is the number of states of the minimal automaton recognizing \(U\), and \(r^\omega\) is the infinite iteration of \(r\).

I conjecture that such language does not exist, though I don't find an approach to attack it. If such a language does exist, it would be interesting to know if there can be an infinite number of words such that the third point holds or not.

20.6 Branching Immediate Observation nets

Branching Immediate Observation (BIO) nets are a subclass of Petri nets defined by their transitions, which are of the form \(|{}^\bullet t - t^{\bullet}| \le 1\). This multiset subtraction means that all input places of \(t\) with arc weight \(k\) are also output places of \(t\) with arc weight \(k\), except for one which may have input arc weight \(k\) and output arc weight \(k-1\). BIO nets generalize Basic Parallel Processes (BPP) nets and Immediate Observation (IO) nets - a token can “branch” into any number of tokens as in BPP, but may need to “observe” that another token is in a certain place to proceed with its transition as in IO.

Continue Reading →

20.7 Equivalence of Cost Register Automata: the quest for decidability

Consider the model introduced in this problem. It is mentioned therein that equivalence is undecidable for that model. We ask what further restrictions we can impose on that model to make equivalence decidable.

If the \(\min\) operation is removed, then this is known to lead to decidability [Alur et al.'13]. But as soon as we have \(\min\), we don't know of a model with decidable equivalence.

We conjecture that it is decidable is the CRA is ordered; this means that the registers can be ordered, say \(x_1, x_2, \ldots, x_n\), such that for all updates, \(x_i\) is only updated with registers \(x_j\) for \(j \geq i\).

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 →