Take the setting of probabilistic Turing machines with nondeterminism. In these machines, the control states are partitioned into the probabilistic and nondeterministic states. Each of these states are associated with finite sets of transitions that can be taken at that state. Probabilistic states associate probability distributions across available transitions at these states. Successors at these states are picked according to this distribution. At nondeterministic states, however, successors are determined by \(\textit{schedulers}\). Schedulers are functions that map finite program histories to decisions at nondeterministic states. Given a machine, they produce execution trees that branch at probabilistic configurations by resolving the nondeterminism in the execution.\(\\\)

Call a transition nondeterministic if it originates at a nondeterministic state. Infinite executions of these programs enable a nondeterministic transition infinitely often if they visit the origin of that transition infinitely often. With a scheduler and an initial state, the unrolled execution of these machines are trees that branch at probabilistic states. For such a machine M, call a scheduler fair if, in all infinite executions it induces, all nondeterministic transitions enabled infinitely often are taken by the scheduler infinitely often.\(\\\)

Consider the decision problem of deciding if a probabilistic nondeterministic Turing machine terminates with probability 1 under all fair schedulers. What is the recursion-theoretic complexity of this problem? Note this this problem is trivially undecidable, and that the corresponding decision problem for non-probabilistic Turing machines is known to be \(\Pi^1_1\)-complete.\(\\\)

Separately, Hoare-style proof systems for reasoning about properties of non-probabilistic programs (written in a Turing-complete language) under fair schedulers have been studied in the 80s. Such proof systems provided rules for deducing the fair termination of these programs that are both sound and complete. Naturally, we ask: what are sound and complete techniques for deducing the fair almost-sure termination of probabilistic programs?

Fix a finite alphabet \(A\). Denote by \(T\) the set of \(A\)-labellings of the complete infinite binary tree, i.e. maps \(\{0,1\}^*\rightarrow A\). Let \(R \subseteq T \times T\) be an (equivalence) relation of such trees. A (binary) tree automaton with \(R\)-constraints consists of a finite state set \(Q\), an initial state \(q_0 \in Q\), and a transition relation \(\Delta\subseteq (Q \times A\times \{R,\neg R\}) \times (Q \times Q)\). A run of a tree automaton on a tree labelling \(\lambda:\{0,1\}^*\rightarrow A\) is a choice of states \(q:\{0,1\}^*\rightarrow Q\) and transitions \(t:\{0,1\}^*\rightarrow \Delta\) for each vertex such that \(q(\epsilon)=q_0\) and \(t(w)=(q(w),\lambda(w),X,q(w0),q(w1))\), where \(X=R\) if the left and right subtree of \(w\) are in \(R\)-relation and \(X=\neg R\) otherwise. A tree automaton accepts a labelling if there is a run for it. This can be extended to different more intricate acceptance conditions (Büchi condition along paths, parity conditions, …). The set of labellings accepted by an automaton is called its language. The following questions might depend to some extent on the nature of the relation \(R\) and should be understood as "for your favourite/interesting \(R\)". \[\\\] Question: Is emptiness/universality decidable for these automata?\(\\\) Question: What are the closure properties for these language classes?

Fijalkow and Horn studied generalised reachability games on graphs, which requires Eve (Player 1) to visit vertices from several different target sets. If all target sets are of size 1, the problem is solvable in PTIME. We are interested in the complexity of determining how many target sets Eve can guarantee to visit, i.e, given an arena, target vertices \(v_1, v_2, \dots, v_n\), and a \(k\leq n\), does Eve have a strategy that ensures at least \(k\) targets are visited? This is known to be in PSPACE and NP-hard. Can we obtain better upper or lower bounds?

Definitions: A temporal graph is a graph where in addition to set of vertices and edges, for each edge, a set of times at which times it can be traversed is specified. Depending on how the edge availability relation is specified, this results in different complexity for different problems. We are interested in the formalism where the edge availability relation is specified, by specifying for every edge, an existential Presburger arithmetic formula with one free variable \(\phi(x)\), such that the edge is available at time \(t\) iff \(\phi(t)\) holds.\(\\\)

A temporal arena is a temporal graph where the set of vertices is partitioned between two opposing players, Adam and Eve. A temporal game is then a temporal arena along with a winning objective for Eve, specifying the winning plays for Eve. The explorability objective requires Eve to visit all vertices of the arena.\(\\\)

Question: Given a temporal arena with edge availability specified using existential Presburger formula, checking if Eve has a winning strategy for the explorability objective is known to be PSPACE-hard (even if all vertices are controlled by Eve) and in EXPTIME. Can we find matching upper or lower bound?

All known algorithms for learning deterministic one clock timed automata (1-DTA) using equivalence and membership queries and without making assumptions on the teacher, require an exponential number of membership queries in the worst case. Prove that it is not possible to do better than that.

A \(d\)-dimesional continuous VASS is a counter system, which consists of a finite set of states and \(d\) counters, each of which can hold a non-negative rational number. A transition of such a machine consists of an integer vector \(\mathbf{v} \in \mathbb{Z}^d\), which allows us to update the counters as follows: Upon taking this transition, we first select some non-zero fraction \(\alpha \in (0,1]\) and then add the vector \(\alpha \cdot \mathbf{v}\) co-ordinate-wise to our current counter values. Since each counter can only hold a non-negative rational number, while adding the vector \(\alpha \cdot \mathbf{v}\), we have to ensure that no counter value becomes negative.\[\]

The reachability problem for continuous VASS is the problem of deciding whether a given source configuration of a continuous VASS can reach a given target configuration. It is known that this problem is NP-complete. When the dimension \(d\) is fixed and all vectors are encoded in binary, it is known that the problem is NL-complete if \(d = 1\) and NP-complete if \(d \ge 2\). However when \(d\) is fixed and all vectors are encoded in unary, the complexity is unknown, which leads to the following question: What is the complexity of reachability in continuous VASS when the dimension \(d\) is fixed?

A (\(d\)-dimensional) Vector Addition System is a set of vectors \(T \subseteq \mathbb Z^d\) and induces a single-step transition relation \(\mathrm\rightarrow\ \subseteq \mathbb N^d \times \mathbb N^d\) by \(\mathbf u \rightarrow \mathbf v \Leftrightarrow \mathbf v = \mathbf u + \mathbf t\) for some \(\mathbf t \in T\). The transitive closure of \(\rightarrow\), \(\rightarrow^*\), is called the reachability relation and for some vector \(\mathbf u \in \mathbb N^d\), we call \(R(\mathbf u) = \{\mathbf v \mid \mathbf u \rightarrow^* \mathbf v\}\) the reachability set of \(\mathbf u\). \(\\\)

The boundedness problem for VAS asks if, given a vector \(\mathbf u\), the set \(R(\mathbf u)\) is finite. It has been long known that the boundedness problem for VAS is EXPSPACE-complete. A more careful analysis reveals an upper bound of \(\mathcal O(n^{2^{d \log d}})\). A similar upper bound for VAS coverability was recently tightened to \(\mathcal O(n^{2^d})\). Can we tighten the upper bound for boundedness too?