PROPhESY: A PRObabilistic ParamEter SYnthesis Tool

被引：85

作者：

Dehnert, Christian ^{[1
]}

Junges, Sebastian ^{[1
]}

Jansen, Nils ^{[1
]}

Corzilius, Florian ^{[1
]}

Volk, Matthias ^{[1
]}

Bruintjes, Harold ^{[1
]}

Katoen, Joost-Pieter ^{[1
]}

Abraham, Erika ^{[1
]}

机构：

[1] Rhein Westfal TH Aachen, Aachen, Germany

来源：

COMPUTER AIDED VERIFICATION, PT I | 2015年 / 9206卷

关键词：

QUANTITATIVE VERIFICATION; MODEL CHECKING; BOUNDS;

D O I：

10.1007/978-3-319-21690-4_13

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

We present PROPhESY, a tool for analyzing parametric Markov chains (MCs). It can compute a rational function (i.e., a fraction of two polynomials in the model parameters) for reachability and expected reward objectives. Our tool outperforms state-of-the-art tools and supports the novel feature of conditional probabilities. PROPhESY supports incremental automatic parameter synthesis (using SMT techniques) to determine "safe" and "unsafe" regions of the parameter space. All values in these regions give rise to instantiated MCs satisfying or violating the (conditional) probability or expected reward objective. PROPhESY features a web front-end supporting visualization and user-guided parameter synthesis. Experimental results show that PROPhESY scales to MCs with millions of states and several parameters.

引用

页码：214 / 231

页数：18

共 40 条

[1]

Alur R., 2015, ACM SIGLOG NEWS, V2, P46

[2]

Andrés ME, 2008, LECT NOTES COMPUT SC, V4963, P157, DOI 10.1007/978-3-540-78800-3_12

[3]

[Anonymous], ACM Transactions on Information and System Security (TISSEC), DOI DOI 10.1145/290163.290168

[4]

[Anonymous], 1994, TEMPLATES SOLUTION L, DOI DOI 10.1137/1.9781611971538

[5]

[Anonymous], 1993, LNCS

[6]

Baier C, 2008, PRINCIPLES OF MODEL CHECKING, P1

[7]

Baier C, 1997, LECT NOTES COMPUT SC, V1254, P119

[8]

Baier C, 2014, LNCS, V8413, P515, DOI DOI 10.1007/978-3-642-54862-8

[9] Performance Evaluation and Model Checking Join Forces [J].

Baier, Christel ;

Haverkort, Boudewijn R. ;

Hermanns, Holger ;

Katoen, Joost-Pieter .

COMMUNICATIONS OF THE ACM, 2010, 53 (09) :76-85

[10]

Barrett C., 2010, The satisfiability modulo theories library (SMT-LIB)

← 1 2 3 4 →