arXiv subjects

Mikhail Raskin

Publications and source records attributed to Mikhail Raskin.

13 recordsLinked to original sources

arXiv2022

Geometry of Reachability sets of Vector Addition Systems

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 simple algorithm for deciding semilinearity of VAS reachability sets, the first one since Hauschildt's 1990 algorithm. As a second corollary, we prove that the complement of a reachability set always contains an infinite linear set.

cs.FL↗

arXiv2021

Population protocols with unreliable communication

Population protocols are a model of distributed computation intended for the study of networks of independent computing agents with dynamic communication structure. Each agent has a finite number of states, and communication opportunities occur nondeterministically, allowing the agents involved to change their states based on each other's states. In the present paper we study unreliable models based on population protocols and their variations from the point of view of expressive power. We model the effects of message loss. We show that for a general definition of unreliable protocols with constant-storage agents such protocols can only compute predicates computable by immediate observation population protocols (sometimes also called one-way protocols). Immediate observation population protocols are inherently tolerant of unreliable communication and keep their expressive power under a wide range of fairness conditions. We also prove that a large class of message-based models that are generally more expressive than immediate observation becomes strictly less expressive than immediate observation in the unreliable case.

cs.DC↗

arXiv2021

Abduction of trap invariants in parameterized systems

In a previous paper we have presented a CEGAR approach for the verification of parameterized systems with an arbitrary number of processes organized in an array or a ring. The technique is based on the iterative computation of parameterized invariants, i.e., infinite families of invariants for the infinitely many instances of the system. Safety properties are proved by checking that every global configuration of the system satisfying all parameterized invariants also satisfies the property; we have shown that this check can be reduced to the satisfiability problem for Monadic Second Order on words, which is decidable. A strong limitation of the approach is that processes can only have a fixed number of variables with a fixed finite range. In particular, they cannot use variables with range [0,N-1], where N is the number of processes, which appear in many standard distributed algorithms. In this paper, we extend our technique to this case. While conducting the check whether a safety property is inductive assuming a computed set of invariants becomes undecidable, we show how to reduce it to checking satisfiability of a first-order formula. We report on experiments showing that automatic first-order theorem provers can still perform this check for a collection of non-trivial examples. Additionally, we can give small sets of readable invariants for these checks.

cs.DC↗

arXiv2021

Computing Parameterized Invariants of Parameterized Petri Nets

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.

cs.DC↗

arXiv2021

The Complexity of Verifying Population Protocols

Population protocols [Angluin et al., 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., Distributed Computing, 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., Acta Informatica, 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 $Π_2^p$ to PSPACE.

cs.LO↗

arXiv2020

Finding Cut-Offs in Leaderless Rendez-Vous Protocols is Easy

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).

cs.LO↗

arXiv2020

Flatness and Complexity of Immediate Observation Petri Nets

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.

cs.LO↗

arXiv2020

Vector TSP: A Traveling Salesperson Problem with Racetrack-like Acceleration Constraints

We study a new version of the Traveling Salesperson Problem, called \VectorTSP, where the traveler is subject to discrete acceleration constraints, as defined in the paper-and-pencil game Racetrack (also known as Vector Racer). In this model, the degrees of freedom at a certain point in time depends on the current velocity, and the speed is not limited. The paper introduces this problem and initiates its study, discussing also the main differences with existing versions of TSP. Not surprisingly, the problem turns out to be NP-hard. A key feature of \VectorTSP is that it deals with acceleration in a discrete, combinatorial way, making the problem more amenable to algorithmic investigation. The problem involves two layers of trajectory planning: (1) the order in which cities are visited, and (2) the physical trajectory realizing such a visit, both interacting with each other. This interaction is formalized as an interactive protocol between a high-level tour algorithm and a trajectory oracle, the former calling the latter repeatedly. We present an exact implementation of the trajectory oracle, adapting the A* algorithm for paths over multiple checkpoints whose ordering is \emph{given} (this algorithm being possibly of independent interest). To motivate the problem further, we perform experiments showing that the naive approach consisting of solving the instance as an \EuclideanTSP first, then optimizing the trajectory of the resulting tour, is typically suboptimal and outperformed by simple (but dedicated) heuristics.

cs.DS↗

arXiv2020

Constructive expressive power of population protocols

Population protocols are a model of distributed computation intended for the study of networks of independent computing agents with dynamic communication structure. Each agent has a finite number of states, and communication opportunities occur nondeterministically, allowing the agents involved to change their states based on each other's states. Population protocols are often studied in terms of reaching a consensus on whether the input configuration satisfied some predicate. In the present paper we propose an alternative point of view. Instead of studying the properties of inputs that a protocol can recognise, we study the properties of outputs that a protocol eventually ensures. We define constructive expressive power. We show that for general population protocols and immediate observation population protocols the constructive expressive power coincides with the normal expressive power. Immediate observation protocols also preserve their relatively low verification complexity in the constructive expressive power setting.

cs.DC↗

arXiv2019

Affine Extensions of Integer Vector Addition Systems with States

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.

cs.LO↗

arXiv2019

A Stay-in-a-Set Game without a Stationary Equilibrium

We give an example of a finite-state two-player turn-based stochastic game with safety objectives for both players which has no stationary Nash equilibrium. This answers an open question of Secchi and Sudderth.

math.OC↗

arXiv2019

The Complexity of Reachability in Affine Vector Addition Systems with States

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.

cs.LO↗

arXiv2019

Parameterized Analysis of Immediate Observation Petri Nets

We introduce immediate observation Petri nets, a class of interest in the study of population protocols (a model of distributed computation), and enzymatic chemical networks. In these areas, relevant analysis questions translate into parameterized Petri net problems: whether an infinite set of Petri nets with the same underlying net, but different initial markings, satisfy a given property. We study the parameterized reachability, coverability, and liveness problems for immediate observation Petri nets. We show that all three problems are in PSPACE for infinite sets of initial markings defined by counting constraints, a class sufficiently rich for the intended application. This is remarkable, since the problems are already PSPACE-hard when the set of markings is a singleton, i.e., in the non-parameterized case. We use these results to prove that the correctness problem for immediate observation population protocols is PSPACE-complete, answering a question left open in a previous paper.

cs.LO↗