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 条
  • [1] A Proof Theory for Model Checking: An Extended Abstract
    Heath, Quentin
    Miller, Dale
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2017, (238): : 1 - 10
  • [2] Controller synthesis for probabilistic systems (extended abstract)
    Baier, C
    Grössler, M
    Leucker, M
    Bollig, B
    Ciesinski, F
    EXPLORING NEW FRONTIERS OF THEORETICAL INFORMATICS, 2004, 155 : 493 - 506
  • [3] On model checking durational Kripke structures
    Laroussinie, F
    Markey, N
    Schnoebelen, P
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, PROCEEDINGS, 2002, 2303 : 264 - 279
  • [4] Model checking: Historical perspective and example (extended abstract)
    Clarke, EM
    Berezin, S
    AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, 1998, 1397 : 18 - 24
  • [5] Model Checking of Recursive Probabilistic Systems
    Etessami, Kousha
    Yannakakis, Mihalis
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2012, 13 (02)
  • [6] Model Checking Hierarchical Probabilistic Systems
    Sun, Jun
    Song, Songzheng
    Liu, Yang
    FORMAL METHODS AND SOFTWARE ENGINEERING, 2010, 6447 : 388 - +
  • [7] Model checking for probabilistic timed systems
    Sproston, J
    VALIDATION OF STOCHASTIC SYSTEMS: A GUIDE TO CURRENT RESEARCH, 2004, 2925 : 189 - 229
  • [8] Model Checking for Probabilistic Multiagent Systems
    Chen Fu
    Andrea Turrini
    Xiaowei Huang
    Lei Song
    Yuan Feng
    Li-Jun Zhang
    Journal of Computer Science and Technology, 2023, 38 : 1162 - 1186
  • [9] Model Checking for Probabilistic Multiagent Systems
    Fu, Chen
    Turrini, Andrea
    Huang, Xiaowei
    Song, Lei
    Feng, Yuan
    Zhang, Li-Jun
    JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY, 2023, 38 (05) : 1162 - 1186
  • [10] Model checking probabilistic distributed systems
    Bollig, B
    Leucker, M
    ADVANCES IN COMPUTING SCIENCE - ASIAN 2003: PROGRAMMING LANGUAGES AND DISTRIBUTED COMPUTATION, 2003, 2896 : 291 - 304
12345