HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties

DOI10.1007/978-3-319-99154-2_2zbMath1514.68030arXiv1804.01853MaRDI QIDQ6104799

Borzoo Bonakdarpour, Erika Ábrahám

Publication date: 28 June 2023

Published in: Quantitative Evaluation of Systems (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1804.01853

Mathematics Subject Classification ID

Temporal logic (03B44) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items (12)

Timed hyperproperties ⋮ HyperPCTL model checking by probabilistic decomposition ⋮ On probability-raising causality in Markov decision processes ⋮ Foundations of probability-raising causality in Markov decision processes ⋮ Temporal causality in reactive systems ⋮ Operational causality -- necessarily sufficient and sufficiently necessary ⋮ Program Repair for Hyperproperties ⋮ Finite-word hyperlanguages ⋮ Compositional model checking for multi-properties ⋮ Statistical Model Checking for Probabilistic Hyperproperties of Real-Valued Signals ⋮ Finite-word hyperlanguages ⋮ Model checking hyperproperties for Markov decision processes

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Defining liveness
• A logic for reasoning about time and reliability
• The Algorithmic Foundations of Differential Privacy
• Proving the Correctness of Multiprocess Programs
• A logical approach to multilevel security of probabilistic systems

This page was built for publication: HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties