Search

• < Previous
• 1
• Next >

---

Forward Analysis for WSTS, Part III: Karp-Miller Trees

Michael Blondin ; Alain Finkel ; Jean Goubault-Larrecq.

This paper is a sequel of "Forward Analysis for WSTS, Part I: Completions" [STACS 2009, LZI Intl. Proc. in Informatics 3, 433-444] and "Forward Analysis for WSTS, Part II: Complete WSTS" [Logical Methods in Computer Science 8(3), 2012]. In these two papers, we provided a framework to conduct forward&nbsp;[&hellip;]

---

Well Behaved Transition Systems

Michael Blondin ; Alain Finkel ; Pierre McKenzie.

The well-quasi-ordering (i.e., a well-founded quasi-ordering such that all antichains are finite) that defines well-structured transition systems (WSTS) is shown not to be the weakest hypothesis that implies decidability of the coverability problem. We show coverability decidable for monotone&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;]

---

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;]

---

Separators in Continuous Petri Nets

Michael Blondin ; Javier Esparza.

Leroux has proved that unreachability in Petri nets can be witnessed by a Presburger separator, i.e. if a marking $\vec{m}_\text{src}$ cannot reach a marking $\vec{m}_\text{tgt}$, then there is a formula $\varphi$ of Presburger arithmetic such that: $\varphi(\vec{m}_\text{src})$ holds; $\varphi$ is&nbsp;[&hellip;]

---