2026-08-15T23:17:32Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9919 2024-03-06T10:45:06Z ddc:004 open_access

Hyper Partial Order Logic Bérard, Béatrice Haar, Stefan Hélouët, Loic Partial orders logic hyper-logic We define HyPOL, a local hyper logic for partial order models, expressing properties of sets of runs. These properties depict shapes of causal dependencies in sets of partially ordered executions, with similarity relations defined as isomorphisms of past observations. Unsurprisingly, since comparison of projections are included, satisfiability of this logic is undecidable. We then address model 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 of HyPOL to a decidable problem, namely model checking of MSO on graphs of bounded treewidth. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Béatrice Bérard and Stefan Haar and Loic Hélouët 2018 Is Part Of LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2018.20 urn:nbn:de:0030-drops-99190 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.20 eng https://creativecommons.org/licenses/by/3.0/legalcode