Population protocols are a model of distributed computation in which a collection of indistinguishable finite-state agents interact randomly in pairs to decide a predicate of their initial configuration. The agents decide by achieving a stable consensus on whether the predicate holds or not. It is known that population protocols can decide exactly the predicates expressible in Presburger arithmetic. Recently, Lossin et al. have introduced a notion of protocol robustness against adversarial crash failures. They show that all atomic Presburger predicates can be decided by robust protocols, and ask whether the same holds for every Presburger predicate. We make progress towards settling this question by proving that all predicates expressible in monadic Presburger arithmetic have robust protocols. In addition, we analyze the cost of robustness in terms of state complexity. We study the ratio between the number of states of the smallest robust protocol for a given predicate and the smallest protocol for it. We show that the cost of robustness is at least double exponential in the size of the predicate, and prove that the robust protocols by Lossin et al. for threshold predicates x ≥ k have optimal state complexity.

The geometric dimension g of a Vector Addition System with States (VASS) is the dimension of the vector space generated by cycles in the VASS; this parameter refines the standard dimension d, the number of counters. Recently, it was discovered that the fastest-known algorithm for solving the reachability problem for VASS has the same complexity in terms of g as in terms of d. This suggests that the geometric dimension may in fact be a more adequate parameter for measuring the complexity of VASS reachability problems. We initiate a more systematic study of the geometric dimension. We discuss differences between two parameters: the geometric dimension and the SCC dimension. Our main technical result states that classical results about the coverability and boundedness problems can be improved from dimension d to geometric dimension g. Namely, coverability is witnessed by runs of length n^{2^𝒪(g)} instead of n^{2^𝒪(d)}, and unboundedness can be witnessed by runs of length n^{2^𝒪(g log g)} instead of n^{2^𝒪(d log d)}, where n is the size of the instance. We also study integer reachability and simultaneous unboundedness in VASS parameterised by the geometric dimension.

This paper concerns decision problems related to finite monoids of rational matrices. We show that determining finiteness of a given finitely presented monoid is in PSpace, improving the known coNExp^NP bound. We also show that the membership problem for finite matrix monoids is PSpace-complete, improving the known NExp-upper bound. Our two complexity results are corollaries of a new polynomial bit-size bound on matrix entries in finite monoids. This is obtained by reduction to the case of matrix groups, using the structure theory of noncommutative algebras and of matrix monoids. Our techniques also give us a polynomial-time algorithm for deciding whether a monoid of rational matrices is conjugate to a monoid of integer matrices.

We consider a variant of VASS extended with integer counters, denoted VASS+ℤ. These are automata equipped with ℕ- and ℤ-counters; the ℕ-counters are required to remain nonnegative and the ℤ-counters do not have this restriction. We study the complexity of the reachability problem for VASS+ℤ when the number of ℕ-counters is fixed. We show that reachability is NP-complete in 1-VASS+ℤ (i.e. when there is only one ℕ-counter) regardless of unary or binary encoding. For d ≥ 2, using a KLMST-based algorithm, we prove that reachability in d-VASS+ℤ lies in the complexity class ℱ_{d+2}. Our upper bound improves on the naively obtained Ackermannian complexity by simulating the ℤ-counters with ℕ-counters. To complement our upper bounds, we show that extending VASS with integer counters significantly lowers the number of ℕ-counters needed to exhibit hardness. We prove that reachability in unary 2-VASS+ℤ is PSpace-hard; without ℤ-counters this lower bound is only known in dimension 5. We also prove that reachability in unary 3-VASS+ℤ is Tower-hard. Without ℤ-counters, reachability in 3-VASS has elementary complexity and Tower-hardness is only known in dimension 8.

Reachability in pushdown vector addition systems with states (PVASS) is among the longest standing open problems in Theoretical Computer Science. We show that the problem is decidable in full generality. Our decision procedure is similar in spirit to the KLMST algorithm for VASS reachability, but works over objects that support an elaborate form of procedure summarization as known from pushdown reachability.

Vector addition systems with states (VASS), also known as Petri nets, are a popular model of concurrent systems. Many problems from many areas reduce to the reachability problem for VASS, which consists of deciding whether a target configuration of a VASS is reachable from a given initial configuration. In this paper, we obtain an Ackermannian (primitive-recursive in fixed dimension) upper bound for the reachability problem in VASS with nested zero tests. Furthermore, we provide a uniform approach which also allows to decide most related problems, for example semilinearity and separability, in the same complexity. For some of these problems like semilinearity the complexity was unknown even for plain VASS.

