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 条
  • [21] Complexity of Verification of Nondeterministic Probabilistic Multiagent Systems
    Valiev, M. K.
    Dekhtyar, M. I.
    AUTOMATIC CONTROL AND COMPUTER SCIENCES, 2011, 45 (07) : 390 - 396
  • [22] Assume-Guarantee Verification for Probabilistic Systems
    Kwiatkowska, Marta
    Norman, Gethin
    Parker, David
    Qui, Hongyang
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2010, 6015 : 23 - +
  • [23] A probabilistic approach to automatic verification of concurrent systems
    Tronci, E
    Della Penna, G
    Intrigila, B
    Zilli, MV
    APSEC 2001: EIGHTH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE, PROCEEDINGS, 2001, : 317 - 324
  • [24] Verification and control of partially observable probabilistic systems
    Gethin Norman
    David Parker
    Xueyi Zou
    Real-Time Systems, 2017, 53 : 354 - 402
  • [25] Probabilistic verification for "black-box" systems
    Younes, HLS
    COMPUTER AIDED VERIFICATION< PROCEEDINGS, 2005, 3576 : 253 - 265
  • [26] Verification of complex real-time systems using rewriting logic
    Computer Science Department, University of Biskra, BP 145 RP, Biskra
    07000, Algeria
    J. Compt. Inf. Technol., 2009, 3 (265-284):
  • [27] Formalization and Verification of Mobile Systems Calculus using the Rewriting Engine Maude
    Xie, Wanling
    Zhu, Huibiao
    Zhang, Min
    Lu, Gang
    Fang, Yucheng
    2018 IEEE 42ND ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC), VOL 1, 2018, : 213 - 218
  • [28] Timed Multiset Rewriting and the Verification of Time-Sensitive Distributed Systems
    Kanovich, Max
    Kirigin, Tajana Ban
    Nigam, Vivek
    Scedrov, Andre
    Talcott, Carolyn
    FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, FORMATS 2016, 2016, 9884 : 228 - 244
  • [29] Compositional Verification in Rewriting Logic
    Martin, Oscar
    Verdejo, Alberto
    Marti-Oliet, Narciso
    THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2024, 24 (01) : 57 - 109
  • [30] Rewriting for cryptographic protocol verification
    Genet, T
    Klay, F
    AUTOMATED DEDUCTION - CADE-17, 2000, 1831 : 271 - 290
12345