Search

• < Previous
• 1
• Next >

---

The Complexity of Reachability in Affine Vector Addition Systems with States

Michael Blondin ; Mikhail Raskin.

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&nbsp;[&hellip;]

---

Affine Extensions of Integer Vector Addition Systems with States

Michael Blondin ; Christoph Haase ; Filip Mazowiecki ; Mikhail Raskin.

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&nbsp;[&hellip;]

---

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

A. R. Balasubramanian ; Javier Esparza ; Mikhail Raskin.

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&nbsp;[&hellip;]

---