HyperPCTL model checking by probabilistic decomposition

DOI10.1007/978-3-031-07727-2_12zbMath1502.68189OpenAlexW4285120389MaRDI QIDQ2165513

Gianfranco Ciardo, Eshita Zaman, Erika Ábrahám, Borzoo Bonakdarpour

Publication date: 19 August 2022

Full work available at URL: https://doi.org/10.1007/978-3-031-07727-2_12

Mathematics Subject Classification ID

Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.) (60J20) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Cites Work

• Unnamed Item
• A temporal logic for asynchronous hyperproperties
• Probability and causality. Essays in honor of Wesley C. Salmon. With an annotated bibliography by Wesley C. Salmon
• Algorithms for model checking HyperLTL and HyperCTL\(^*\)
• Bounded model checking for hyperproperties
• The Algorithmic Foundations of Differential Privacy
• “Sometimes” and “not never” revisited
• HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties
• Verifying hyperliveness

This page was built for publication: HyperPCTL model checking by probabilistic decomposition