Abstract. A temporal graph is a graph whose edges appear only at certain points in time. Recently, the second and the last three authors proposed a natural temporal analog of the Erdős–Rényi random graph model. The proposed model is obtained by randomly permuting the edges of an Erdős–Rényi random graph and interpreting this permutation as an ordering of presence times. It was shown that the connectivity threshold in the Erdős–Rényi model fans out into multiple phase transitions for several distinct notions of reachability in the temporal setting. In the present paper, we identify a sharp threshold for the emergence of a giant temporally connected component. We show that at [Formula: see text] the size of the largest temporally connected component increases from [Formula: see text] to [Formula: see text]. This threshold holds for both open and closed connected components, i.e., components that allow (respectively, forbid) their connecting paths to use external nodes.

We study a new version of the Euclidean TSP called VectorTSP (VTSP for short) where a mobile entity is allowed to move according to a set of physical constraints inspired from the pen-and-pencil game Racetrack (also known as Vector Racer ). In contrast to other versions of TSP accounting for physical constraints, such as Dubins TSP, the spirit of this model is that (1) no speed limitations apply, and (2) inertia depends on the current velocity. As such, this model is closer to typical models considered in path planning problems, although applied here to the visit of n cities in a non-predetermined order. We motivate and introduce the VectorTSP problem, discussing fundamental differences with previous versions of TSP. In particular, an optimal visit order for ETSP may not be optimal for VTSP. We show that VectorTSP is NP-hard, and in the other direction, that VectorTSP reduces to GroupTSP in polynomial time (although with a significant blow-up in size). On the algorithmic side, we formulate the search for a solution as an interactive scheme between a high-level algorithm and a trajectory oracle, the former being responsible for computing the visit order and the latter for computing the cost (or the trajectory) for a given visit order. We present algorithms for both, and we demonstrate and quantify through experiments that this approach frequently finds a better solution than the optimal trajectory realizing an optimal ETSP tour, which legitimates the problem itself and (we hope) motivates further algorithmic developments.

Regular model checking is a technique for the verification of infinite-state systems whose configurations can be represented as finite words over a suitable alphabet. The form we are studying applies to systems whose set of initial configurations is regular, and whose transition relation is captured by a length-preserving transducer. To verify safety properties, regular model checking iteratively computes automata recognizing increasingly larger regular sets of reachable configurations, and checks if they contain unsafe configurations. Since this procedure often does not terminate, acceleration, abstraction, and widening techniques have been developed to compute a regular superset of the reachable configurations. In this paper, we develop a complementary procedure. Instead of approaching the set of reachable configurations from below, we start with the set of all configurations and approach it from above. We use that the set of reachable configurations is equal to the intersection of all inductive invariants of the system. Since this intersection is non-regular in general, we introduce b-invariants, defined as those representable by CNF-formulas with at most b clauses. We prove that, for every $b\geq0$, the intersection of all inductive b-invariants is regular, and we construct an automaton recognizing it. We show that whether this automaton accepts some unsafe configuration is in EXPSPACE for every $b\geq0$, and PSPACE-complete for b=1. Finally, we study how large must b be to prove safety properties of a number of benchmarks.

Abstract. A graph whose edges only appear at certain points in time is called a temporal graph (among other names). Such a graph is temporally connected if each ordered pair of vertices is connected by a path which traverses edges in chronological order (i.e., a temporal path). In this paper, we consider a simple model of random temporal graph, obtained from an Erdős–Rényi random graph, [Formula: see text], by considering a random permutation [Formula: see text] of the edges and interpreting the ranks in [Formula: see text] as presence times. We give a thorough study of the temporal connectivity of such graphs and derive implications for the existence of several kinds of sparse spanners. It turns out that temporal reachability in this model exhibits a surprisingly regular sequence of thresholds. In particular, we show that at [Formula: see text], any fixed pair of vertices can asymptotically almost surely (a.a.s.) reach each other; at [Formula: see text], at least one vertex (and, in fact, any fixed vertex) can a.a.s. reach all others; and at [Formula: see text], all the vertices can a.a.s. reach each other; i.e., the graph is temporally connected. Furthermore, the graph admits a temporal spanner of size [Formula: see text] as soon as it becomes temporally connected, which is nearly optimal, as [Formula: see text] is a lower bound. This result is quite significant because temporal graphs do not admit spanners of size [Formula: see text] in general [Kempe, Kleinberg, and Kumar, J. Comput. System Sci., 64 (2002), pp. 820–842]. In fact, they do not even always admit spanners of size [Formula: see text] [Axiotis and Fotakis, On the size and the approximability of minimum temporally connected subgraphs, 2016, pp. 149:1–149:14]. Thus, our result implies that the obstructions found in these works—and more generally any non-negligible obstruction—are statistically insignificant: nearly optimal spanners always exist in random temporal graphs. All the above thresholds are sharp. Carrying the study of temporal spanners a step further, we show that pivotal spanners—i.e., spanners of size [Formula: see text] composed of two spanning trees glued at a single vertex (one descending in time, the other ascending subsequently)—exist a.a.s. at [Formula: see text], this threshold being also sharp. Finally, we show that optimal spanners (of size [Formula: see text]) also exist a.a.s. at [Formula: see text]. Whether this value is a sharp threshold is open; we conjecture that it is. For completeness, we compare the above results to existing results in related areas, including edge-ordered graphs, gossip theory, and population protocols, showing that our results can be interpreted in these settings as well and that in some cases they improve known results therein. Finally, we discuss an intriguing connection between our results and Janson’s celebrated results on percolation in weighted graphs.

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.

