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

---

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

---