About Me

Well-structured transition systems (WSTS) are an abstract family of systems that encompasses a vast landscape of infinite-state systems. By requiring a well-quasi-ordering (wqo) on the set of states, a WSTS enables generic algorithms for classic verification tasks such as coverability and termination. However, even for systems that are WSTS like vector addition systems (VAS), the framework is notoriously ill-equipped to analyse reachability (as opposed to coverability). Moreover, some important types of infinite-state systems fall out of WSTS’ scope entirely, such as pushdown systems (PDS). Inspired by recent algorithmic techniques on VAS, we propose an abstract notion of systems where the set of runs is equipped with a wqo and supports amalgamation of runs. We show that it subsumes a large class of infinite-state systems, including (reachability languages of) VAS and PDS, and even all systems from the abstract framework of valence systems, except for those already known to be Turing-complete. Moreover, this abstract setting enables simple and general algorithmic solutions to unboundedness problems, which have received much attention in recent years. We present algorithms for the (i) simultaneous unboundedness problem (which implies computability of downward closures and decidability of separability by piecewise testable languages), (ii) computing priority downward closures, (iii) deciding whether a language is bounded, meaning included in \(w_1^* \cdots w_k^*\) for some words \(w_1, \ldots ,w_k\), and (iv) effective regularity of unary languages. This leads to either drastically simpler proofs or new decidability results for a rich variety of systems.

A recent breakthrough by Künnemann, Mazowiecki, Schütze, Sinclair-Banks, and Węgrzycki (ICALP, 2023) bounds the running time for the coverability problem in \(d\)-dimensional vector addition systems under unary encoding to \(n^{2^{\mathcal{O}(d)}}\), improving on Rackoff’s \(n^{2^{\mathcal{O}(d \log d)}}\) upper bound (Theor. Comput. Sci., 1978), and provides conditional matching lower bounds. In this paper, we revisit Lazić and Schmitz’ “ideal view” of the backward coverability algorithm (Inform. Comput., 2021) in the light of this breakthrough. We show that the controlled strongly monotone descending chains of downwards-closed sets over ℕ\(^d\) that arise from the dual backward coverability algorithm of Lazić and Schmitz on \(d\)-dimensional unary vector addition systems also enjoy this tight \(n^{2^{\mathcal{O}(d)}}\) upper bound on their length, and that this also translates into the same bound on the running time of the backward coverability algorithm. Furthermore, our analysis takes place in a more general setting than that of Lazić and Schmitz, which allows to show the same results and improve on the 2EXPSPACE upper bound derived by Benedikt, Duff, Sharad, and Worrell (LICS, 2017) for the coverability problem in invertible affine nets.

Seminal results establish that the coverability problem for Vector Addition Systems with States (VASS) is in EXPSPACE (Rackoff, ‘78) and is EXPSPACE-hard already under unary encodings (Lipton, ‘76). More precisely, Rosier and Yen later utilise Rackoff’s bounding technique to show that if coverability holds then there is a run of length at most \( n^{2^{\mathcal{O}(d \log d)}} \), where \(d\) is the dimension and \(n\) is the size of the given unary VASS. Earlier, Lipton showed that there exist instances of coverability in d-dimensional unary VASS that are only witnessed by runs of length at least \( n^{2^{Ω(d)}} \). Our first result closes this gap. We improve the upper bound by removing the twice-exponentiated \(\log d\) factor, thus matching Lipton’s lower bound. This closes the corresponding gap for the exact space required to decide coverability. This also yields a deterministic \( n^{2^{\mathcal{O}(d)}} \)-time algorithm for coverability. Our second result is a matching lower bound, that there does not exist a deterministic \(n^{2^{\mathcal{o}(d)}} \)-time algorithm, conditioned upon the Exponential Time Hypothesis. When analysing coverability, a standard proof technique is to consider VASS with bounded counters. Bounded VASS make for an interesting and popular model due to strong connections with timed automata. Withal, we study a natural setting where the counter bound is linear in the size of the VASS. Here the trivial exhaustive search algorithm runs in \( \mathcal{O}(n^{d+1}) \)-time. We give evidence to this being near-optimal. We prove that in dimension one this trivial algorithm is conditionally optimal, by showing that \(n^{2-\mathcal{o}(1)}\)-time is required under the k-cycle hypothesis. In general fixed dimension \(d\), we show that \(n^{d-2-\mathcal{o}(1)}\)-time is required under the 3-uniform hyperclique hypothesis.