In rendez-vous protocols an arbitrarily large number of indistinguishable finite-state agents interact in pairs. The cut-off problem asks if there exists a number $B$ such that all initial configurations of the protocol with at least $B$ agents in a given initial state can reach a final configuration with all agents in a given final state. In a recent paper (Horn and Sangnier, CONCUR 2020), Horn and Sangnier proved that the cut-off problem is decidable (and at least as hard as the Petri net reachability problem) for protocols with a leader, and in EXPSPACE for leaderless protocols. Further, for the special class of symmetric protocols they reduce these bounds to PSPACE and NP, respectively. The problem of lowering these upper bounds or finding matching lower bounds was left open. We show that the cut-off problem is P-complete for leaderless protocols and in NC for leaderless symmetric protocols. Further, we also consider a variant of the cut-off problem suggested in (Horn and Sangnier, CONCUR 2020), which we call the bounded-loss cut-off problem and prove that this problem is P-complete for leaderless protocols and NL-complete for leaderless symmetric protocols. Finally, by reusing some of the techniques applied for the analysis of leaderless protocols, we show that the cut-off problem for symmetric protocols with a leader is NP-complete, thereby improving upon all the elementary upper bounds of (Horn and Sangnier, CONCUR 2020).

Regular model checking is a technique for the verification of infinite-state systems whose configurations can be represented as finite words over a suitable alphabet. It applies to systems whose set of initial configurations is regular, and whose transition relation is captured by a length-preserving transducer. To verify safety properties, regular model checking iteratively computes automata recognizing increasingly larger regular sets of reachable configurations, and checks if they contain unsafe configurations. Since this procedure often does not terminate, acceleration, abstraction, and widening techniques have been developed to compute a regular superset of the reachable configurations. In this paper we develop a complementary procedure. Instead of approaching the set of reachable configurations from below, we start with the set of all configurations and approach it from above. We use that the set of reachable configurations is equal to the intersection of all inductive invariants of the system. Since this intersection is non-regular in general, we introduce b-bounded invariants, defined as those representable by CNF-formulas with at most b clauses. We prove that, for every b ≥ 0, the intersection of all b-bounded inductive invariants is regular, and we construct an automaton recognizing it. We show that whether this automaton accepts some unsafe configuration is in EXPSPACE for every b ≥ 0, and PSPACE-complete for b = 1. Finally, we study how large must b be to prove safety properties of a number of benchmarks.

A fundamental advantage of Petri net models is the possibility to automatically compute useful system invariants from the syntax of the net. Classical techniques used for this are place invariants, P-components, siphons or traps. Recently, Bozga et al. have presented a novel technique for the \emph{parameterized} verification of safety properties of systems with a ring or array architecture. They show that the statement \enquote{for every instance of the parameterized Petri net, all markings satisfying the linear invariants associated to all the P-components, siphons and traps of the instance are safe} can be encoded in \acs{WS1S} and checked using tools like MONA. However, while the technique certifies that this infinite set of linear invariants extracted from P-components, siphons or traps are strong enough to prove safety, it does not return an explanation of this fact understandable by humans. We present a CEGAR loop that constructs a \emph{finite} set of \emph{parameterized} P-components, siphons or traps, whose infinitely many instances are strong enough to prove safety. For this we design parameterization procedures for different architectures. Comment: Final version from editor

