Statistical Model Checking for Probabilistic Hyperproperties of Real-Valued Signals

DOI10.1007/978-3-031-15077-7_4MaRDI QIDQ6487300zbMATH OpenFDO

Authors Shiraj Arora, René Rydhof Hansen, Kim G. Larsen, Axel Legay, Danny Bøgsted Poulsen

Publication date 7 December 2022

Full work available at URL https://doi.org/10.1007/978-3-031-15077-7_4

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties
• Probabilistic Hyperproperties of Markov Decision Processes
• Model checking quantitative hyperproperties
• HyperPCTL model checking by probabilistic decomposition
• Probabilistic Hyperproperties with Nondeterminism

Cites work

• A theory of timed automata
• Algorithms for model checking HyperLTL and HyperCTL^*
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• scientific article; zbMATH DE number 1905115 (Why is no real title available?)
• HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties
• Model checking quantitative hyperproperties
• Probabilistic Hyperproperties of Markov Decision Processes
• Probabilistic Hyperproperties with Nondeterminism
• Statistical model checking
• Statistical Model Checking for Networks of Priced Timed Automata
• The dining cryptographers problem: Unconditional sender and recipient untraceability
• Transforming out timing leaks

Cited in

(3)

• Conformance relations and hyperproperties for doping detection in time and space
• Probabilistic Hyperproperties with Nondeterminism
• RobTL: robustness temporal logic for CPS

This page was built for publication: Statistical Model Checking for Probabilistic Hyperproperties of Real-Valued Signals

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