We consider the reachability problem for one-counter automata. In this model, we have a finite set of states and a single counter with values over the natural numbers. Each transition can change the current state of the automaton as well as increment or decrement the current value of the counter by some number, encoded in binary. The reachability problem for this model is known to be NP-complete. However, the exact running time of the best possible deterministic algorithm for this problem is unknown.

Similar to the theory of NP-completeness which lets us prove that various problems do not admit polynomial-time algorithms under some plausible assumptions, in recent years, a theory of fine-grained complexity has emerged which lets us pinpoint the exact running time of various problems under plausible hypotheses. It would be interesting to see the applicability of techniques from this field for the reachability problem for one-counter automata.

By \(\le\) we denote the (scattered) subsequence relation between words. Example: \(aba \le baabbabbb\). Fix a finite alphabet \(A\). Let \(X\) be a set of string variables. A subsequence constraint is an expression of the form \(x \le \alpha \) where \(x \in X\) and \(\alpha \in X^*\). A homomorphism \(h: X^\ast \to A^*\) satisfies a subsequence constraint \(x \le \alpha \) if \(h(x) \le h(\alpha)\). A domain restriction constraint \(d: X \to RE(A)\) restricts the domain of possible values for a variable \(x\) to the regular language given by the regular expression \(d(e)\). We are interested in the decidability of the following problem:

Input: A set \(C\) of subsequence constraints and a domain restriction \(d\). Question:Is there a homomorphism \(h\) that respects the domain restriction \(d\) and satisfies every subsequence constraint in \(C\)?

A VASS of dimension \(d\) is an automaton where the transitions from states to states are given with a vector \(\bar{v}\in\mathbb{Z}^d\), meant to be added coordinate-wise to the current counter. A transition can only be taken if it keeps each coordinate non-negative. A language of words can either be recognised by reachability (one reads the word from an initial configuration \(\langle q_0,\bar{v}_0\rangle\) to a final one) or by coverability (one reads the word from an initial configuration to any configuration \(\langle q,\bar{v}\rangle\) which dominates coordinate-wise a specified one).

We would like to investigate the following class of problems, for F being a class of regular languages: is the language recognised by a given VASS in F?

In most cases, the problem is undecidable, but for different reasons, depending on how the VASS is recognised. If the VASS is recognised by reachability, the problem is undecidable as soon as the formalism F admits some very basic closure properties, hence there is little hope for obtaining anything interesting. However, if the VASS is recognised by coverability, then the problem is undecidable as soon as the class F contains LT (for Locally Testable), the class of languages definable in terms of prefixes, infixes, and suffixes. This leaves the problem open for F being for instance the well-studied class FO2 (First-Order Logic with two variables), or PTL (the class of languages being peacewise testable, meaning which are defined in terms of subwords).

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.

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

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

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?