concurrent system designers

Abstract: Vector addition systems (VAS) are a fundamental model of concurrent computation in which transitions update nonnegative integer counters by adding integer vectors, provided all counters remain nonnegative. Closely related to Petri nets, VAS are the single-state counterpart of vector addition systems with states (VASS), which use finitely many states to restrict the available transitions. A classical simulation of $d$-VASS by $(d+3)$-VAS connects their reachability problems, but the complexity-theoretic picture of fixed-dimensional VAS remains largely unclear. While reachability in $2$-VASS is PSPACE-complete under binary encoding, the best known upper bound for $5$-VAS was only elementary. We prove that every reachable $5$-VAS instance has a reachability witness of length polynomial in its unary size. Consequently, $5$-VAS reachability is NL-complete under unary encoding and PSPACE-complete under binary encoding. We also establish a polynomial factorization of the reachability relation of every $d$-VAS with $d \ge 3$. For $5$-VAS, this strengthens Hopcroft and Pansiot's effective semilinearity of reachability sets to the full reachability relation. For every fixed $d\ge3$, it also yields an $\mathsf F_d$ upper bound for reachability in $(d+3)$-VAS.

Abstract: We investigate the parameterized reachability problem for concurrent register machines over infinite data domains. In this framework, each machine is a program equipped with a set of local registers, the communication across machines is mediated through a set of shared registers. Both local and shared registers can take values from an infinite data domain. The program's primitive operations include copying values between registers, assigning constants, comparing registers for (dis-)equality, and nondeterministic assignments that store an arbitrary domain value into a local register. The parameterized reachability problem considers a program and a target location, asking whether there exists some n in Naturals such that an execution of n identical machines (referred to as instances) results in at least one instance reaching the specified location. We show that this problem is Pspace-complete in the general case and it becomes undecidable if a freshness assumption (i.e., each assignment must produce a unique value distinct from all constants) is applied to nondeterministic assignments. This undecidability persists even for systems restricted to two shared and two local registers. Finally, we establish optimal decidability results for two restricted settings: when each thread is limited to a single local register, or when the system utilizes only one shared register.

Abstract: Concurrent games and strategies based on event structures are an established and expressive model of interactive computation. In this paper we revisit the problem of equipping this model with symmetry. Symmetry is essential for many applications, but it is also a source of mathematical complexity, not least because strategies with symmetry can be compared up to several distinct notions of equivalence. Our first contribution is a complete characterization of two classes of strategies for which composition admits an identity. For these two classes the identity laws hold, respectively, up to a "weak" and a "strong" notion of equivalence. The main result is that the weak class of strategies corresponds precisely to those inducing Street fibrations over the game. We also show how the established "thin" approach to symmetry also fits in this general framework. A second contribution is a formal connection between games and setoid-valued profunctors. This follows a long tradition of relating games and relational models, but here additionally includes a very general model of symmetries. Our characterization of strategies as Street fibrations makes the connection to profunctors significantly easier to establish.

Abstract: Among the different ways of approaching the semantics of process calculi, true-concurrency models stand out for their ability to highlight subtle interplays between events. At their heart lie three crucial relations: concurrency, causality and conflict. This paper shows that reversibility, when endowed with a notion of independence, provides a rich tooling to study and characterise these true-concurrency relations. First, we prove that systems admitting pre-reversibility (i.e., that can be extended with an independence relation satisfying some basic axioms) have a unique notion of independence, events, concurrency, causality and conflict. We then analyse the relationship between independence and the true-concurrency relations, establishing novel independence-based characterisations of causality and conflict. Our second series of contributions revolves around two concrete process calculi and two syntactic notions defined on their transition labels, namely independence and dependence; we prove that they partition connected transitions and characterise elegantly concurrency on adjacent transitions. This part of our development was machine-checked using the proof assistant Beluga. Last, we study how the key mechanism commonly used in reversible process algebra can be used as a proxy to retrieve causality and core independence on past events. We conclude by discussing how our results extend beyond reversible systems.

Abstract: It is an established idea in concurrency theory that every Petri net admits an unfolding semantics. This is a denotational object that represents its domain of possible executions. Unfoldings play an important role in practical analysis and verification. This paper is concerned with the following well-known problem: while the unfolding resembles a universal construction in the category of Petri nets, it generally fails to satisfy the expected universal property. This is because the unfolding construction overlooks the net's internal symmetries. There are two solutions: make these symmetries explicit to obtain a weak universal property (one that holds only ''up to symmetry''); or break the symmetries by assigning individual identities to components of the net. We review these two solutions and establish, in each case, a universal unfolding of Petri nets to event structures. This paper demonstrates a 2-categorical approach to Petri net unfoldings. We show that each unfolding semantics determines a 2-categorical relative adjunction involving Petri nets and event structures. Viewed in this way, the above two constructions can be related formally via an appropriate morphism of adjunctions. We exhibit a 2-density property of event structures which implies that unfolding functors are essentially unique.