Is the reachability problem decidable for reversible data VAS where the set of data values A satisfy the following properties:

1. A is a homogeneous relational structure and has a linear order as one of its relations.
2. The embedding relation on finite substructures of X labelled with natural numbers is a well quasi order.

Some explanations: By saying A is a homogeneous relational structure we mean that any isomorphism between two finite substructures of A can be extended to an automorphism of A.

Examples: Dense linear order, random/Rado graph.

This question comes from the following paper with Sławomir Lasota: [arxiv:2402.17604] (arxiv) [https://doi.org/10.1145/3661814.3662074] (LICS'24 proceedings link).

A regular function is given by a deterministic 2way transducer: a deterministic 2way automaton with outputs. Over the word \(w\in \Sigma^* \) such an automaton has an input tape with content \({\vdash} w {\dashv}\) and can move left and right in a read-only fashion (accepting runs have to end on \(\dashv\)). On every transition an output word in \(\Gamma^*\) is written on a right-only output tape. Such a machine realizes a partial function \(f:\Sigma^*\rightarrow\Gamma^*\), defined on words with an accepting run.

Such a function \(f\) is monotone if for any \(u,v\in\Sigma^*\), if \(u\leq v\) then \(f(u)\leq f(v)\), where \(\leq \) denotes the prefix order.

A sequential 2way transducer is a syntactic restriction of deterministic transducers where no transition is allowed on symbol \(\dashv\). Such a machine necessarily realizes a monotone function since the run over word \(u\) is a prefix of the run over word \(uv\). </p>

Question: Can every monotone regular function be realized by a sequential 2way transducer?

Although quite natural, the problem of deciding if a weighted automaton can be determinized has only been solved in 2022 by Bell & Smertnig [arXiv:2209.02260]. Following this decidability result, it is shown in Benalioua, Lhote & Reynier [arXiv:2307.13505] that one can decide in 2EXPTIME if a weighted automaton over the field of rationals is equivalent to a deterministic one. It is shown in Jecker, Mazowiecki & Purser [arXiv:2310.02204] that determinizability can be decided in PSPACE, when the automata are restricted to polynomial ambiguity.

Question: Can one obtain lower bounds for the decision problem of determinizability of weighted automata over \(\mathbb Q\)?

We aim to model the problem of networked control. Sometimes (e.g., signals at a train junction, a rover on Mars), the systems are operated remotely, but the communication channels may be unreliable. We wish to ensure the specification satisfiability under unreliable channels. To this end, we consider the following game on graphs:

The vertices have no ownership, but the two players player at alternate timesteps. The system has a LTL specification to satisfy on the infinite words generated by the plays. The system player plays remotely and has to send a signal to make a move on the graph. However, the signal could be delayed (with a bound) or lost during the transmission, and the token does not move. Then the environment player makes a move to move the token.

Questions:

1. Does the system have a strategy (with/without memory) to satisfy the specification?
2. If not, identify the minimal set of unsafe edges that should be removed from the graph so that even if the delays and losses occur, the environment may not take an action such that the specification satisfaction becomes impossible.

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?

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.

Starting from finite state automata, one can create a hierarchy of automata models by repeatedly applying one of the following constructions:

• Adding VASS counters (i.e. over \(\mathbb{N}\), without zero tests), and
• Building stacks containing the model.

As a special case, we get, for example:

• \(\mathsf{FSA}\) with \(\mathbb{N}\)-counters \(= \mathsf{VASS}\)
• Stacks over \(\mathsf{FSA}\) \(= \mathsf{PDA}\)
• \(\mathsf{PDA}\) with \(\mathbb{N}\)-counters \(= \mathsf{PVASS}\)

It would be interesting to know whether this hierarchy is proper, or if it collapses at some level.

A first avenue of investigation might be to consider the hierarchy created by building stacks and adding \(\mathbb{Z}\)-counters.