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
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 […]
Published on July 28, 2022