Deterministic Suffix-reading Automata (DSA) are a model of automata over finite words introduced recently. DSAs are able to represent regular languages more succinctly than conventional DFAs.

Transitions in a DSA are labeled with words. From a state, a DSA triggers an outgoing transition on seeing a word ending with the transition's label. Therefore, rather than moving along an input word letter by letter, a DSA can jump along blocks of letters, with each block ending in a suitable suffix. This enables DSAs to represent regular languages more concisely.

This is a very recent model with plenty of open questions. Here is one concrete question: given a DSA, is it minimal?

For DFAs, this question can be answered by identifying a distinguishing string for every pair of states, thanks to the Myhill-Nerode theorem. No such characterization is known in the DSA setting.

Timed automata are finite-state automata extended with finite real-valued variables called clocks. Timed automata with additive constraints are timed automata extended with atomic clock constraints of the form \[x + y \sim c\] where x and y are clocks, and c is a constant.

The emptiness-checking problem for Timed automata with additive constraints was shown to be undecidable with only 4 clocks, while it is decidable for 2 clocks [Beìrard Duford '00]. However the case of 3 clocks was left open in the paper.

Question: Is the emptiness-checking decidable for timed automata with additive constraints for 3 clocks?

Weighted timed games (WTGs for short) are two-player zero-sum games played in a timed automaton equipped with integer weights into transitions and locations. In a turn-based fashion, the current player chooses the next delay and transition. We consider optimal reachability objectives, in which one of the players, whom we call Min, wants to reach a target location while minimising the cumulated weight given by the sequence of transitions firing and the time spent in each location. Its opponent, called Max, has the opposite objective, i.e. avoids the target or maximises the accumulated weight needed to reach the target.

This allows one to define the value of a WTG as the minimal weight Min can guarantee whatever Max does. In a WTG, the value for a given location is a function according to the valuation of the clocks when the first player starts to play.

While knowing if Min has a strategy to guarantee the value lower than a given threshold is known to be undecidable (with two or more clocks), several conditions, one of them being the divergence or one-clock WTGs have been given to recover decidability. Decidability proof relies on the properties of the value: it is a piecewise affine function characterise as a fixpoint of a operator that locally chooses the best option for each player.

I propose to study this function for all WTGs: for which class of WTGs, the value function is continuous and/or a fixed point of the local operator? In particular, I propose to start with WTGs that only use non-negative weights.

Problem A: Given a deterministic one-counter automaton (a pushdown automaton with one stack alphabet) \(A\) and a nondeterministic one-counter net (a one-counter automaton with no zero-tests) \(N\), decide if the language recognised by $A$ is the same as the language recognised by \(N\).

Decidability of A is open. This is related to the open question of decidability for the following problem, which is relatively more well-known.

Problem B: Given a deterministic one-counter net \(D\) and a nondeterministic one-counter net \(N\), decide if the language recognised by \(D\) is the same as the language recognised by \(N\).

Petri nets with ordered data is an extension of Petri nets where tokens carry values from the set of rational numbers \(\mathbb{Q}\), and executability of transitions is conditioned by inequalities between data values. More precisely, every arc is labeled by a finite number of variables corresponding to the data values of tokens, and every transition is labeled by a first-order formula over a signature \(\{\leq\}\), where variables are from incident arcs. Data values of tokens produced and consumed by a transition must satisfy that formula. A configuration (marking) of a Petri net is a function that assigns to every place a finite multiset of rational numbers (data values carried by the tokens on this place). A configuration \(q'\) is reachable from a configuration \(q\) if there is a sequence of transition firings that leads from \(q\) to \(q'\).

Question: Is the following problem decidable?

• Input: a Petri net with ordered data and its two configurations \(q, q'\).
• Question: is \(q\) reachable from \(q'\) and \(q'\) reachable from \(q\)?

We consider multi-player infinite duration games on graphs. A game is given by a directed graph, with vertices partitioned in $k$ sets; Player $i$ controls vertices in the ith set. Edges are coloured with colours in a set $C$, and each player has an objective $W_i \subseteq C^\omega$. A strategy profile is an array of $k$ strategies, $\bar{\sigma} = (\sigma_1,\dots, \sigma_k)$, one for each player. It is a Nash equilibrium if no player has an incentive to change their strategy, that is: If $\bar{\sigma}$ produces a losing outcome for Player $i$, then Player $i$ cannot modify his strategy and obtain a winning outcome.

It is known that, under some mild hypothesis on the objectives $W_i$, every game admits some Nash equilibrium. The proofs for this fact usually build a NE where strategies use infinite memory, even for games with very simple objectives.

Question: Do all reachability/Büchi/parity games admit a Nash equilibrium in which all strategies are positional?

A 1-dimensional Vector Addition System with States (1-VASS) can be seen as an directed and integer weighted graph that is equipped with a non-negative integer counter. A configuration of a 1-VASS is a pair \((q, x)\) that is the current node \(q\) and the current non-negative counter value \(x\). A run in a 1-VASS is a sequence of configurations \((q_0, x_0), (q_1, x_1), \ldots, (q_k, x_k)\) where for each \(i \in \{ 1, \ldots, k\}\), there is an edge from \(x_{i-1}\) to \(x_i\) with weight \(x_i - x_{i-1}\). Let \(n\) the size of a 1-VASS, encoded in unary, that is the number of states plus the absolute value of all weights. The coverability problem asks whether there is a run from \((p, 0)\) to \((q, x)\) in \(\mathcal{V}\), where \(x \geq 0\); the input consists of a 1-VASS \(\mathcal{V}\), an initial state \(p\), and a target state \(q\). There is a straightforward \(\mathcal{O}(n^2)\)-time algorithm for coverability in 1-VASS.

Is there an \(o(n^2)\)-time algorithm for coverability in 1-VASS?