Name
Abstract | ||
|---|---|---|
Markov decision processes (MDP) can serve as operational model for probabilistic distributed systems and yield the basis for model checking algorithms against qualitative or quantitative properties. In this paper, we summarize the main steps of a quantitative analysis for a given MDP and formula of linear temporal logic, give an introduction to the modelling language ProbMela which provides a simple and intuitive way to describe complex systems with a MDP-semantics and present the basic features of the MDP model checker LiQuor. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1145/1059816.1059821 | SIGMETRICS Performance Evaluation Review |
Keywords | Field | DocType |
markov decision process,basic feature,main step,linear temporal logic,complex system,quantitative analysis,model checking algorithm,quantitative property,mdp model checker,operational model,distributed system,model checking | Complex system,Model checking,Markov model,Computer science,Partially observable Markov decision process,Markov decision process,Theoretical computer science,Linear temporal logic,Artificial intelligence,Probabilistic logic,Machine learning | Journal |
Volume | Issue | Citations |
32 | 4 | 8 |
PageRank | References | Authors |
0.55 | 18 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Christel Baier | 1 | 3053 | 185.85 |
| Frank Ciesinski | 2 | 299 | 14.52 |
| Marcus Größer | 3 | 334 | 18.23 |