Parameter Synthesis for Parametric Interval Markov Chains

被引：9

作者：

Delahaye, Benoit ^{[1
]}

Lime, Didier ^{[2
]}

Petrucci, Laure ^{[3
]}

机构：

[1] Univ Nantes, LINA, Nantes, France

[2] Ecole Cent Nantes, IRCCyN, Nantes, France

[3] Univ Paris 13, Sorbonne Paris Cite, UMR CNRS 7030, LIPN, Paris, France

来源：

VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2016 | 2016年 / 9583卷

关键词：

MODEL-CHECKING; SYSTEMS;

D O I：

10.1007/978-3-662-49122-5_18

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

Interval Markov Chains (IMCs) are the base of a classic probabilistic specification theory introduced by Larsen and Jonsson in 1991. They are also a popular abstraction for probabilistic systems. In this paper we study parameter synthesis for a parametric extension of Interval Markov Chains in which the endpoints of intervals may be replaced with parameters. In particular, we propose constructions for the synthesis of all parameter values ensuring several properties such as consistency and consistent reachability in both the existential and universal settings with respect to implementations. We also discuss how our constructions can be modified in order to synthesise all parameter values ensuring other typical properties.

引用

页码：372 / 390

页数：19

共 25 条

[1] An extension of the inverse method to probabilistic timed automata [J].

Andre, Etienne ;

Fribourg, Laurent ;

Sproston, Jeremy .

FORMAL METHODS IN SYSTEM DESIGN, 2013, 42 (02) :119-145

[2] Probabilistic model checking of biological systems with uncertain kinetic rates [J].

Barbuti, Roberto ;

Levi, Francesca ;

Milazzo, Paolo ;

Scatena, Guido .

THEORETICAL COMPUTER SCIENCE, 2012, 419 :2-16

[3]

Benedikt M, 2013, LECT NOTES COMPUT SC, V7795, P32, DOI 10.1007/978-3-642-36742-7_3

[4]

Bertrand N., 2013, IARCS ANN C FDN SOFT, V24, P501

[5]

Bertrand N, 2014, LECT NOTES COMPUT SC, V8412, P134

[6]

Biondi Fabrizio, 2013, Language and Automata Theory and Applications. 7th International Conference, LATA 2013. Proceedings, P128, DOI 10.1007/978-3-642-37064-9_13

[7] Constraint Markov Chains [J].

Caillaud, Benoit ;

Delahaye, Benoit ;

Larsen, Kim G. ;

Legay, Axel ;

Pedersen, Mikkel L. ;

Wasowski, Andrzej .

THEORETICAL COMPUTER SCIENCE, 2011, 412 (34) :4373-4404

[8] Model Checking of Open Interval Markov Chains [J].

Chakraborty, Souymodip ;

Katoen, Joost-Pieter .

ANALYTICAL AND STOCHASTIC MODELLING TECHNIQUES AND APPLICATIONS, ASMTA 2015, 2015, 9081 :30-42

[9] Computing Expected Absorption Times for Parametric Determinate Probabilistic Timed Automata [J].

Charnseddine, N. ;

Duflot, M. ;

Fribourg, L. ;

Picaronnyl, C. ;

Sproston, J. .

QUANTITATIVE EVALUATION OF SYSTEMS: QEST 2008, PROCEEDINGS, 2008, :254-+

[10]

Chatterjee K, 2008, LECT NOTES COMPUT SC, V4962, P302, DOI 10.1007/978-3-540-78499-9_22

← 1 2 3 →