A graph whose edges only appear at certain points in time is called a temporal graph (among other names). Such a graph is temporally connected if each ordered pair of vertices is connected by a path which traverses edges in chronological order (i.e., a temporal path). In this paper, we consider a simple model of random temporal graph, obtained from an Erdös-Rényi random graph G ~ Gn,p by considering a random permutation π of the edges and interpreting the ranks in π as presence times. We give a thorough study of the temporal connectivity of such graphs and derive implications for the existence of several kinds of sparse spanners. It turns out that temporal reachability in this model exhibits a surprisingly regular sequence of thresholds. In particular, we show that, at p = log$n$/n, any fixed pair of vertices can a.a.s. reach each other; at 2 log$n$/n, at least one vertex (and in fact, any fixed vertex) can a.a.s. reach all others; and at 3 log$n$/n, all the vertices can a.a.s. reach each other, i.e., the graph is temporally connected. Furthermore, the graph admits a temporal spanner of size 2n + o(n) as soon as it becomes temporally connected, which is nearly optimal as 2n - 4 is a lower bound. This result is quite significant because temporal graphs do not admit spanners of size O(n) in general (Kempe, Kleinberg, Kumar, STOC 2000). In fact, they do not even always admit spanners of size o($n$2) (Axiotis, Fotakis, ICALP 2016). Thus, our result implies that the obstructions found in these works, and more generally, any non-negligible obstruction is statistically insignificant: nearly optimal spanners always exist in random temporal graphs. All the above thresholds are sharp. Carrying the study of temporal spanners a step further, we show that pivotal spanners-i.e., spanners of size 2n - 2 made of two spanning trees glued at a single vertex (one descending in time, the other ascending subsequently)-exist a.a.s. at 4 log$n$/ n, this threshold being also sharp. Finally, we show that optimal spanners (of size 2n - 4) also exist a.a.s. at p = 4 log$n$/n, Whether this value is a sharp threshold is open, we conjecture that it is. For completeness, we compare the above results to existing results in related areas, including edge-ordered graphs, gossip theory, and population protocols, showing that our results can be interpreted in these settings as well, and that in some cases, they improve known results therein. Finally, we discuss an intriguing connection between our results and Janson's celebrated results on percolation in weighted graphs.

Abstract In rendez-vous protocols an arbitrarily large number of indistinguishable finite-state agents interact in pairs. The cut-off problem asks if there exists a number B such that all initial configurations of the protocol with at least B agents in a given initial state can reach a final configuration with all agents in a given final state. In a recent paper [17], Horn and Sangnier prove that the cut-off problem is equivalent to the Petri net reachability problem for protocols with a leader, and in "Image missing" for leaderless protocols. Further, for the special class of symmetric protocols they reduce these bounds to "Image missing" and "Image missing" , respectively. The problem of lowering these upper bounds or finding matching lower bounds is left open. We show that the cut-off problem is "Image missing" -complete for leaderless protocols, "Image missing" -complete for symmetric protocols with a leader, and in "Image missing" for leaderless symmetric protocols, thereby solving all the problems left open in [17].

Abstract Population protocols (Angluin et al. in PODC, 2004) are a model of distributed computation in which indistinguishable, finite-state agents interact in pairs to decide if their initial configuration, i.e., the initial number of agents in each state, satisfies a given property. In a seminal paper Angluin et al. classified population protocols according to their communication mechanism, and conducted an exhaustive study of the expressive power of each class, that is, of the properties they can decide (Angluin et al. in Distrib Comput 20(4):279–304, 2007). In this paper we study the correctness problem for population protocols, i.e., whether a given protocol decides a given property. A previous paper (Esparza et al. in Acta Inform 54(2):191–215, 2017) has shown that the problem is decidable for the main population protocol model, but at least as hard as the reachability problem for Petri nets, which has recently been proved to have non-elementary complexity. Motivated by this result, we study the computational complexity of the correctness problem for all other classes introduced by Angluin et al., some of which are less powerful than the main model. Our main results show that for the class of observation models the complexity of the problem is much lower, ranging from $$\varPi _2^p$$ Π 2 p to .

We study the reachability problem for affine $\mathbb{Z}$-VASS, which are integer vector addition systems with states in which transitions perform affine transformations on the counters. This problem is easily seen to be undecidable in general, and we therefore restrict ourselves to affine $\mathbb{Z}$-VASS with the finite-monoid property (afmp-$\mathbb{Z}$-VASS). The latter have the property that the monoid generated by the matrices appearing in their affine transformations is finite. The class of afmp-$\mathbb{Z}$-VASS encompasses classical operations of counter machines such as resets, permutations, transfers and copies. We show that reachability in an afmp-$\mathbb{Z}$-VASS reduces to reachability in a $\mathbb{Z}$-VASS whose control-states grow linearly in the size of the matrix monoid. Our construction shows that reachability relations of afmp-$\mathbb{Z}$-VASS are semilinear, and in particular enables us to show that reachability in $\mathbb{Z}$-VASS with transfers and $\mathbb{Z}$-VASS with copies is PSPACE-complete. We then focus on the reachability problem for affine $\mathbb{Z}$-VASS with monogenic monoids: (possibly infinite) matrix monoids generated by a single matrix. We show that, in a particular case, the reachability problem is decidable for this class, disproving a conjecture about affine $\mathbb{Z}$-VASS with infinite matrix monoids we raised in a preliminary version of this paper. We complement this result by presenting an affine $\mathbb{Z}$-VASS with monogenic matrix monoid and undecidable reachability relation.

