CISPA
Browse

Probabilistic Hyperproperties of Markov Decision Processes

Download (391.34 kB)
conference contribution
posted on 2023-11-29, 18:14 authored by Rayna DimitrovaRayna Dimitrova, Bernd FinkbeinerBernd Finkbeiner, Hazem Torfah
Hyperproperties are properties that describe the correctness of a system as a relation between multiple executions. Hyperproperties generalize trace properties and include information-flow security requirements, like noninterference, as well as requirements like symmetry, partial observation, robustness, and fault tolerance. We initiate the study of the specification and verification of hyperproperties of Markov decision processes (MDPs). We introduce the temporal logic PHL (Probabilistic Hyper Logic), which extends classic probabilistic logics with quantification over schedulers and traces. PHL can express a wide range of hyperproperties for probabilistic systems, including both classical applications, such as probabilistic noninterference, and novel applications in areas such as robotics and planning. While the model checking problem for PHL is in general undecidable, we provide methods both for proving and for refuting formulas from a fragment of the logic. The fragment includes many probabilistic hyperproperties of interest.

History

Preferred Citation

Rayna Dimitrova, Bernd Finkbeiner and Hazem Torfah. Probabilistic Hyperproperties of Markov Decision Processes. In: International Symposium on Automated Technology for Verification and Analysis (ATVA). 2020.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

International Symposium on Automated Technology for Verification and Analysis (ATVA)

Legacy Posted Date

2020-12-07

Open Access Type

  • Green

BibTeX

@inproceedings{cispa_all_3320, title = "Probabilistic Hyperproperties of Markov Decision Processes", author = "Dimitrova, Rayna and Finkbeiner, Bernd and Torfah, Hazem", booktitle="{International Symposium on Automated Technology for Verification and Analysis (ATVA)}", year="2020", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC