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 条
  • [11] Abstract model repair for probabilistic systems
    Chatzieleftheriou, G.
    Katsaros, P.
    INFORMATION AND COMPUTATION, 2018, 259 : 142 - 160
  • [12] Probabilistic Model Checking of Regenerative Concurrent Systems
    Paolieri, Marco
    Horvath, Andras
    Vicario, Enrico
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2016, 42 (02) : 153 - 169
  • [13] Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent Systems
    Fu, Chen
    Turrini, Andrea
    Huang, Xiaowei
    Song, Lei
    Feng, Yuan
    Zhang, Lijun
    PROCEEDINGS OF THE TWENTY-SEVENTH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2018, : 4757 - 4763
  • [14] Probabilistic model checking of networked automation systems
    Greifeneder, Juergen
    Frey, Georg
    AT-AUTOMATISIERUNGSTECHNIK, 2007, 55 (12) : 624 - 633
  • [15] Extended abstract: Transition traversal coverage estimation for symbolic model checking
    Xu, XW
    Kimura, S
    Horikawa, K
    Tsuchiya, T
    THIRD ACM & IEEE INTERNATIONAL CONFERENCE ON FORMAL METHODS AND MODELS FOR CO-DESIGN, PROCEEDINGS, 2005, : 259 - 260
  • [16] Abstract interpretation and model checking for checking secure information flow in concurrent systems
    De Francesco, N
    Santone, A
    Tesei, L
    FUNDAMENTA INFORMATICAE, 2003, 54 (2-3) : 195 - 211
  • [17] On the Use of Model and Logical Embeddings for Model Checking of Probabilistic Systems
    Das, Susmoy
    Sharma, Arpit
    FORMAL TECHNIQUES FOR DISTRIBUTED OBJECTS, COMPONENTS, AND SYSTEMS, FORTE 2023, 2023, 13910 : 115 - 131
  • [18] Model checking probabilistic systems against pushdown specifications
    Dubslaff, Clemens
    Baier, Christel
    Berg, Manuela
    INFORMATION PROCESSING LETTERS, 2012, 112 (8-9) : 320 - 328
  • [19] Logic and Model Checking by Imprecise Probabilistic Interpreted Systems
    Termine, Alberto
    Antonucci, Alessandro
    Primiero, Giuseppe
    Facchini, Alessandro
    MULTI-AGENT SYSTEMS, EUMAS 2021, 2021, 12802 : 211 - 227
  • [20] Probabilistic Model Checking for Feature-Oriented Systems
    Dubslaff, Clemens
    Baier, Christel
    Klueppelholz, Sascha
    TRANSACTIONS ON ASPECT-ORIENTED SOFTWARE DEVELOPMENT XII, 2015, 8989 : 180 - 220
12345