Name
Abstract | ||
|---|---|---|
In the past, several model checking algorithms have been proposed to verify probabilistic reactive systems.The techniques to combat the state-explosion problem have mainly concentrated on symbolic methods with variants of decision diagrams or abstraction methods.In this paper, we show how partial order reduction with a variant of Peled's ample set method can be applied in the context of LTL model checking for probabilistic systems modelled by Markov decision processes. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1109/QEST.2004.30 | QEST |
Keywords | Field | DocType |
Markov processes,decision diagrams,decision theory,probability,program verification,set theory,symbol manipulation,temporal logic,LTL model checking,Markov decision processes,Peled ample set method,abstraction methods,decision diagrams,partial order reduction,probabilistic reactive systems,state-explosion problem,symbolic methods | Abstraction model checking,Discrete mathematics,Markov process,Model checking,Computer science,Algorithm,Markov decision process,Theoretical computer science,Decision theory,Probabilistic logic,Partial order reduction,Probabilistic relevance model | Conference |
ISBN | Citations | PageRank |
0-7695-2185-1 | 40 | 1.62 |
References | Authors | |
37 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Christel Baier | 1 | 3053 | 185.85 |
| Marcus Groser | 2 | 40 | 1.62 |
| Frank Ciesinski | 3 | 299 | 14.52 |