Skip to Main content Skip to Navigation
Conference papers

Hyper Partial Order Logic

Béatrice Bérard 1 Stefan Haar 2 Loïc Hélouët 3
2 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], Inria Saclay - Ile de France
3 SUMO - SUpervision of large MOdular and distributed systems
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : We define HyPOL, a local hyper logic for partial order models, expressing properties of sets ofruns. These properties depict shapes of causal dependencies in sets of partially ordered executions,with similarity relations defined as isomorphisms of past observations. Unsurprisingly, sincecomparison of projections are included, satisfiability of this logic is undecidable. We then addressmodel checking of HyPOL and show that, already for safe Petri nets, the problem is undecidable.Fortunately, sensible restrictions of observations and nets allow us to bring back model checking ofHyPOL to a decidable problem, namely model checking of MSO on graphs of bounded treewidth.
Document type :
Conference papers
Complete list of metadata

Cited literature [29 references]  Display  Hide  Download

https://hal.inria.fr/hal-01884390
Contributor : Loic Helouet <>
Submitted on : Sunday, September 30, 2018 - 10:22:00 PM
Last modification on : Friday, April 30, 2021 - 9:54:24 AM
Long-term archiving on: : Monday, December 31, 2018 - 12:55:08 PM

File

Hopla.pdf
Files produced by the author(s)

Identifiers

Citation

Béatrice Bérard, Stefan Haar, Loïc Hélouët. Hyper Partial Order Logic. FSTTCS 2018 - Foundations of Software Technology and Theoretical Computer Science, Dec 2018, Ahmedabad, India. pp.20:1--20:21, ⟨10.4230/LIPIcs.FSTTCS.2018.20⟩. ⟨hal-01884390⟩

Share

Metrics

Record views

288

Files downloads

189