Record link: 
http://hdl.handle.net/20.500.12708/146162
-
Title: 
Probabilistic Hyperproperties with Rewards
en
Citation: 
Dobe, O., Wilke, L., Ábrahám, E., Bartocci, E., & Bonakdarpour, B. (2022). Probabilistic Hyperproperties with Rewards. In J. V. Deshmukh, K. Havelund, & I. Perez (Eds.), NASA Formal Methods : 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24–27, 2022, Proceedings (pp. 656–673). Springer. https://doi.org/10.1007/978-3-031-06773-0_35
-
Publisher DOI: 
10.1007/978-3-031-06773-0_35
-
Publication Type: 
Inproceedings - Full-Paper Contribution
en
Language: 
English
-
Authors: 
Dobe, Oyendrila 
Wilke, Lukas 
Ábrahám, Erika 
Bartocci, Ezio 
Bonakdarpour, Borzoo 
-
Organisational Unit: 
E191-01 - Forschungsbereich Cyber-Physical Systems 
-
Published in: 
NASA Formal Methods : 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24–27, 2022, Proceedings 
-
ISBN: 
978-3-031-06773-0
-
Volume: 
13260
-
Date (published): 
2022
-
Event name: 
14th International Symposium of NASA Formal Methods (NFM 2022) 
en
Event date: 
24-May-2022 - 27-May-2022
-
Event place: 
Pasadena, CA, United States of America (the)
-
Number of Pages: 
18
-
Publisher: 
Springer, Cham
-
Peer reviewed: 
Yes
-
Keywords: 
Hyperproperties; Markov models; Model checking; Policy; Rewards
en
Abstract: 
Probabilistic hyperproperties describe system properties that are concerned with the probability relation between different system executions. Likewise, it is desirable to relate performance metrics (e.g., energy, execution time, etc.) between multiple runs. This paper introduces the notion of rewards to the temporal logic HyperPCTL by extending the syntax and semantics of the logic to express the accumulated reward relation among different computations. We demonstrate the application of the extended logic in expressing side-channel timing countermeasures, efficiency in probabilistic conformance, path planning in robotics applications, and recovery time in distributed self-stabilizing systems. We also propose a model checking algorithm for verifying Markov Decision Processes against HyperPCTL with rewards and report experimental results.
en
Research Areas: 
Computer Engineering and Software-Intensive Systems: 100%
-
Science Branch: 
1020 - Informatik: 100%
-
Appears in Collections:
Conference Paper

Show full item record

Page view(s)

91
checked on Nov 23, 2023

Google ScholarTM

Check