Probabilistic Hyperproperties of Markov Decision Processes

DOI10.1007/978-3-030-59152-6_27MaRDI QIDQ6485906zbMATH OpenFDO

Authors Rayna Dimitrova, Bernd Finkbeiner, Hazem Torfah

Publication date 22 December 2022

Published in 1517.68228 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-030-59152-6_27

Mathematics Subject Classification ID

Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Markov and semi-Markov decision processes (90C40)

Recommendations

• Probabilistic Hyperproperties with Nondeterminism
• HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties
• HyperPCTL model checking by probabilistic decomposition
• Model checking algorithms for hyperproperties (invited paper)
• Temporal hyperproperties

Cited in

(23)

• Generalizing Markov decision processes to imprecise probabilities
• HyperPCTL model checking by probabilistic decomposition
• Verification of quantitative hyperproperties using trace enumeration relations
• Quantitative information flow as safety and liveness hyperproperties
• Towards incrementalization of holistic hyperproperties
• Probabilistic opacity for Markov decision processes
• Quantitative information flow as safety and liveness hyperproperties
• HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties
• HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems
• Temporal causality in reactive systems
• Probabilistic Hyperproperties with Nondeterminism
• Statistical Model Checking for Probabilistic Hyperproperties of Real-Valued Signals
• Stack-aware hyperproperties
• Second-order hyperproperties
• Monitoring algorithmic fairness
• Introducing asynchronicity to probabilistic hyperproperties
• Deductive controller synthesis for probabilistic hyperproperties
• Deciding hyperproperties combined with functional specifications
• Counterfactuals modulo temporal logics
• Stochastic games with synchronization objectives
• HyperLTL satisfiability is highly undecidable, \(\mathrm{HyperCTL}^*\) is even harder
• Demonic variance and a non-determinism score for Markov decision processes
• From verification to causality-based explications (invited talk)

This page was built for publication: Probabilistic Hyperproperties of Markov Decision Processes

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