Hyper Partial Order Logic - Archive ouverte HAL Access content directly
Conference Papers Year :

Hyper Partial Order Logic

(1) , (2) , (3)
1
2
3

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.
Fichier principal
Vignette du fichier
Hopla.pdf (670.23 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01884390 , version 1 (30-09-2018)

Identifiers

Cite

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⟩
185 View
154 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More