20.12 Succinctness of GFG pushdown automata

By Martin Zimmermann

Valiant showed that the succinctness gap between deterministic and nondeterministic pushdown automata (restricted to deterministic contextfree languages) is nonrecursive, i.e., there is no computable function \(f\) with the following property: If the language of a pushdown automaton \(A\) is deterministic contextfree, then there is a deterministic pushdown automaton of size \(f(|A|)\) recognizing \(L(A)\).

Recently, good-for-games pushdown automata have been introduced, whose expressive power is strictly between the deterministic contextfree and the contextfree languages.

Continue Reading →

20.9 Memory requirements for generalized reachability games

By Antonio Casares

Given a regular language \(L\) (on finite words), we consider the condition over omega-words "having a prefix in \(L\)". We want to characterize the optimal memory requirements for this condition over finite arenas. The memory requirements for the opponent were characterized by Colcombet, Fijalkow and Horn in the 2012 paper "Playing Safe" (that also holds for infinite arenas).

20.8 Good games for good-for-games automata

By Karoliina Lehtinen

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

By Lorenzo Clemente
  • 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

By Vincent Penelle

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

By Chana Weil-Kennedy

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

By Michaël Cadilhac

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\).