2 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
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