On the numerical verification of probabilistic rewriting systems

被引：0

作者：

Ben Hassen, Jounaidi ^{[1
]}

Tahar, Sofiene ^{[1
]}

机构：

[1] Concordia Univ, Dept Elect & Comp Engn, Montreal, PQ H3G 1M8, Canada

来源：

2006 DESIGN AUTOMATION AND TEST IN EUROPE, VOLS 1-3, PROCEEDINGS | 2006年

关键词：

D O I：

暂无

中图分类号：

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

学科分类号：

0812 ;

摘要：

We present in this paper a technique for the formal verification of probabilistic systems described in PMAUDE, a probabilistic extension of the rewriting system Maude. Our methodology is based on a numerical verification using the probabilistic symbolic model checking tool PRISM. In particular we show how we can construct an abstract system from the runs of a model that preserve all the probabilistic properties of the latter Then we deduce the probabilistic matrix that will be used for the verification in PRISM.

引用

页码：1223 / +

页数：2

共 50 条

[41] Quantitative Multi-objective Verification for Probabilistic Systems
Forejt, Vojtech
Kwiatkowska, Marta
Norman, Gethin
Parker, David
Qu, Hongyang
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2011, 6605 : 112 - +
[42] PROBABILISTIC VERIFICATION
PNUELI, A
ZUCK, LD
INFORMATION AND COMPUTATION, 1993, 103 (01) : 1 - 29
[43] Numerical probabilistic analysis for the study of systems with uncertainty
Dobronets, Boris S.
Popova, Olga A.
VESTNIK TOMSKOGO GOSUDARSTVENNOGO UNIVERSITETA-UPRAVLENIE VYCHISLITELNAJA TEHNIKA I INFORMATIKA-TOMSK STATE UNIVERSITY JOURNAL OF CONTROL AND COMPUTER SCIENCE, 2012, 21 (04): : 39 - 46
[44] Numerical probabilistic analysis of structural/acoustic systems
Allen, MJ
Vlahopoulos, N
MECHANICS OF STRUCTURES AND MACHINES, 2002, 30 (03): : 353 - 380
[45] Towards Erlang Verification by Term Rewriting
Vidal, German
LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION, LOPSTR 2013, 2014, 8901 : 109 - 126
[46] Software specification and verification in rewriting logic
Meseguer, J
MODELS, ALGEBRAS AND LOGIC OF ENGINEERING SOFTWARE, 2003, 191 : 133 - 193
[47] Verification of CRWL programs with rewriting logic
Cleva, Jose Miguel
Pita, Isabel
JOURNAL OF UNIVERSAL COMPUTER SCIENCE, 2006, 12 (11) : 1594 - 1617
[48] Probabilistic verification of hierarchical leader election protocol in dynamic systems
Yu Zhou
Nvqi Zhou
Tingting Han
Jiayi Gu
Weigang Wu
Frontiers of Computer Science, 2018, 12 : 763 - 776
[49] Verification of Strong Nash-equilibrium for Probabilistic BAR Systems
Fernando, Dileepa
Dong, Naipeng
Jegourel, Cyrille
Dong, Jin Song
FORMAL METHODS AND SOFTWARE ENGINEERING, ICFEM 2018, 2018, 11232 : 106 - 123
[50] Probabilistic verification of hierarchical leader election protocol in dynamic systems
Zhou, Yu
Zhou, Nvqi
Han, Tingting
Gu, Jiayi
Wu, Weigang
FRONTIERS OF COMPUTER SCIENCE, 2018, 12 (04) : 763 - 776

← 1 2 3 4 5 →