Efficient Sensitivity Analysis for Parametric Robust Markov Chains

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

doi:10.1007/978-3-031-37709-9_4

Efficient Sensitivity Analysis for Parametric Robust Markov Chains

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

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › Academic › peer review

33 Downloads (Pure)

Samenvatting

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.

Originele taal-2	Engels
Titel	Computer Aided Verification
Subtitel	35th International Conference, CAV 2023, Paris, France, July 17–22, 2023, Proceedings, Part III
Redacteuren	Constantin Enea, Akash Lal
Plaats van productie	Cham
Uitgeverij	Springer
Pagina's	62-85
Aantal pagina's	24
ISBN van elektronische versie	978-3-031-37709-9
ISBN van geprinte versie	978-3-031-37708-2
DOI's	https://doi.org/10.1007/978-3-031-37709-9_4
Status	Gepubliceerd - 17 jul. 2023
Evenement	35th International Conference on Computer Aided Verification, CAV 2023 - Paris, Frankrijk Duur: 17 jul. 2023 → 22 jul. 2023 Congresnummer: 35

Publicatie series

Naam	Lecture Notes in Computer Science (LNCS)
Volume	13966
ISSN van geprinte versie	0302-9743
ISSN van elektronische versie	1611-3349

Congres

Congres	35th International Conference on Computer Aided Verification, CAV 2023
Verkorte titel	CAV 2023
Land/Regio	Frankrijk
Stad	Paris
Periode	17/07/23 → 22/07/23

Financiering

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.

Financiers	Financiernummer
Birkbeck University of London
Taiwan’s Executive Yuan Data Safety and Talent Cultivation Project	AS-KPQ-109-DSTCP
ERATO HASUO Metamathematics for Systems Design Project	JPMJER1603
FAIR	PE00000013
ISCAS New Cultivation Project	ISCAS-PYFX-202201
Swedish Vinnova FFI Programme	2021-02519
National Science Foundation(NSF)	2019302, 1815633, 2110397
Office of Naval Research	N00014-21-1-2502
Air Force Office of Scientific Research (AFOSR)	FA9550-22-1-0403
Defense Advanced Research Projects Agency
Simons Foundation
International Society for Computer Aided Surgery
Engineering and Physical Sciences Research Council	EP/V043676/1, EP/V00252X/1, EIC 101070802, 101089047
European Research Council	101077178, 863818
Ministry of Communications and Information, Singapore
Deutsche Forschungsgemeinschaft	389792660 TRR 248-CPEC, SCHM 3541/1-1, ERC-2020-AdG 101020093, 389792660 TRR 248
Stiftelsen för Strategisk Forskning	RIT17-0011
National Natural Science Foundation of China	62072309, 62002228, 61836005, 62172271, YSBR-040
Ministerstvo Školství, Mládeže a Tělovýchovy	LL1908
Grantová Agentura České Republiky	GA23-07565S, FIT-S-23-8151, NSTC 111-2119-M-001-004-and 112-2119-M-001-006, GA23-06506S
Japan Science and Technology Agency	JPMJFS2136
Research Grants Council, University Grants Committee	26208122, R9272, HKJRI3A-055
Nederlandse Organisatie voor Wetenschappelijk Onderzoek	NWA.1160.18.238
Natural Science Foundation of Guangdong Province	2022A1515010880, 2022A1515011458
Vetenskapsrådet	2018-04727
Nanjing University	KFKT2022A03
European Regional Development Fund	PID2021-122830OB-C41
Shenzhen University
Provincia Autonoma di Trento
Science, Technology and Innovation Commission of Shenzhen Municipality	JCYJ20210324094202008
Agencia Estatal de Investigación
State Key Laboratory of Novel Software Technology
Ethereum Foundation	FY22-0698
National Science and Technology Council	NSTC111-2221-E-001-014-MY3, NSTC111-2634-F-002-019, AS-IA-109-M01, NSTC110-2221-E-001-008-MY3

Toegang tot document

10.1007/978-3-031-37709-9_4Licentie: CC BY

pdfDefinitieve gepubliceerde versie, 759 KBLicentie: CC BY

Andere bestanden en links

Link naar publicatie in Scopus

1 computerprogramma software

Experiments for 'Efficient Sensitivity Analysis for Parametric Robust Markov Chains'
Badings, T. S., Junges, S., Marandi, A., Topcu, U. & Jansen, N., 12 mei 2023
Onderzoeksoutput: Niet-tekstuele vorm › computerprogramma software › Professioneel

Open Access

Citeer dit

