pith. sign in

arxiv: 2604.06859 · v1 · submitted 2026-04-08 · 💻 cs.LO

Tractable Hyperproperties for MDPs

Lina Gerlach (RWTH Aachen University , Aachen , Germany) , Tobias Winkler (RWTH Aachen University , Erika \'Abrah\'am (RWTH Aachen University , Borzoo Bonakdarpour (Michigan State University , East Lansing , MI
show 4 more authors
USA) Sebastian Junges (Radboud University Nijmegen the Netherlands)
This is my paper

Pith reviewed 2026-05-10 17:22 UTC · model grok-4.3

classification 💻 cs.LO
keywords probabilistic hyperpropertiesMarkov decision processesmodel checkingreachabilityomega-regular objectivesrelational propertiessecurity verificationmulti-objective verification
0
0 comments X

The pith

Relational comparisons of event probabilities across independent MDP executions reduce to standard reachability and omega-regular verification.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes efficient algorithms for fragments of probabilistic hyperproperties that relate probabilities of events, possibly observed in separate independent runs of a Markov decision process. These fragments include checks such as whether distinct target states are reached with equal probability from one start, or whether one target is reached with equal probability from distinct starts, and extend to safety, Buchi, and coBuchi objectives as well as their conjunctive combinations. A sympathetic reader would care because full probabilistic hyperlogics are undecidable on MDPs, yet these restricted relational forms capture key security and privacy questions while admitting practical verification. The work supplies both polynomial-time algorithms for the tractable cases and hardness results for others, together with an implementation that runs orders of magnitude faster than general solvers on the relevant benchmark subset.

Core claim

We study relational probabilistic properties that compare the probabilities of events in possibly independent executions of an MDP. For reachability, safety, Buchi, and coBuchi objectives we supply efficient algorithms based on reductions to ordinary MDP model-checking problems whenever the property obeys a syntactic restriction that keeps the executions independent. Conjunctive combinations of these properties generalize standard multi-objective verification. We also prove computational hardness for other relational variants. An implementation of the approach outperforms solvers for more general probabilistic hyperlogics by orders of magnitude on the subset of benchmarks that lie inside the

What carries the argument

The central mechanism is the syntactic restriction to probability comparisons (equality or inequality) between events belonging to independent executions; this restriction enables sound reduction of the hyperproperty to a standard MDP reachability or omega-regular verification task.

If this is right

  • Equality between reachability probabilities for different targets from the same initial state reduces to a single reachability query or linear-equation system on the MDP.
  • Conjunctive combinations of relational properties can be solved by combining the independent reductions with existing multi-objective MDP techniques.
  • Safety, Buchi, and coBuchi objectives inherit the same polynomial-time procedures once the independence restriction holds.
  • Variants that drop the independence restriction remain hard even for simple reachability comparisons.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Existing off-the-shelf MDP solvers can be reused for this class of hyperproperties after a syntactic preprocessing step that encodes the relational query.
  • Many practical security policies that compare leakage or success probabilities across scenarios are likely to fall inside the tractable fragment rather than requiring undecidable full hyperlogics.
  • The same independence-preserving reduction technique could be tested on discounted probabilities or expected-reward comparisons to obtain analogous tractable fragments.

Load-bearing premise

The compared events must come from independent executions so that their probability measures factor and the reduction to single-system analysis remains valid.

What would settle it

Take an MDP whose nondeterminism can correlate two executions, encode a relational equality claim between their event probabilities, run the reduction algorithm, and compare its output against an exhaustive enumeration of all path measures to see whether equality is reported incorrectly.

read the original abstract

Probabilistic hyperproperties describe probabilistic relations between multiple sets of executions in a stochastic system. Prominent examples include information-theoretic characterizations of security and privacy policies. However, model checking for existing probabilistic hyperlogics, such as HyperPCTL and PHL, is undecidable in Markov decision processes (MDPs). In this paper, we study an underexplored problem: the verification of fragments of probabilistic hyperproperties that relate the probabilities of different events to each other, possibly across independent executions of an MDP. Representative verification questions include: Can two different target states be reached from the same initial state with the same probability? (different events), Can a given target state be reached from two different initial states with the same probability? (same event, independent executions), and natural combinations of these forms. Besides reachability, our relational probabilistic properties cover safety, B\"uchi, and coB\"uchi objectives. They can also be combined conjunctively, thereby generalizing standard multi-objective MDP properties. We provide efficient algorithms for relevant classes of relational properties, while proving computational hardness and completeness results for others. An implementation of our approach outperforms solvers for more general probabilistic hyperlogics by orders of magnitude on the subset of their benchmarks that lies within our fragment.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper claims to identify tractable fragments of probabilistic hyperproperties on MDPs consisting of relational comparisons (equality or inequality) between probabilities of events, possibly across independent executions. These fragments cover reachability, safety, Büchi, and coBüchi objectives and admit conjunctive combinations that generalize multi-objective MDP properties. Efficient algorithms are given via reductions to standard MDP reachability and ω-regular verification problems, hardness and completeness results are proven for complementary fragments, and an implementation is reported to outperform general probabilistic hyperlogic solvers by orders of magnitude on the relevant subset of existing benchmarks.