Vector addition systems with states (VASS) are widely used for the formal verification of concurrent systems. Given their tremendous computational complexity, practical approaches have relied on techniques such as reachability relaxations, e.g., allowing for negative intermediate counter values. It is natural to question their feasibility for VASS enriched with primitives that typically translate into undecidability. Spurred by this concern, we pinpoint the complexity of integer relaxations with respect to arbitrary classes of affine operations. More specifically, we provide a trichotomy on the complexity of integer reachability in VASS extended with affine operations (affine VASS). Namely, we show that it is NP-complete for VASS with resets, PSPACE-complete for VASS with (pseudo-)transfers and VASS with (pseudo-)copies, and undecidable for any other class. We further present a dichotomy for standard reachability in affine VASS: it is decidable for VASS with permutations, and undecidable for any other class. This yields a complete and unified complexity landscape of reachability in affine VASS. We also consider the reachability problem parameterized by a fixed affine VASS, rather than a class, and we show that the complexity landscape is arbitrary in this setting.

In a previous paper we introduced immediate observation (IO) Petri nets, a class of interest in the study of population protocols and enzymatic chemical networks. In the first part of this paper we show that IO nets are globally flat, and so their safety properties can be checked by efficient symbolic model checking tools using acceleration techniques, like FAST. In the second part we study Branching IO nets (BIO nets), whose transitions can create tokens. BIO nets extend both IO nets and communication-free nets, also called BPP nets, a widely studied class. We show that, while BIO nets are no longer globally flat, and their sets of reachable markings may be non-semilinear, they are still locally flat. As a consequence, the coverability and reachability problem for BIO nets, and even a certain set-parameterized version of them, are in PSPACE. This makes BIO nets the first natural net class with non-semilinear reachability relation for which the reachability problem is provably simpler than for general Petri nets.

Vector addition systems with states (VASS) are widely used for the formal verification of concurrent systems. Given their tremendous computational complexity, practical approaches have relied on techniques such as reachability relaxations, e.g., allowing for negative intermediate counter values. It is natural to question their feasibility for VASS enriched with primitives that typically translate into undecidability. Spurred by this concern, we pinpoint the complexity of integer relaxations w.r.t. arbitrary classes of affine operations.

We show that the minimization of visibly pushdown automata is NP-complete. This result is obtained by introducing immersions, that recognize multiple languages (over a usual, non-visible alphabet) using a common deterministic transition graph, such that each language is associated with an initial state and a set of final states. We show that minimizing immersions is NP-complete, and reduce this problem to the minimization of visibly pushdown automata.

Unambiguous non-deterministic finite automata (UFA) are non-deterministic automata (over finite words) such that there is at most one accepting run over each input. Such automata are known to be potentially exponentially more succinct than deterministic automata, and non-deterministic automata can be exponentially more succinct than them. In this paper we establish a superpolynomial lower bound for the state complexity of the translation of an UFA to a non-deterministic automaton for the complement language. This disproves the formerly conjectured polynomial upper bound for this translation. This lower bound only involves a one letter alphabet, and makes use of the random graph methods. The same proof also shows that the translation of sweeping automata to non-deterministic automata is superpolynomial.

We present the first linear lower bound for the number of bits required to be accessed in the worst case to increment an integer in an arbitrary space-optimal binary representation. The best previously known lower bound was logarithmic. It is known that a logarithmic number of read bits in the worst case is enough to increment some of the integer representations that use one bit of redundancy, therefore we show an exponential gap between space-optimal and redundant counters. Our proof is based on considering the increment procedure for a space optimal counter as a permutation and calculating its parity. For every space optimal counter, the permutation must be odd, and implementing an odd permutation requires reading at least half the bits in the worst case. The combination of these two observations explains why the worst-case space-optimal problem is substantially different from both average-case approach with constant expected number of reads and almost space optimal representations with logarithmic number of reads in the worst case.