3 results
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 […]
Published on October 22, 2012
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 […]
Published on December 21, 2010
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 […]
Published on August 10, 2021