We consider a general class of decision problems concerning formal languages, called “(one-dimensional) unboundedness predicates”, for automata that feature reversal-bounded counters (RBCA). We show that each problem in this class reduces – non-deterministically in polynomial time – to the same problem for just finite automata. We also show an analogous reduction for automata that have access to both a pushdown stack and reversal-bounded counters (PRBCA). This allows us to answer several open questions: For example, we show that it is coNP-complete to decide whether a given (P)RBCA language \(L\) is bounded, meaning whether there exist words \(w_1,\ldots,w_n\) with \( L \subseteq w^*_1 \cdots w^*_n \). For PRBCA, even decidability was open. Our methods also show that there is no language of a (P)RBCA of intermediate growth. This means, the number of words of each length grows either polynomially or exponentially. Part of our proof is likely of independent interest: We show that one can translate an RBCA into a machine with \(\mathbb{Z}\)-counters in logarithmic space, while preserving the accepted language.

A pushdown vector addition system with states (PVASS) extends the model of vector addition systems with a pushdown store. A PVASS is said to be bidirected if every transition (pushing/popping a symbol or modifying a counter) has an accompanying opposite transition that reverses the effect. Bidirectedness arises naturally in many models; it can also be seen as a overapproximation of reachability. We show that the reachability problem for bidirected PVASS is decidable in Ackermann time and primitive recursive for any fixed dimension. For the special case of one-dimensional bidirected PVASS, we show reachability is in PSPACE, and in fact in polynomial time if the stack is polynomially bounded. Our results are in contrast to the directed setting, where decidability of reachability is a long-standing open problem already for one dimensional PVASS, and there is a PSPACE-lower bound already for one-dimensional PVASS with bounded stack. The reachability relation in the bidirected (stateless) case is a congruence over \(\mathbb{N}^d\). Our upper bounds exploit saturation techniques over congruences. In particular, we show novel elementary-time constructions of semilinear representations of congruences generated by finitely many vector pairs. In the case of one-dimensional PVASS, we employ a saturation procedure over bounded-size counters. We complement our upper bound with a TOWER-hardness result for arbitrary dimension and \(k\)-EXPSPACE hardness in dimension \(2k+6\) using a technique by Lazić and Totzke to implement iterative exponentiations.

Giving tight estimates for output bounds is key to an accurate network analysis using the stochastic network calculus (SNC) framework. In order to upper bound the delay for a flow of interest in the network, one typically has to calculate output bounds of cross-traffic flows several times. Thus, an improvement in the output bound calculation pays off considerably. In this paper, we propose a new output bound calculation in the SNC framework by making use of Jensen’s inequality. It consists of inserting a convex function \(h\) into the bound, the so-called \(h\)-mitigator. We prove the bound’s validity and also show that, by choosing \(h\) as the power function, that it is always at least as accurate as the state-of-the-art method. Numerical evaluations demonstrate that even in small heterogeneous two-server topologies, our approach can improve a delay bound’s violation probability by a factor of over 135. For a set of randomly generated parameters, the bound is still decreased by a factor of 1.23 on average. Furthermore, our approach can be easily integrated in existing end-to-end analyses. Last but not least, we investigated another variant for \(h\), the exponential function and showed numerically that this approach is mostly disadvantageous

The FAIR control system (CS) is an alarm-based design and employs White Rabbit time synchronization over a GbE network to issue commands executed accurate to 1 ns. In such a network based CS, graphs of possible machine com- mand sequences are specified in advance by physics frame- works. The actual traffic pattern, however, is determined at runtime, depending on interlocks and beam requests from experiments and accelerators. In ’unlucky’ combinations, large packet bursts can delay commands beyond their deadline, potentially causing emergency shutdowns. Thus, prior verification if any possible combination of given command sequences can be delivered on time is vital to guarantee deterministic behavior of the CS. Deterministic network calculus (DNC) can derive upper bounds on message delivery latencies. This paper presents an approach for calculating worst-case descriptors of runtime traffic patterns. These so-called arrival curves are deduced from specified partial traffic sequences and are used to calculate end-to-end traffic properties. With the arrival curves and a DNC model of the FAIR CS network, a worst-case latency for specific packet flows or the whole CS can be obtained.