Search

• < Previous
• 1
• Next >

---

Petri Net Reachability Graphs: Decidability Status of First Order Properties

Philippe Darondeau ; Stephane Demri ; Roland Meyer ; Christophe Morvan.

We investigate the decidability and complexity status of model-checking problems on unlabelled reachability graphs of Petri nets by considering first-order and modal languages without labels on transitions or atomic propositions on markings. We consider several parameters to separate decidable&nbsp;[&hellip;]

---

A Complete Axiomatisation for Quantifier-Free Separation Logic

Stéphane Demri ; Étienne Lozes ; Alessio Mansutti.

We present the first complete axiomatisation for quantifier-free separation logic. The logic is equipped with the standard concrete heaplet semantics and the proof system has no external feature such as nominals/labels. It is not possible to rely completely on proof systems for Boolean BI as the&nbsp;[&hellip;]

---