On-the-fly model checking for extended action-based probabilistic operators

被引：0
|
作者：
Radu Mateescu
José Ignacio Requeno
机构：
[1] Univ. Grenoble Alpes,
[2] Inria,undefined
[3] CNRS,undefined
[4] Grenoble INP,undefined
[5] LIG,undefined
[6] University of Zaragoza,undefined
来源：
International Journal on Software Tools for Technology Transfer | 2018年 / 20卷
关键词：
Probabilistic transition system; Action-based probabilistic logic; On-the-fly model checking;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
The quantitative analysis of concurrent systems requires expressive and user-friendly property languages combining temporal, data handling, and quantitative aspects. In this paper, we aim at facilitating the quantitative analysis of systems modeled as PTSs (Probabilistic Transition Systems) labeled by actions containing data values and probabilities. We propose a new regular probabilistic operator that specifies the probability measure of a path described by a generalized regular formula involving arbitrary computations on data values. This operator, which subsumes the Until operators of PCTL and their action-based counterparts, can provide useful quantitative information about paths having certain (e.g., peak) cost values. We integrated the regular probabilistic operator into MCL (Model Checking Language) and we devised an associated on-the-fly model checking method, based on a combined local resolution of linear and Boolean equation systems. We implemented the method in the EVALUATOR model checker of the CADP toolbox and experimented it on realistic PTSs modeling concurrent systems.
引用
收藏
页码：563 / 587
页数：24
相关论文
共 50 条
  • [21] On-the-fly model checking of program runs for automated debugging
    Frey, M
    Schlingloff, BH
    24TH EUROMICRO CONFERENCE - PROCEEDING, VOLS 1 AND 2, 1998, : 426 - 434
  • [22] On-the-fly TCTL model checking for time Petri nets
    Hadjidj, Rachid
    Boucheneb, Hanifa
    THEORETICAL COMPUTER SCIENCE, 2009, 410 (42) : 4241 - 4261
  • [23] On-the-fly model checking under fairness that exploits symmetry
    Gyuris, V
    Sistla, AP
    COMPUTER AIDED VERIFICATION, 1997, 1254 : 232 - 243
  • [24] Model checking for process rewrite systems and a class of action-based regular properties
    Bozzelli, Laura
    THEORETICAL COMPUTER SCIENCE, 2006, 360 (1-3) : 352 - 372
  • [25] Model checking for Process Rewrite Systems and a class of action-based regular properties
    Bozzelli, L
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, PROCEEDINGS, 2005, 3385 : 282 - 297
  • [26] Combining partial order reductions with on-the-fly model-checking
    Peled, D
    FORMAL METHODS IN SYSTEM DESIGN, 1996, 8 (01) : 39 - 64
  • [27] On-the-fly model checking of fair non-repudiation Protocols
    Li, Guoqiang
    Ogawa, Mizuhito
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2007, 4762 : 511 - +
  • [28] On-the-fly symbolic model checking for real-time systems
    Bouajjani, A
    Tripakis, S
    Yovine, S
    18TH IEEE REAL-TIME SYSTEMS SYMPOSIUM, PROCEEDINGS, 1997, : 25 - 34
  • [29] Fast on-the-fly parametric real-time model checking
    Zhang, DZ
    Cleaveland, R
    RTSS 2005: 26TH IEEE INTERNATIONAL REAL-TIME SYSTEMS SYMPOSIUM, PROCEEDINGS, 2005, : 157 - 166
  • [30] Concurrent On-the-fly SCC Detection for Automata-based Model Checking with Fairness Assumption
    Wu, Zhimin
    Xu, Yi
    Gunay, Akin
    Liu, Yang
    Qin, Shengchao
    2016 21ST INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS 2016), 2016, : 135 - 144
12345