Deductive controller synthesis for probabilistic hyperproperties

DOI10.1007/978-3-031-43835-6_20MaRDI QIDQ6546464zbMATH OpenFDO

Authors Roman Andriushchenko, Ezio Bartocci, Milan Češka, Francesco Pontiggia, Sarah Sallinger

Publication date 29 May 2024

Full work available at URL https://doi.org/10.1007/978-3-031-43835-6_20

Mathematics Subject Classification ID

Markov and semi-Markov decision processes (90C40) Synthesis problems (93B50)

Recommendations

• Model checking hyperproperties for Markov decision processes
• Probabilistic Hyperproperties of Markov Decision Processes
• Probabilistic Hyperproperties with Nondeterminism
• HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties

Cites work

• scientific article; zbMATH DE number 2163041 (Why is no real title available?)
• scientific article; zbMATH DE number 7559459 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• A logic for reasoning about time and reliability
• A logical approach to multilevel security of probabilistic systems
• Differential Privacy
• HyperPCTL model checking by probabilistic decomposition
• HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties
• Inductive synthesis for probabilistic programs reaches new horizons
• Model checking hyperproperties for Markov decision processes
• Model checking probabilistic systems
• On probability-raising causality in Markov decision processes
• Probabilistic Couplings from Program Logics
• Probabilistic Hyperproperties of Markov Decision Processes
• Probabilistic Hyperproperties with Nondeterminism
• Shepherding hordes of Markov chains
• Software Verification of Hyperproperties Beyond k-Safety
• Synthesis from hyperproperties
• Synthesizing reactive systems from hyperproperties
• Verification and control of partially observable probabilistic real-time systems

This page was built for publication: Deductive controller synthesis for probabilistic hyperproperties

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