Model checking durational probabilistic systems - (Extended abstract)

被引：0
|
作者：
Laroussinie, F [1 ]
Sproston, J
机构：
[1] ENS, Lab Specificat & Verificat, CNRS, UMR 8643, Cachan, France
[2] Univ Turin, Dipartimento Informat, I-10149 Turin, Italy
来源：
FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, PROCEEDINGS | 2005年 / 3441卷
关键词：
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We consider model-checking algorithms for durational probabilistic systems, which are systems exhibiting nondeterministic, probabilistic and discrete-timed behaviour. We present two semantics for durational probabilistic systems, and show how formulae of the probabilistic and timed temporal logic PTCTL can be verified on such systems. We also address complexity issues, in particular identifying the cases in which model checking durational probabilistic systems is harder than verifying non-probabilistic durational systems.
引用
收藏
页码：140 / 154
页数：15
相关论文
共 50 条
  • [21] Quantitative refinement and model checking for the analysis of probabilistic systems
    McIver, A. K.
    FM 2006: FORMAL METHODS, PROCEEDINGS, 2006, 4085 : 131 - 146
  • [22] An optimal algorithm for checking regularity -: (Extended Abstract)
    Kohayakawa, Y
    Rödl, V
    Thomas, L
    PROCEEDINGS OF THE THIRTEENTH ANNUAL ACM-SIAM SYMPOSIUM ON DISCRETE ALGORITHMS, 2002, : 277 - 286
  • [23] Probabilistic Model Checking
    Baier, Christel
    DEPENDABLE SOFTWARE SYSTEMS ENGINEERING, 2016, 45 : 1 - 23
  • [24] Probabilistic Observations and Valuations (Extended Abstract)
    Schroeder, Matthias
    Simpson, Alex
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 155 : 605 - 615
  • [25] Model checking epistemic-probabilistic logic using probabilistic interpreted systems
    Wan, Wei
    Bentahar, Jamal
    Ben Hamza, Abdessamad
    KNOWLEDGE-BASED SYSTEMS, 2013, 50 : 279 - 295
  • [26] Abstract regular model checking
    Bouajjani, A
    Habermehl, P
    Vojnar, T
    COMPUTER AIDED VERIFICATION, 2004, 3114 : 372 - 386
  • [27] On-the-fly model checking for extended action-based probabilistic operators
    Radu Mateescu
    José Ignacio Requeno
    International Journal on Software Tools for Technology Transfer, 2018, 20 : 563 - 587
  • [28] Probabilistic model checking of biological systems with uncertain kinetic rates
    Barbuti, Roberto
    Levi, Francesca
    Milazzo, Paolo
    Scatena, Guido
    THEORETICAL COMPUTER SCIENCE, 2012, 419 : 2 - 16
  • [29] Towards probabilistic model checking on P systems using PRISM
    Romero-Campero, Francisco J.
    Gheorghe, Marian
    Bianco, Luca
    Pescini, Dario
    Perez-Jimenez, Mario J.
    Ceterchi, Rodica
    MEMBRANE COMPUTING, 2006, 4361 : 477 - +
  • [30] On-the-fly model checking for extended action-based probabilistic operators
    Mateescu, Radu
    Ignacio Requeno, Jose
    INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2018, 20 (05) : 563 - 587
12345