Approximate Parameter Synthesis for Probabilistic Time-Bounded Reachability

被引：45

作者：

Han, Tingting ^{[1
]}

Katoen, Joost-Pieter ^{[1
]}

Mereacre, Alexandru ^{[1
]}

机构：

[1] Univ Aachen, Rhein Westfal TH Aachen, Aachen, Germany

来源：

RTSS: 2008 REAL-TIME SYSTEMS SYMPOSIUM, PROCEEDINGS | 2008年

关键词：

MODEL-CHECKING;

D O I：

10.1109/RTSS.2008.19

中图分类号：

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

学科分类号：

0812 ;

摘要：

This paper proposes a technique to synthesize parametric rate values in continuous-time Markov chains that ensure the validity of bounded reachability properties. Rate expressions over variables indicate the average speed of state changes and are expressed using the polynomials over reals. The key contribution is an algorithm that approximates the set of parameter values for which the stochastic real-time system guarantees the validity of bounded reachability properties. This algorithm is based on discretizing parameter ranges together with a refinement technique. This paper describes the algorithm, analyzes its time complexity, and shows its applicability by deriving parameter constraints for a real-time storage system with probabilistic error checking facilities.

引用

页码：173 / 182

页数：10

共 23 条

[1]

Alur R., 1993, Proceedings of the Twenty-Fifth Annual ACM Symposium on the Theory of Computing, P592, DOI 10.1145/167088.167242

[2]

Avriel M., 1976, Nonlinear Programming: Analysis and Methods

[3] Model-checking algorithms for continuous-time Markov chains [J].

Baier, C ;

Haverkort, B ;

Hermanns, H ;

Katoen, JP .

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2003, 29 (06) :524-541

[4] ANALYSIS OF PROBABILISTIC ERROR CHECKING PROCEDURES ON STORAGE-SYSTEMS [J].

CHEN, IR ;

YEN, IL .

COMPUTER JOURNAL, 1995, 38 (05) :348-354

[5]

Cormen T. H., 2001, Introduction to Algorithms, V2nd, DOI DOI 10.1145/963770.963776

[6]

Daws C, 2005, LECT NOTES COMPUT SC, V3407, P280

[7]

Froberg R., 1998, INTRO GROBNER BASES

[8]

Hamming R. W., 1973, Numerical Methods for Scientists and Engineers

[9]

Hansen Eldon R., 1992, Global Optimization using Interval Analysis

[10]

HENRICI P, 1988, POWER SERIES INTEGRA

← 1 2 3 →