Model checking for probabilistic timed automata

被引:82
作者
Norman, Gethin [1 ]
Parker, David [2 ]
Sproston, Jeremy [3 ]
机构
[1] Univ Glasgow, Sch Comp Sci, Glasgow G12 8RZ, Lanark, Scotland
[2] Univ Birmingham, Sch Comp Sci, Birmingham B15 2TT, W Midlands, England
[3] Univ Turin, Dipartimento Informat, I-10149 Turin, Italy
关键词
Probabilistic timed automata; Probabilistic model checking; Probabilistic real-time systems; SYSTEMS; BISIMULATION; VERIFICATION; GAMES;
D O I
10.1007/s10703-012-0177-x
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
Probabilistic timed automata (PTAs) are a formalism for modelling systems whose behaviour incorporates both probabilistic and real-time characteristics. Applications include wireless communication protocols, automotive network protocols and randomised security protocols. This paper gives an introduction to PTAs and describes techniques for analysing a wide range of quantitative properties, such as "the maximum probability of the airbag failing to deploy within 0.02 seconds", "the maximum expected time for the protocol to terminate" or "the minimum expected energy consumption required to complete all tasks". We present a temporal logic for specifying such properties and then give a survey of available model-checking techniques for formulae specified in this logic. We then describe two case studies in which PTAs are used for modelling and analysis: a probabilistic non-repudiation protocol and a task-graph scheduling problem.
引用
收藏
页码:164 / 190
页数:27
相关论文
共 67 条
[1]   A THEORY OF TIMED AUTOMATA [J].
ALUR, R ;
DILL, DL .
THEORETICAL COMPUTER SCIENCE, 1994, 126 (02) :183-235
[2]   MODEL-CHECKING IN DENSE REAL-TIME [J].
ALUR, R ;
COURCOUBETIS, C ;
DILL, D .
INFORMATION AND COMPUTATION, 1993, 104 (01) :2-34
[3]  
ALUR R, 1992, LECT NOTES COMPUT SC, V630, P340
[4]   Optimal paths in weighted timed automata [J].
Alur, R ;
La Torre, S ;
Pappas, GJ .
THEORETICAL COMPUTER SCIENCE, 2004, 318 (03) :297-322
[5]  
Alur R., 2011, 2011 International Conference on Embedded Software (EMSOFT 2011), P165
[6]  
ALUR R, 1991, LECT NOTES COMPUT SC, V510, P115
[7]   An extension of the inverse method to probabilistic timed automata [J].
Andre, Etienne ;
Fribourg, Laurent ;
Sproston, Jeremy .
FORMAL METHODS IN SYSTEM DESIGN, 2013, 42 (02) :119-145
[8]  
[Anonymous], 1976, DENUMERABLE MARKOV C, DOI DOI 10.1007/978-1-4684-9455-6
[9]  
Asarin E, 1998, LECT NOTES COMPUT SC, V1466, P470, DOI 10.1007/BFb0055642
[10]   Analysis of Non-Linear Probabilistic Hybrid Systems [J].
Assouramou, Joseph ;
Desharnais, Josee .
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2011, (57) :104-119