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

---

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

---