Simple Strategies in Multi-Objective MDPs

Florent Delgrange; Joost-Pieter Katoen; Tim Quatmann; Mickael Randour

doi:10.1007/978-3-030-45190-519

Simple Strategies in Multi-Objective MDPs

Florent Delgrange, Joost-Pieter Katoen, Tim Quatmann, Mickael Randour

Onderzoeksoutput: Conference paper

48 Downloads (Pure)

Samenvatting

We consider the verification of multiple expected reward objectives at once on Markov decision processes (MDPs). This enables a trade-off analysis among multiple objectives by obtaining a Pareto front. We focus on strategies that are easy to employ and implement. That is, strategies that are pure (no randomization) and have bounded memory. We show that checking whether a point is achievable by a pure stationary strategy is NP-complete, even for two objectives, and we provide an MILP encoding to solve the corresponding problem. The bounded memory case is treated by a product construction. Experimental results using Storm and Gurobi show the feasibility of our algorithms.

Originele taal-2	English
Titel	Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I
Redacteuren	Armin Biere, David Parker
Uitgeverij	Springer
Pagina's	346-364
Aantal pagina's	19
Volume	12078
ISBN van elektronische versie	978-3-030-45190-5
ISBN van geprinte versie	978-3-030-45189-9
DOI's	https://doi.org/10.1007/978-3-030-45190-519 https://doi.org/10.1007/978-3-030-45190-5_19
Status	Published - 17 apr 2020
Evenement	European Joint Conferences on Theory and Practice of Software: Tools and Algorithms for the Construction and Analysis of Systems - Dublin, Ireland Duur: 25 apr 2020 → 30 apr 2020 Congresnummer: 26 https://etaps.org/

Publicatie series

Naam	Lecture Notes in Computer Science
Uitgeverij	Springer

Conference

Conference	European Joint Conferences on Theory and Practice of Software
Verkorte titel	ETAPS 2020
Land	Ireland
Stad	Dublin
Periode	25/04/20 → 30/04/20
Internet adres	https://etaps.org/

Toegang tot document

Simple Strategies in Multi-Objective MDPsFinal published version, 467 KBLicentie: CC BY

Citeer dit

Delgrange, F., Katoen, J-P., Quatmann, T., & Randour, M. (2020). Simple Strategies in Multi-Objective MDPs. In A. Biere, & D. Parker (editors), Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I (Vol. 12078, blz. 346-364). (Lecture Notes in Computer Science). Springer. https://doi.org/10.1007/978-3-030-45190-519, https://doi.org/10.1007/978-3-030-45190-5_19

Delgrange, Florent ; Katoen, Joost-Pieter ; Quatmann, Tim ; Randour, Mickael. / Simple Strategies in Multi-Objective MDPs. Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I. redacteur / Armin Biere ; David Parker. Vol. 12078 Springer, 2020. blz. 346-364 (Lecture Notes in Computer Science).

@inproceedings{35c05449e7c04079a301b061809801af,

title = "Simple Strategies in Multi-Objective MDPs",

abstract = "We consider the verification of multiple expected reward objectives at once on Markov decision processes (MDPs). This enables a trade-off analysis among multiple objectives by obtaining a Pareto front. We focus on strategies that are easy to employ and implement. That is, strategies that are pure (no randomization) and have bounded memory. We show that checking whether a point is achievable by a pure stationary strategy is NP-complete, even for two objectives, and we provide an MILP encoding to solve the corresponding problem. The bounded memory case is treated by a product construction. Experimental results using Storm and Gurobi show the feasibility of our algorithms.",

author = "Florent Delgrange and Joost-Pieter Katoen and Tim Quatmann and Mickael Randour",

year = "2020",

month = apr,

day = "17",

doi = "10.1007/978-3-030-45190-519",

language = "English",

isbn = "978-3-030-45189-9",

volume = "12078",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "346--364",

editor = "Armin Biere and David Parker",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I",

note = "European Joint Conferences on Theory and Practice of Software : Tools and Algorithms for the Construction and Analysis of Systems, ETAPS 2020 ; Conference date: 25-04-2020 Through 30-04-2020",

url = "https://etaps.org/",

}

Delgrange, F, Katoen, J-P, Quatmann, T & Randour, M 2020, Simple Strategies in Multi-Objective MDPs. in A Biere & D Parker (redactie), Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I. vol. 12078, Lecture Notes in Computer Science, Springer, blz. 346-364, European Joint Conferences on Theory and Practice of Software, Dublin, Ireland, 25/04/20. https://doi.org/10.1007/978-3-030-45190-519, https://doi.org/10.1007/978-3-030-45190-5_19

Simple Strategies in Multi-Objective MDPs. / Delgrange, Florent; Katoen, Joost-Pieter; Quatmann, Tim; Randour, Mickael.

Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I. redactie / Armin Biere; David Parker. Vol. 12078 Springer, 2020. blz. 346-364 (Lecture Notes in Computer Science).

Onderzoeksoutput: Conference paper

TY - GEN

T1 - Simple Strategies in Multi-Objective MDPs

AU - Delgrange, Florent

AU - Katoen, Joost-Pieter

AU - Quatmann, Tim

AU - Randour, Mickael

N1 - Conference code: 26

PY - 2020/4/17

Y1 - 2020/4/17

N2 - We consider the verification of multiple expected reward objectives at once on Markov decision processes (MDPs). This enables a trade-off analysis among multiple objectives by obtaining a Pareto front. We focus on strategies that are easy to employ and implement. That is, strategies that are pure (no randomization) and have bounded memory. We show that checking whether a point is achievable by a pure stationary strategy is NP-complete, even for two objectives, and we provide an MILP encoding to solve the corresponding problem. The bounded memory case is treated by a product construction. Experimental results using Storm and Gurobi show the feasibility of our algorithms.

AB - We consider the verification of multiple expected reward objectives at once on Markov decision processes (MDPs). This enables a trade-off analysis among multiple objectives by obtaining a Pareto front. We focus on strategies that are easy to employ and implement. That is, strategies that are pure (no randomization) and have bounded memory. We show that checking whether a point is achievable by a pure stationary strategy is NP-complete, even for two objectives, and we provide an MILP encoding to solve the corresponding problem. The bounded memory case is treated by a product construction. Experimental results using Storm and Gurobi show the feasibility of our algorithms.

UR - https://link.springer.com/chapter/10.1007/978-3-030-45190-5_19

U2 - 10.1007/978-3-030-45190-519

DO - 10.1007/978-3-030-45190-519

M3 - Conference paper

SN - 978-3-030-45189-9

VL - 12078

T3 - Lecture Notes in Computer Science

SP - 346

EP - 364

BT - Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I

A2 - Biere, Armin

A2 - Parker, David

PB - Springer

T2 - European Joint Conferences on Theory and Practice of Software

Y2 - 25 April 2020 through 30 April 2020

ER -

Delgrange F, Katoen J-P, Quatmann T, Randour M. Simple Strategies in Multi-Objective MDPs. In Biere A, Parker D, redacteurs, Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I. Vol. 12078. Springer. 2020. blz. 346-364. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-030-45190-519, https://doi.org/10.1007/978-3-030-45190-5_19

Simple Strategies in Multi-Objective MDPs

Samenvatting

Publicatie series

Conference

Toegang tot document

Vingerafdruk

Citeer dit