Robust probabilistic model checking with continuous reward domains
File(s)
Accepted version
Author(s)
Ji, Xiaotong
Wang, Hanchun
Filieri, Antonio
Epifani, Ilenia
Type
Conference Paper
Abstract
Probabilistic model checking traditionally verifies properties on the expected value of a measure of interest. This restriction may fail to capture the quality of service of a significant proportion of a system's runs, especially when the probability distribution of the measure of interest is poorly represented by its expected value due to heavy-tail behaviors or multiple modalities. Recent works inspired by distributional reinforcement learning use discrete histograms to approximate integer reward distribution, but they struggle with continuous reward space and present challenges in balancing accuracy and scalability. We propose a novel method for handling both continuous and discrete reward distributions in Discrete Time Markov Chains using moment matching with Erlang mixtures. By analytically deriving higher-order moments through Moment Generating Functions, our method approximates the reward distribution with theoretically bounded error while preserving the statistical properties of the true distribution. This detailed distributional insight enables the formulation and robust model checking of quality properties based on the entire reward distribution function, rather than restricting to its expected value. We include a theoretical foundation ensuring bounded approximation errors, along with an experimental evaluation demonstrating our method's accuracy and scalability in practical model-checking problems.
Date Issued
2025-06-13
Date Acceptance
2025-04-01
Citation
2025 IEEE/ACM 20th Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS), 2025, pp.13-24
ISSN
2157-2305
Publisher
IEEE
Start Page
13
End Page
24
Journal / Book Title
2025 IEEE/ACM 20th Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS)
Copyright Statement
Copyright © 2025, IEEE. Spiral Notice: Action Required DR Dear INSERT AUTHOR NAME, Thank you for submitting your paper. Please note that this submission is a duplicate of the following item which is already live in Spiral with the following identifier: INSERT SPIRAL HANDLE. Therefore, this submission has been rejected. No action is required by you in response to this email. If you have any questions or concerns, please do not hesitate to contact us. Kind regards, INSERT STAFF NAME HERE Imperial Open Access Team Please log into Symplectic here: https://www.imperial.ac.uk/research-and-innovation/support-for-staff/scholarly-communication/symplectic/ See: Symplectic & Spiral - what's the relationship? https://www.imperial.ac.uk/research-and-innovation/support-for-staff/scholarly-communication/open-access/symplectic-spiral-relationship/
License URL
Source
2025 IEEE/ACM 20th Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS)
Publication Status
Published
Start Date
2025-04-28
Finish Date
2025-04-29
Coverage Spatial
Ottawa, ON, Canada