Badings, T., Junges, S., Marandi, A., Topcu, U., & Jansen, N. (2023). Efficient Sensitivity Analysis for Parametric Robust Markov Chains. In C. Enea, & A. Lal (editors), Computer Aided Verification: 35th International Conference, CAV 2023, Paris, France, July 17–22, 2023, Proceedings, Part III (blz. 62-85). (Lecture Notes in Computer Science (LNCS); Vol. 13966). Springer. https://doi.org/10.1007/978-3-031-37709-9_4

Badings, Thom ; Junges, Sebastian ; Marandi, Ahmadreza et al. / Efficient Sensitivity Analysis for Parametric Robust Markov Chains. Computer Aided Verification: 35th International Conference, CAV 2023, Paris, France, July 17–22, 2023, Proceedings, Part III. redacteur / Constantin Enea ; Akash Lal. Cham : Springer, 2023. blz. 62-85 (Lecture Notes in Computer Science (LNCS)).

@inproceedings{1fc0c3b976a74843b52d7021e26ff034,

title = "Efficient Sensitivity Analysis for Parametric Robust Markov Chains",

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.",

author = "Thom Badings and Sebastian Junges and Ahmadreza Marandi and Ufuk Topcu and Nils Jansen",

year = "2023",

month = jul,

day = "17",

doi = "10.1007/978-3-031-37709-9_4",

language = "English",

isbn = "978-3-031-37708-2",

series = "Lecture Notes in Computer Science (LNCS)",

publisher = "Springer",

pages = "62--85",

editor = "Constantin Enea and Akash Lal",

booktitle = "Computer Aided Verification",

address = "Germany",

note = "35th International Conference on Computer Aided Verification, CAV 2023, CAV 2023 ; Conference date: 17-07-2023 Through 22-07-2023",

}

Badings, T, Junges, S, Marandi, A, Topcu, U & Jansen, N 2023, Efficient Sensitivity Analysis for Parametric Robust Markov Chains. in C Enea & A Lal (uitgave), Computer Aided Verification: 35th International Conference, CAV 2023, Paris, France, July 17–22, 2023, Proceedings, Part III. Lecture Notes in Computer Science (LNCS), vol. 13966, Springer, Cham, blz. 62-85, 35th International Conference on Computer Aided Verification, CAV 2023, Paris, Frankrijk, 17/07/23. https://doi.org/10.1007/978-3-031-37709-9_4

Efficient Sensitivity Analysis for Parametric Robust Markov Chains. / Badings, Thom; Junges, Sebastian ; Marandi, Ahmadreza et al.
Computer Aided Verification: 35th International Conference, CAV 2023, Paris, France, July 17–22, 2023, Proceedings, Part III. uitgave / Constantin Enea; Akash Lal. Cham: Springer, 2023. blz. 62-85 (Lecture Notes in Computer Science (LNCS); Vol. 13966).

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › Academic › peer review

TY - GEN

T1 - Efficient Sensitivity Analysis for Parametric Robust Markov Chains

AU - Badings, Thom

AU - Junges, Sebastian

AU - Marandi, Ahmadreza

AU - Topcu, Ufuk

AU - Jansen, Nils

N1 - Conference code: 35

PY - 2023/7/17

Y1 - 2023/7/17

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85169480532&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-37709-9_4

DO - 10.1007/978-3-031-37709-9_4

M3 - Conference contribution

SN - 978-3-031-37708-2

T3 - Lecture Notes in Computer Science (LNCS)

SP - 62

EP - 85

BT - Computer Aided Verification

A2 - Enea, Constantin

A2 - Lal, Akash

PB - Springer

CY - Cham

T2 - 35th International Conference on Computer Aided Verification, CAV 2023

Y2 - 17 July 2023 through 22 July 2023

ER -

Badings T, Junges S, Marandi A, Topcu U, Jansen N. Efficient Sensitivity Analysis for Parametric Robust Markov Chains. In Enea C, Lal A, redacteurs, Computer Aided Verification: 35th International Conference, CAV 2023, Paris, France, July 17–22, 2023, Proceedings, Part III. Cham: Springer. 2023. blz. 62-85. (Lecture Notes in Computer Science (LNCS)). doi: 10.1007/978-3-031-37709-9_4

Efficient Sensitivity Analysis for Parametric Robust Markov Chains

Samenvatting

Publicatie series

Congres

Financiering

Toegang tot document

Andere bestanden en links

Vingerafdruk

Onderzoekersoutput

Experiments for 'Efficient Sensitivity Analysis for Parametric Robust Markov Chains'

Citeer dit