Significance. If the reductions and algorithms are correct, the work is significant because it carves out practically relevant decidable fragments from the undecidable landscape of full HyperPCTL/PHL model checking on MDPs. The explicit connection to multi-objective reachability, the delineation of hardness boundaries, and the reported performance gains on benchmarks provide both theoretical clarity and immediate engineering value for verifying security and privacy hyperproperties in stochastic systems.

minor comments (2)
  1. [Abstract] The abstract states that the implementation 'outperforms solvers ... by orders of magnitude'; a table or figure in the evaluation section that reports concrete runtime ratios on the shared benchmarks would strengthen this claim.
  2. The precise syntactic definition of the relational fragment (including how conjunctive combinations are formed) should be stated early, ideally with a small grammar or example formulas, to make the scope of the tractability results immediately clear.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary of our work and the recommendation of minor revision. The referee's description accurately reflects the paper's contributions on tractable relational probabilistic hyperproperties for MDPs, including the algorithms, hardness results, and implementation. No specific major comments were provided in the report.

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper defines syntactically restricted fragments of probabilistic hyperproperties (limited to direct equality/inequality comparisons of event probabilities, possibly across independent executions) and reduces their verification to standard, independently established MDP problems such as reachability and omega-regular verification. These reductions rely on the syntactic restrictions rather than any self-referential definitions, fitted parameters presented as predictions, or load-bearing self-citations. Hardness results for complementary fragments align with known undecidability of full HyperPCTL/PHL model checking. The central derivation chain is self-contained against external MDP theory benchmarks and exhibits no circular steps.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The approach rests on standard results about the decidability and complexity of reachability and omega-regular properties in finite MDPs; no new free parameters or postulated entities are introduced.

axioms (1)
  • standard math Reachability and omega-regular properties in finite MDPs are decidable in PSPACE and can be solved via linear programming or graph algorithms.
    Invoked to obtain polynomial or PSPACE algorithms for the relational fragment.

pith-pipeline@v0.9.0 · 5573 in / 1170 out tokens · 55033 ms · 2026-05-10T17:22:11.391212+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

