| Identifikační kód | RIV/00216224:14330/15:00081426 |
|---|
| Název v anglickém jazyce | MultiGain: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives |
|---|
| Druh | D - Článek ve sborníku |
|---|
| Jazyk | eng - angličtina |
|---|
| Obor - skupina | I - Informatika |
|---|
| Obor | IN - Informatika |
|---|
| Rok uplatnění | 2015 |
|---|
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
|---|
| Počet výskytů výsledku | 1 |
|---|
| Počet tvůrců celkem | 4 |
|---|
| Počet domácích tvůrců | 2 |
|---|
| Výčet všech uvedených jednotlivých tvůrců | Tomáš Brázdil (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 1762834)
Chatterjee Krishnendu (státní příslušnost: AT - Rakouská republika)
Vojtěch Forejt (státní příslušnost: CZ - Česká republika, vedidk: 2477912)
Antonín Kučera (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 9872655) |
|---|
| Popis výsledku v anglickém jazyce | We present MultiGain, a tool to synthesize strategies for Markov decision processes (MDPs) with multiple mean-payoff objectives. Our models are described in PRISM, and our tool uses the existing interface and simulator of PRISM. Our tool extends PRISM byadding novel algorithms for multiple mean-payoff objectives, and also provides features such as (i) generating strategies and exploring them for simulation, and checking them with respect to other properties; and (ii) generating an approximate Pareto curve for two mean-payoff objectives. In addition, we present a new practical algorithm for the analysis of MDPs with multiple mean-payoff objectives under memoryless strategies. |
|---|
| Klíčová slova oddělená středníkem | Markov decision processes; mean-payoff reward; multi-objective optimisation; formal verification |
|---|
| Stránka www, na které se nachází výsledek | - |
|---|
| DOI výsledku | 10.1007/978-3-662-46681-0_12 |
|---|