Time-Bounded Reachability in Distributed Input/Output Interactive Probabilistic Chains

被引：0

作者：

Cahn, Georgel ^{[1
]}

Crouzen, Pepijn ^{[1
]}

D'Argenio, Pedro R. ^{[2
]}

Hahn, E. Moritz ^{[1
]}

Zhang, Lijun ^{[3
]}

机构：

[1] Univ Saarland, Dept Comp Sci, D-6600 Saarbrucken, Germany

[2] Univ Nacl Cordoba, FAMAF, Cordoba, Argentina

[3] Tech Univ Denmark, DTU Informat, Lyngby, Denmark

来源：

MODEL CHECKING SOFTWARE | 2010年 / 6349卷

关键词：

Distributed Systems; Probabilistic Models; Nondeterminism; Time-Bounded Reachability; MODEL CHECKING;

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We develop an algorithm to compute timed reachability probabilities for distributed models which are both probabilistic and nondeterministic. To obtain realistic results we consider the recently introduced class of (strongly) distributed schedulers, for which no analysis techniques are known. Our algorithm is based on reformulating the nondeterministic models as parametric ones, by interpreting scheduler decisions as parameters. We then apply the PARAM tool to extract the reachability probability as a polynomial function, which we optimize using nonlinear programming.

引用

页码：193 / +

页数：3

共 23 条

[1] AULT LH, 1982, MASTERMIND HDB
[2] Bianco A., 1995, Foundations of Software Technology and Theoretical Computer Science. 15th Conference. Proceedings, P499
[3] Boudali H, 2007, LECT NOTES COMPUT SC, V4762, P441
[4] CALIN G, 2010, 14AVACS64 SFBTR
[5] Canny J., 1988, Proceedings of the Twentieth Annual ACM Symposium on Theory of Computing, P460, DOI 10.1145/62212.62257
[6] Chaum D., 1988, Journal of Cryptology, V1, P65, DOI 10.1007/BF00206326
[7] Cheung L, 2005, LECT NOTES COMPUT SC, V3407, P494
[8] Coste N, 2008, DES AUT TEST EUROPE, P86
[9] Coste N, 2009, LECT NOTES COMPUT SC, V5643, P204, DOI 10.1007/978-3-642-02658-4_18
[10] Daws C, 2005, LECT NOTES COMPUT SC, V3407, P280

← 1 2 3 →