24 extracted references · 24 canonical work pages

  1. [1]

    Parameter synthesis for probabilistic hyperproperties

    1 Erika Ábrahám, Ezio Bartocci, Borzoo Bonakdarpour, and Oyendrila Dobe. Parameter synthesis for probabilistic hyperproperties. In Elvira Albert and Laura Kovács, editors,23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR 2020, volume 73 ofEPiC Series in Computing, pages 12–31. EasyChair, 2020.doi: 10.29007...

    work page doi:10.29007/37lf 2020

  2. [2]

    3 Erika Ábrahám and Borzoo Bonakdarpour

    doi:10.1007/978-3-030-59152-6_29. 3 Erika Ábrahám and Borzoo Bonakdarpour. HyperPCTL: A temporal logic for probabilistic hyperproperties. In Annabelle McIver and András Horváth, editors,Quantitative Evaluation of Systems - 15th International Conference, QEST 2018, volume 11024 ofLecture Notes in Computer Science, pages 20–35. Springer, 2018.doi:10.1007/97...

    work page doi:10.1007/978-3-030-59152-6_29 2018

  3. [3]

    URL: https://www.ijcai.org/proceedings/2024/1. 5 S. Akshay, Blaise Genest, and Nikhil Vyas. Distribution-based objectives for markov decision processes. In Anuj Dawar and Erich Grädel, editors,Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 36–45. ACM, 2018.doi:10.1145/3209108....

    work page doi:10.1145/3209108.3209185 2024

  4. [4]

    10 Gilles Barthe and Justin Hsu

    doi: 10.46298/LMCS-20(1:4)2024. 10 Gilles Barthe and Justin Hsu. Probabilistic Couplings from Program Logics. In Alexandra Silva, Gilles Barthe, and Joost-Pieter Katoen, editors,Foundations of Probabilistic Programming, L. Gerlach, T. Winkler, E. Ábrahám, B. Bonakdarpour, S. Junges 51 pages 145–184. Cambridge University Press, Cambridge, 2020.doi:10.1017/...

    work page doi:10.46298/lmcs-20(1:4)2024 2024

  5. [5]

    Model checking of probabilistic and nondeterministic systems

    11 Andrea Bianco and Luca de Alfaro. Model checking of probabilistic and nondeterministic systems. In P. S. Thiagarajan, editor,Foundations of Software Technology and Theoretical Computer Science, FSTTCS 1995, volume 1026 ofLecture Notes in Computer Science, pages 499–513. Springer, 1995.doi:10.1007/3-540-60692-0_70. 12 Krishnendu Chatterjee. Markov Decis...

    work page doi:10.1007/3-540-60692-0_70 1995

  6. [6]

    15 Alexandre David, Kim G

    doi:10.1016/J.IPL.2013.01.004. 15 Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikucionis, and Zheng Wang. Time for Statistical Model Checking of Real-Time Systems. In Ganesh Gopalakrishnan and Shaz Qadeer, editors,Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20,

    work page doi:10.1016/j.ipl.2013.01.004 2013

  7. [7]

    Springer, 2011.doi:10.1007/978-3-642-22110-1_27

    Proceedings, volume 6806 ofLecture Notes in Computer Science, pages 349–355. Springer, 2011.doi:10.1007/978-3-642-22110-1_27. 16 Luca de Alfaro.Formal verification of probabilistic systems. PhD thesis, Stanford University, USA,

    work page doi:10.1007/978-3-642-22110-1_27 2011

  8. [8]

    Simple Strategies in Multi-Objective MDPs

    17 Florent Delgrange, Joost-Pieter Katoen, Tim Quatmann, and Mickael Randour. Simple Strategies in Multi-Objective MDPs. In Armin Biere and David Parker, editors,Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, E...

    work page doi:10.1007/978-3-030-45190-5_19 2020

  9. [9]

    52 Tractable Hyperproperties for MDPs 22 Kousha Etessami, Marta Z

    doi: 10.1007/11817963_11. 52 Tractable Hyperproperties for MDPs 22 Kousha Etessami, Marta Z. Kwiatkowska, Moshe Y. Vardi, and Mihalis Yannakakis. Multi- Objective Model Checking of Markov Decision Processes.Log. Methods Comput. Sci., 4(4), 2008.doi:10.2168/LMCS-4(4:8)2008. 23 Davis Foote and Brian Chu. Polynomial Time Approximate Solutions to Markov Decis...

    work page doi:10.1007/11817963_11 2008

  10. [10]

    Springer, 2011.doi:10.1007/978-3-642-19835-9_11

    Proceedings, volume 6605 ofLecture Notes in Computer Science, pages 112–127. Springer, 2011.doi:10.1007/978-3-642-19835-9_11. 25 Vojtech Forejt, Marta Z. Kwiatkowska, and David Parker. Pareto Curves for Probabil- istic Model Checking. In Supratik Chakraborty and Madhavan Mukund, editors,Auto- mated Technology for Verification and Analysis - 10th Internati...

    work page doi:10.1007/978-3-642-19835-9_11 2011

  11. [11]

    Springer, 2012.doi:10.1007/978-3-642-33386-6_25

    Proceedings, volume 7561 ofLecture Notes in Computer Science, pages 317–332. Springer, 2012.doi:10.1007/978-3-642-33386-6_25. 26 M. R. Garey and David S. Johnson. "Strong" NP-Completeness Results: Motivation, Examples, and Implications.J. ACM, 25(3):499–508, 1978.doi:10.1145/322077.322090. 27 Lina Gerlach, Tobias Winkler, Erika Ábrahám, Borzoo Bonakdarpou...

    work page doi:10.1007/978-3-642-33386-6_25 2012

  12. [12]

    28 Lina Gerlach, Tobias Winkler, Erika Ábrahám, Borzoo Bonakdarpour, and Sebastian Junges

    Springer Nature Switzerland.doi:10.1007/978-3-031-98668-0_6. 28 Lina Gerlach, Tobias Winkler, Erika Ábrahám, Borzoo Bonakdarpour, and Sebastian Junges. Efficient probabilistic model checking for relational reachability (extended version),

    work page doi:10.1007/978-3-031-98668-0_6

  13. [13]

    URL: https://arxiv.org/abs/2505.16357, arXiv:2505.16357, doi:10.48550/ARXIV.2505. 16357. 29Martin Grohe. Descriptive and parameterized complexity. InProc. of the 8th Int. Workshop on Computer Science Logic (CSL’99), pages 14–31, 1999.doi:10.1007/3-540-48168-0_3. 30 Arnd Hartmanns, Sebastian Junges, Tim Quatmann, and Maximilian Weininger. A Practi- tioner’...

    work page doi:10.48550/arxiv.2505 1999

  14. [14]

    31 Arnd Hartmanns and Benjamin Lucien Kaminski

    doi:10.1007/978-3-031-30823-9_24. 31 Arnd Hartmanns and Benjamin Lucien Kaminski. Optimistic value iteration. InProc. of the 32nd Int. Conf. on Computer Aided Verification (CAV’20), pages 488–511,

    work page doi:10.1007/978-3-031-30823-9_24

  15. [15]

    32 Christian Hensel, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, and Matthias Volk

    doi:10.1007/978-3-030-53291-8_26. 32 Christian Hensel, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, and Matthias Volk. The probabilistic model checker Storm.Int. J. Softw. Tools Technol. Transf., 24(4):589–610, 2022.doi:10.1007/S10009-021-00633-Z. 33 Amos Israeli and Marc Jalfon. Token Management Schemes and Random Walks Yield Self- Stabilizing Mu...

    work page doi:10.1007/978-3-030-53291-8_26 2022

  16. [16]

    LTL-Constrained Steady-State Policy Synthesis

    39 Jan Kretínský. LTL-Constrained Steady-State Policy Synthesis. In Zhi-Hua Zhou, editor, Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event / Montreal, Canada, 19-27 August 2021, pages 4104–4111. ijcai.org,

    work page 2021

  17. [17]

    40 Marta Z

    doi:10.24963/IJCAI.2021/565. 40 Marta Z. Kwiatkowska, Gethin Norman, and David Parker. PRISM 4.0: verification of probabilistic real-time systems. In Ganesh Gopalakrishnan and Shaz Qadeer, editors,Computer Aided Verification - 23rd International Conference, CAV 2011, volume 6806 ofLecture Notes in Computer Science, pages 585–591. Springer, 2011.doi:10.100...

    work page doi:10.24963/ijcai.2021/565 2021

  18. [18]

    44 Jasper Nalbach, Erika Ábrahám, and Gereon Kremer

    URL:https://doi.org/10.1007/s10817-025-09736-7, doi:10.1007/S10817-025-09736-7. 44 Jasper Nalbach, Erika Ábrahám, and Gereon Kremer. Extending the Fundamental Theorem of Linear Programming for Strict Inequalities. In Frédéric Chyzak and George Labahn, editors, ISSAC ’21: International Symposium on Symbolic and Algebraic Computation, Virtual Event, Russia,...

    work page doi:10.1007/s10817-025-09736-7 2021

  19. [19]

    46 Martin L

    Springer Berlin Heidelberg.doi:10.1007/978-3-642-36563-8_8. 46 Martin L. Puterman.Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics. Wiley, 1994.doi:10.1002/9780470316887. 47 Tim Quatmann.Multi-Objective Model Checking of Markov Automata. Master’s thesis,

    work page doi:10.1007/978-3-642-36563-8_8 1994

  20. [20]

    48 Tim Quatmann.Verification of Multi-Objective Markov Models

    doi:10.5281/zenodo.5101292. 48 Tim Quatmann.Verification of Multi-Objective Markov Models. PhD thesis, RWTH Aachen University,

    work page doi:10.5281/zenodo.5101292

  21. [21]

    Parameter Synthesis for Markov Models: Faster Than Ever

    49 Tim Quatmann, Christian Dehnert, Nils Jansen, Sebastian Junges, and Joost-Pieter Katoen. Parameter Synthesis for Markov Models: Faster Than Ever. In Cyrille Artho, Axel Legay, and Doron Peled, editors,Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings, volume 9938...

    work page doi:10.1007/978-3-319-46520-3_4 2016

  22. [22]

    51 Tim Quatmann and Joost-Pieter Katoen

    doi:10.1007/978-3-319-63387-9_7. 51 Tim Quatmann and Joost-Pieter Katoen. Sound Value Iteration. In Hana Chockler and Georg Weissenbacher, editors,Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I, volume 10981 ofLecture Notes ...

    work page doi:10.1007/978-3-319-63387-9_7 2018

  23. [23]

    53 Koushik Sen, Mahesh Viswanathan, and Gul Agha

    doi:10.1007/S10703-016-0262-7. 53 Koushik Sen, Mahesh Viswanathan, and Gul Agha. Model-Checking Markov Chains in the Presence of Uncertainties. In Holger Hermanns and Jens Palsberg, editors,Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, TACAS 2006 Held as Part of the Joint European Conferences on Theory a...

    work page doi:10.1007/s10703-016-0262-7 2006

  24. [24]

    A Full Algorithm forRelReach(Section 5.1) The algorithms in this section are taken verbatim from [28]

    doi:10.1109/ADPRL.2007.368183. A Full Algorithm forRelReach(Section 5.1) The algorithms in this section are taken verbatim from [28]. Algorithm 7 outlines the procedure presented in Section 5.1 for arbitrary comparison operators, including the handling of approximate computations using a black-box for approximate expected reward computa- tions Algorithm

    work page doi:10.1109/adprl.2007.368183 2007