Name
Abstract | ||
|---|---|---|
This tutorial presents an overview of model checking for both discrete and continuous-time Markov chains (DTMCs and CTMCs).
Model checking algorithms are given for verifying DTMCs and CTMCs against specifications written in probabilistic extensions
of temporal logic, including quantitative properties with rewards. Example properties include the probability that a fault
occurs and the expected number of faults in a given time period. We also describe the practical application of stochastic
model checking with the probabilistic model checker PRISM by outlining the main features supported by PRISM and three real-world
case studies: a probabilistic security protocol, dynamic power management and a biological pathway.
|
Year | DOI | Venue |
|---|---|---|
2007 | 10.1007/978-3-540-72522-0_6 | School on Formal Methods for the Design of Computer, Communication and Software Systems |
Keywords | DocType | Volume |
stochastic model checking,probabilistic security protocol,biological pathway,probabilistic model checker prism,model checking,verifying dtmcs,model checking algorithm,dynamic power management,probabilistic extension,continuous-time markov chain,continuous time markov chain,stochastic model,probabilistic model,temporal logic,security protocol | Conference | 4486 |
ISSN | Citations | PageRank |
0302-9743 | 127 | 4.89 |
References | Authors | |
46 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Marta Z. Kwiatkowska | 1 | 6118 | 322.21 |
| Gethin Norman | 2 | 4163 | 193.68 |
| David Parker | 3 | 4018 | 184.00 |