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

---

Reasoning about Data Repetitions with Counter Systems

Stephane Demri ; Diego Figueira ; M Praveen.

We study linear-time temporal logics interpreted over data words with multiple attributes. We restrict the atomic formulas to equalities of attribute values in successive positions and to repetitions of attribute values in the future or past. We demonstrate correspondences between satisfiability&nbsp;[&hellip;]

---

The complexity of linear-time temporal logic over the class of ordinals

Stephane Demri ; Alexander Rabinovich.

We consider the temporal logic with since and until modalities. This temporal logic is expressively equivalent over the class of ordinals to first-order logic by Kamp's theorem. We show that it has a PSPACE-complete satisfiability problem over the class of ordinals. Among the consequences of our&nbsp;[&hellip;]

---

Why Does Propositional Quantification Make Modal and Temporal Logics on Trees Robustly Hard?

Bartosz Bednarczyk ; Stéphane Demri.

Adding propositional quantification to the modal logics K, T or S4 is known to lead to undecidability but CTL with propositional quantification under the tree semantics (tQCTL) admits a non-elementary Tower-complete satisfiability problem. We investigate the complexity of strict fragments of tQCTL&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;]

---