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 条
  • [31] MODEL-CHECKING FOR PROBABILISTIC REAL-TIME SYSTEMS
    ALUR, R
    COURCOUBETIS, C
    DILL, D
    LECTURE NOTES IN COMPUTER SCIENCE, 1991, 510 : 115 - 126
  • [32] Modeling and analysis of cell membrane systems with probabilistic model checking
    Mirlaine A Crepalde
    Alessandra C Faria-Campos
    Sérgio VA Campos
    BMC Genomics, 12
  • [33] Statistical model checking of black-box probabilistic systems
    Sen, K
    Viswanathan, M
    Agha, G
    COMPUTER AIDED VERIFICATION, 2004, 3114 : 202 - 215
  • [34] An optimal automata approach to LTL model checking of probabilistic systems
    Couvreur, JM
    Saheb, N
    Sutre, G
    LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS, 2003, 2850 : 361 - 375
  • [35] Modeling and analysis of cell membrane systems with probabilistic model checking
    Crepalde, Mirlaine A.
    Faria-Campos, Alessandra C.
    Campos, Sergio V. A.
    BMC GENOMICS, 2011, 12
  • [36] Probabilistic Model Checking of Biological Systems with Uncertain Kinetic Rates
    Barbuti, Roberto
    Levi, Francesca
    Milazzo, Paolo
    Scatena, Guido
    REACHABILITY PROBLEMS, PROCEEDINGS, 2009, 5797 : 64 - +
  • [37] Checking the convexity of polytopes and the planarity of subdivisions - (Extended abstract)
    Devillers, O
    Liotta, G
    Preparata, FP
    Tamassia, R
    ALGORITHMS AND DATA STRUCTURES, 1997, 1272 : 186 - 199
  • [38] Predicting protein folding kinetics via temporal logic model checking (Extended abstract)
    Langmead, Christopher James
    Jha, Sumit Kumar
    ALGORITHMS IN BIOINFORMATICS, PROCEEDINGS, 2007, 4645 : 252 - +
  • [39] PCTL* Stochastic Model Checking Label-Extended Probabilistic Petri Net System Model
    Liu, Yang
    2014 5TH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND SERVICE SCIENCE (ICSESS), 2014, : 287 - 290
  • [40] Compiling Probabilistic Model Checking into Probabilistic Planning
    Klauck, Michaela
    Steinmetz, Marcel
    Hoffmann, Joerg
    Hermanns, Holger
    TWENTY-EIGHTH INTERNATIONAL CONFERENCE ON AUTOMATED PLANNING AND SCHEDULING (ICAPS 2018), 2018, : 150 - 154
12345