Name
Abstract | ||
|---|---|---|
Markov automata allow us to model a wide range of complex real-life systems by combining continuous stochastic timing with probabilistic transitions and nondeterministic choices. By adding a reward function it is possible to model costs like the energy consumption of a system as well.However, models of real-life systems tend to be large, and the analysis methods for such powerful models like Markov (reward) automata do not scale well, which limits their applicability. To solve this problem we present an abstraction technique for Markov reward automata, based on stochastic games, together with automatic refinement methods for the computation of time-bounded accumulated reward properties. Experiments show a significant speed-up and reduction in system size compared to direct analysis methods. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1007/978-3-662-46081-8_10 | VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION (VMCAI 2015) |
Field | DocType | Volume |
Quantum finite automata,Nondeterministic algorithm,Computer science,Markov model,Markov chain,Automaton,Markov decision process,Theoretical computer science,Variable-order Markov model,Stochastic game | Conference | 8931 |
ISSN | Citations | PageRank |
0302-9743 | 2 | 0.37 |
References | Authors | |
27 | 6 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| bettina braitling | 1 | 60 | 4.64 |
| Luis María Ferrer Fioriti | 2 | 20 | 1.95 |
| Hassan Hatefi | 3 | 78 | 5.38 |
| Ralf Wimmer | 4 | 407 | 34.28 |
| Bernd Becker | 5 | 855 | 73.74 |
| Holger Hermanns | 6 | 3418 | 229.22 |