Efficient Sensitivity Analysis for Parametric Robust Markov Chains

Thom Badings, Sebastian Junges, Ahmadreza Marandi, Ufuk Topcu, Nils Jansen

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

29 Downloads (Pure)

Abstract

We provide a novel method for sensitivity analysis of parametric robust Markov chains. These models incorporate parameters and sets of probability distributions to alleviate the often unrealistic assumption that precise probabilities are available. We measure sensitivity in terms of partial derivatives with respect to the uncertain transition probabilities regarding measures such as the expected reward. As our main contribution, we present an efficient method to compute these partial derivatives. To scale our approach to models with thousands of parameters, we present an extension of this method that selects the subset of $k$ parameters with the highest partial derivative. Our methods are based on linear programming and differentiating these programs around a given value for the parameters. The experiments show the applicability of our approach on models with over a million states and thousands of parameters. Moreover, we embed the results within an iterative learning scheme that profits from having access to a dedicated sensitivity analysis.
Original languageEnglish
Title of host publicationComputer Aided Verification
Subtitle of host publication35th International Conference, CAV 2023, Paris, France, July 17–22, 2023, Proceedings, Part III
EditorsConstantin Enea, Akash Lal
Place of PublicationCham
PublisherSpringer
Pages62-85
Number of pages24
ISBN (Electronic)978-3-031-37709-9
ISBN (Print)978-3-031-37708-2
DOIs
Publication statusPublished - 17 Jul 2023
Event35th International Conference on Computer Aided Verification, CAV 2023 - Paris, France
Duration: 17 Jul 202322 Jul 2023
Conference number: 35

Publication series

NameLecture Notes in Computer Science (LNCS)
Volume13966
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference35th International Conference on Computer Aided Verification, CAV 2023
Abbreviated titleCAV 2023
Country/TerritoryFrance
CityParis
Period17/07/2322/07/23

Funding

The authors are supported by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST. K.W. is supported by the JST grant No. JPMJFS2136. A. Griggio has been partly supported by the project “AI@TN” funded by the Autonomous Province of Trento and by the PNRR project FAIR - Future AI Research (PE00000013), under the NRRP MUR program funded by the NextGenerationEU. M. Jonáš has been partly supported by the Czech Science Foundation grant GA23-06506S. Acknowledgements. This work is funded in part by the National Science Foundation under grant 1815633. Felix Stutz was supported by the Deutsche Forschungsgemein-schaft project 389792660 TRR 248—CPEC. This work is supported by the National Natural Science Foundation of China (62072309), CAS Project for Young Scientists in Basic Research (YSBR-040), ISCAS New Cultivation Project (ISCAS-PYFX-202201), an oversea grant from the State Key Laboratory of Novel Software Technology, Nanjing University (KFKT2022A03), and Birkbeck BEI School Project (EFFECT). Acknowledgments. The authors in Academia Sinica are partially funded by National Science and Technology Council grants NSTC110-2221-E-001-008-MY3, NSTC111-2221-E-001-014-MY3, NSTC111-2634-F-002-019, the Sinica Investigator Award AS-IA-109-M01, the Data Safety and Talent Cultivation Project AS-KPQ-109-DSTCP, and the Intel Fast Verified Postquan-tum Software Project. The authors in Shenzhen University and ISCAS are partially funded by Shenzhen Science and Technology Innovation Commission (JCYJ20210324094202008), the National Natural Science Foundation of China (62002228, 61836005), and the Natural Science Foundation of Guangdong Province (2022A1515011458, 2022A1515010880). This research has been partially funded by NWO grant NWA.1160.18.238 (PrimaVera), the ERC Starting Grant 101077178 (DEUCE), and grants ONR N00014-21-1-2502 and AFOSR FA9550-22-1-0403. Acknowledgement. This paper is based upon work supported in part by the National Science Foundation under FMITF-Track I Grant No. 2019302. We thank the CAV reviewers, and He Zhu for their valuable feedback. We also thank CloudLab for providing the research testbed for our experiments. Acknowledgements. This work has been partially funded by the Swedish Vinnova FFI Programme under grant 2021-02519, the Swedish Research Council (VR) under grant 2018-04727, the Swedish Foundation for Strategic Research (SSF) under the project WebSec (Ref. RIT17-0011), and the Wallenberg project UPDATE. We are also grateful for the opportunity to discuss the research at the Dagstuhl Seminar 22451 on “Principles of Contract Languages.” This material is in part based upon work supported by the DARPA SIEVE program and the Simons foundation. Any opinions, findings, and conclusions or recommendations expressed in this report are those of the author(s) and do not necessarily reflect the views of DARPA. It is also funded in part by NSF grant number 2110397 and the Stanford Center for Automated Reasoning. Acknowledgements. We thank the reviewers for their useful remarks that helped us improve the quality of the paper. This work was supported by the Czech Ministry of Education, Youth and Sports project LL1908 of the ERC.CZ programme, the Czech Science Foundation project GA23-07565S, the FIT BUT internal project FIT-S-23-8151, and the NSTC QC project under Grant no. NSTC 111-2119-M-001-004-and 112-2119-M-001-006-. Authors ordered alphabetically. R. Majumdar and A.-K. Schmuck are partially supported by DFG project 389792660 TRR 248-CPEC. A.-K. Schmuck is additionally funded through DFG project (SCHM 3541/1-1). K. Mallik is supported by the ERC project ERC-2020-AdG 101020093. M. Rychlicki is supported by the EPSRC project EP/V00252X/1. S. Soudjani is supported by the following projects: EPSRC EP/V043676/1, EIC 101070802, and ERC 101089047. This work was funded partially by the Ethereum Foundation under Grant ID FY22-0698 and the Spanish MCI, AEI and FEDER (EU) project PID2021-122830OB-C41. Acknowledgement. We thank Prof. Bican Xia for valuable information on the exponential theory of reals. The work is partially supported by the National Natural Science Foundation of China (NSFC) with Grant No. 62172271, ERC CoG 863818 (ForM-SMArt), the Hong Kong Research Grants Council ECS Project Number 26208122, the HKUST-Kaisa Joint Research Institute Project Grant HKJRI3A-055 and the HKUST Startup Grant R9272.

FundersFunder number
National Science Foundation2019302, 1815633, 2110397
Office of Naval ResearchN00014-21-1-2502
Air Force Office of Scientific Research (AFOSR)FA9550-22-1-0403
Engineering and Physical Sciences Research CouncilEP/V043676/1, EP/V00252X/1, EIC 101070802, 101089047
H2020 European Research Council101077178, 863818
Deutsche Forschungsgemeinschaft389792660 TRR 248-CPEC, SCHM 3541/1-1, ERC-2020-AdG 101020093, 389792660 TRR 248
National Natural Science Foundation of China62072309, 62002228, 61836005, 62172271, YSBR-040
Grantová Agentura České RepublikyGA23-07565S, FIT-S-23-8151, NSTC 111-2119-M-001-004-and 112-2119-M-001-006, GA23-06506S
Japan Science and Technology AgencyJPMJFS2136
Nederlandse Organisatie voor Wetenschappelijk OnderzoekNWA.1160.18.238
Vetenskapsrådet2018-04727
Nanjing UniversityKFKT2022A03
European Regional Development FundPID2021-122830OB-C41
Shenzhen University

    Fingerprint

    Dive into the research topics of 'Efficient Sensitivity Analysis for Parametric Robust Markov Chains'. Together they form a unique fingerprint.

    Cite this