Population protocols are a well-studied model of distributed computation in which a group of anonymous finite-state agents communicates via pairwise interactions. Together they decide whether their initial configuration, i. e., the initial distribution of agents in the states, satisfies a property. As an extension in order to express properties of multisets over an infinite data domain, Blondin and Ladouceur (ICALP'23) introduced population protocols with unordered data (PPUD). In PPUD, each agent carries a fixed data value, and the interactions between agents depend on whether their data are equal or not. Blondin and Ladouceur also identified the interesting subclass of immediate observation PPUD (IOPPUD), where in every transition one of the two agents remains passive and does not move, and they characterised its expressive power. We study the decidability and complexity of formally verifying these protocols. The main verification problem for population protocols is well-specification, that is, checking whether the given PPUD computes some function. We show that well-specification is undecidable in general. By contrast, for IOPPUD, we exhibit a large yet natural class of problems, which includes well-specification among other classic problems, and establish that these problems are in ExpSpace. We also provide a lower complexity bound, namely coNExpTime-hardness.

Vector addition systems (VAS), also known as Petri nets, are a popular model of concurrent systems. Many problems from many areas reduce to the reachability problem for VAS, which consists of deciding whether a target configuration of a VAS is reachable from a given initial configuration. One of the main approaches to solve the problem on practical instances is called flattening, intuitively removing nested loops. This technique is known to terminate for semilinear VAS. In this paper, we prove that also for VAS with nested zero tests, called Priority VAS, flattening does in fact terminate for all semilinear reachability relations. Furthermore, we prove that Priority VAS admit semilinear inductive invariants. Both of these results are obtained by defining a well-quasi-order on runs of Priority VAS which has good pumping properties.

Population protocols are a model of computation in which indistinguishable mobile agents interact in pairs to decide a property of their initial configuration. Originally introduced by Angluin et. al. in 2004 with a constant number of states, research nowadays focuses on protocols where the space usage depends on the number of agents. The expressive power of population protocols has so far however only been determined for protocols using $o(\log n)$ states, which compute only semilinear predicates, and for $Ω(n)$ states. This leaves a significant gap, particularly concerning protocols with $Θ(\log n)$ or $Θ(\mathsf{polylog}~ n)$ states, which are the most common constructions in the literature. In this paper we close the gap and prove that for any $ε > 0$ and $f {\in}Ω(\log n) {\cap}O(n^{1-ε})$, both uniform and non-uniform population protocols with $Θ(f(n))$ states can decide exactly those predicates, whose unary encoding lies in $\mathsf{NSPACE}(f(n) \log n)$.

Vector Addition Systems (VAS), aka Petri nets, are a popular model of concurrency. The reachability set of a VAS is the set of configurations reachable from the initial configuration. Leroux has studied the geometric properties of VAS reachability sets, and used them to derive decision procedures for important analysis problems. In this paper we continue the geometric study of reachability sets. We show that every reachability set admits a finite decomposition into disjoint almost hybridlinear sets enjoying nice geometric properties. Further, we prove that the decomposition of the reachability set of a given VAS is effectively computable. As a corollary, we derive a new proof of Hauschildt’s 1990 result showing the decidability of the question whether the reachability set of a given VAS is semilinear. As a second corollary, we prove that the complement of a reachability set, if it is infinite, always contains an infinite linear set.

Esparza and Reiter have recently conducted a systematic comparative study of models of distributed computing consisting of a network of identical finite-state automata that cooperate to decide if the underlying graph of the network satisfies a given property. The study classifies models according to four criteria, and shows that twenty-four initially possible combinations collapse into seven equivalence classes with respect to their decision power, i.e. the properties that the automata of each class can decide. However, Esparza and Reiter only show (proper) inclusions between the classes, and so do not characterise their decision power. In this paper we do so for labelling properties, i.e. properties that depend only on the labels of the nodes, but not on the structure of the graph. In particular, majority (whether more nodes carry label a than b) is a labelling property. Our results show that only one of the seven equivalence classes identified by Esparza and Reiter can decide majority for arbitrary networks. We then study the expressive power of the classes on bounded-degree networks, and show that three classes can. In particular, we present an algorithm for majority that works for all bounded-degree networks under adversarial schedulers, i.e. even if the scheduler must only satisfy that every node makes a move infinitely often, and prove that no such algorithm can work for arbitrary networks.