Quantitative Supermartingale Certificates
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908305080713216 |
|---|---|
| author | Abate, Alessandro Giacobbe, Mirco Roy, Diptarko |
| author_facet | Abate, Alessandro Giacobbe, Mirco Roy, Diptarko |
| contents | We introduce a general methodology for quantitative model checking and control synthesis with supermartingale certificates. We show that every specification that is invariant to time shifts admits a stochastic invariant that bounds its probability from below; for systems with general state space, the stochastic invariant bounds this probability as closely as desired; for systems with finite state space, it quantifies it exactly. Our result enables the extension of every certificate for the almost-sure satisfaction of shift-invariant specifications to its quantitative counterpart, ensuring completeness up to an approximation in the general case and exactness in the finite-state case. This generalises and unifies existing supermartingale certificates for quantitative verification and control under reachability, safety, reach-avoidance, and stability specifications, as well as asymptotic bounds on accrued costs and rewards. Furthermore, our result provides the first supermartingale certificate for computing upper and lower bounds on the probability of satisfying $ω$-regular and linear temporal logic specifications. We present an algorithm for quantitative $ω$-regular verification and control synthesis based on our method and demonstrate its practical efficacy on several infinite-state examples. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_05065 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Quantitative Supermartingale Certificates Abate, Alessandro Giacobbe, Mirco Roy, Diptarko Logic in Computer Science Systems and Control We introduce a general methodology for quantitative model checking and control synthesis with supermartingale certificates. We show that every specification that is invariant to time shifts admits a stochastic invariant that bounds its probability from below; for systems with general state space, the stochastic invariant bounds this probability as closely as desired; for systems with finite state space, it quantifies it exactly. Our result enables the extension of every certificate for the almost-sure satisfaction of shift-invariant specifications to its quantitative counterpart, ensuring completeness up to an approximation in the general case and exactness in the finite-state case. This generalises and unifies existing supermartingale certificates for quantitative verification and control under reachability, safety, reach-avoidance, and stability specifications, as well as asymptotic bounds on accrued costs and rewards. Furthermore, our result provides the first supermartingale certificate for computing upper and lower bounds on the probability of satisfying $ω$-regular and linear temporal logic specifications. We present an algorithm for quantitative $ω$-regular verification and control synthesis based on our method and demonstrate its practical efficacy on several infinite-state examples. |
| title | Quantitative Supermartingale Certificates |
| topic | Logic in Computer Science Systems and Control |
| url | https://arxiv.org/abs/2504.05065 |