Modelling and analysis of Markov reward automata
| Autor: | Guck, Dennis, Timmer, Mark, Hatefi, Hassan, Ruijters, Enno J.J., Stoelinga, Mariëlle I.A., Cassez, Franck, Raskin, Jean-François |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2014 |
| Předmět: |
Computer Science::Machine Learning
Mathematical optimization Computer Science::Computer Science and Game Theory Computer science SCOOP 02 engineering and technology Reachability 0202 electrical engineering electronic engineering information engineering EC Grant Agreement nr.: FP7/2007-2013 EC Grant Agreement nr.: FP7/318490 ComputingMilieux_MISCELLANEOUS computer.programming_language Markov chain business.industry Probabilistic logic 020207 software engineering Extension (predicate logic) Energy consumption Automaton Costs EC Grant Agreement nr.: FP7/318003 020201 artificial intelligence & image processing Artificial intelligence State (computer science) EC Grant Agreement nr.: FP7/295261 business Markov automata computer Rewards Analysis |
| Zdroj: | Proceedings of the 12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014, 168-184 STARTPAGE=168;ENDPAGE=184;TITLE=Proceedings of the 12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014 Automated Technology for Verification and Analysis ISBN: 9783319119359 ATVA |
| ISSN: | 0302-9743 |
| DOI: | 10.1007/978-3-319-11936-6_13 |
| Popis: | Costs and rewards are important ingredients for many types of systems, modelling critical aspects like energy consumption, task completion, repair costs, and memory usage. This paper introduces Markov reward automata, an extension of Markov automata that allows the modelling of systems incorporating rewards (or costs) in addition to nondeterminism, discrete probabilistic choice and continuous stochastic timing. Rewards come in two flavours: action rewards, acquired instantaneously when taking a transition; and state rewards, acquired while residing in a state. We present algorithms to optimise three reward functions: the expected cumulative reward until a goal is reached, the expected cumulative reward until a certain time bound, and the long-run average reward. We have implemented these algorithms in the SCOOP/IMCA tool chain and show their feasibility via several case studies. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|