Model checking hyperproperties for Markov decision processes

DOI10.1016/J.IC.2022.104978MaRDI QIDQ2105474zbMATH OpenOpenAlexWikidataFDO

Authors Oyendrila Dobe, Erika Ábrahám, Ezio Bartocci, Borzoo Bonakdarpour

Publication date 8 December 2022

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ic.2022.104978

zbMATH Keywords

hyperpropertiesinformation leakageMarkov modelsmodel checkingpolicy synthesis

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Recommendations

• Model checking algorithms for hyperproperties (invited paper)
• Bounded model checking for hyperproperties
• Multi-objective Model Checking of Markov Decision Processes
• Multi-Objective Model Checking of Markov Decision Processes
• Model checking quantitative hyperproperties
• Model checking finite-horizon Markov chains with probabilistic inference
• Model-checking continuous-time Markov chains
• scientific article; zbMATH DE number 7760477
• Model Checking Interactive Markov Chains

Cites work

• Algorithms for model checking HyperLTL and HyperCTL^*
• Bounded model checking for hyperproperties
• Defining liveness
• scientific article; zbMATH DE number 3614066 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties
• Model checking quantitative hyperproperties
• Monitoring hyperproperties
• On Decision Problems for Probabilistic Büchi Automata
• Program Repair for Hyperproperties
• Rewriting-based runtime verification for alternation-free HyperLTL
• Stochastic game logic
• Synthesis from hyperproperties
• The algorithmic foundations of differential privacy

Cited in

(4)

• Model checking quantitative hyperproperties
• Efficient loop conditions for bounded model checking hyperproperties
• Introducing asynchronicity to probabilistic hyperproperties
• Deductive controller synthesis for probabilistic hyperproperties

Describes a project that uses

Uses Software

• z3
• Storm

This page was built for publication: Model checking hyperproperties for Markov decision processes

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2105474)