Teaching Stratego to Play Ball: Optimal Synthesis for Continuous Space MDPs

Manfred Jaeger, Peter Gjøl Jensen*, Kim Guldstrand Larsen, Axel Bernard E Legay, Sean Sedwards, Jakob Haahr Taankvist

*Corresponding author

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Abstract

Formal models of cyber-physical systems, such as priced timed Markov decision processes, require a state space with continuous and discrete components. The problem of controller synthesis for such systems then can be cast as finding optimal strategies for Markov decision processes over a Euclidean state space. We develop two different reinforcement learning strategies that tackle the problem of continuous state spaces via online partition refinement techniques. We provide theoretical insights into the convergence of partition refinement schemes. Our techniques are implemented in Open image in new window . Experimental results show the advantages of our new techniques over previous optimization algorithms of Open image in new window .
Original languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis- 17th International Symposium, AVTA 2019, Proceedings : ATVA 2019: Automated Technology for Verification and Analysis
EditorsYu-Fang Chen, Chih-Hong Cheng, Javier Esparza
Number of pages17
PublisherSpringer
Publication date28 Oct 2019
Pages81-97
ISBN (Print)978-3-030-31783-6
ISBN (Electronic)978-3-030-31784-3
DOIs
Publication statusPublished - 28 Oct 2019
EventInternational Symposium on Automated Technology for Verification and Analysis - Taipei, Taiwan, Province of China
Duration: 28 Oct 201931 Oct 2019

Conference

ConferenceInternational Symposium on Automated Technology for Verification and Analysis
CountryTaiwan, Province of China
CityTaipei
Period28/10/201931/10/2019
SeriesLecture Notes in Computer Science
Volume11781
ISSN0302-9743

Fingerprint

Reinforcement learning
Teaching
Controllers
Cyber Physical System

Cite this

Jaeger, M., Jensen, P. G., Larsen, K. G., Legay, A. B. E., Sedwards, S., & Taankvist, J. H. (2019). Teaching Stratego to Play Ball: Optimal Synthesis for Continuous Space MDPs. In Y-F. Chen, C-H. Cheng, & J. Esparza (Eds.), Automated Technology for Verification and Analysis- 17th International Symposium, AVTA 2019, Proceedings: ATVA 2019: Automated Technology for Verification and Analysis (pp. 81-97). Springer. Lecture Notes in Computer Science, Vol.. 11781 https://doi.org/10.1007/978-3-030-31784-3_5
Jaeger, Manfred ; Jensen, Peter Gjøl ; Larsen, Kim Guldstrand ; Legay, Axel Bernard E ; Sedwards, Sean ; Taankvist, Jakob Haahr. / Teaching Stratego to Play Ball : Optimal Synthesis for Continuous Space MDPs. Automated Technology for Verification and Analysis- 17th International Symposium, AVTA 2019, Proceedings: ATVA 2019: Automated Technology for Verification and Analysis. editor / Yu-Fang Chen ; Chih-Hong Cheng ; Javier Esparza. Springer, 2019. pp. 81-97 (Lecture Notes in Computer Science, Vol. 11781).
@inproceedings{8215b9e2fec048ab9b02b61d0058b401,
title = "Teaching Stratego to Play Ball: Optimal Synthesis for Continuous Space MDPs",
abstract = "Formal models of cyber-physical systems, such as priced timed Markov decision processes, require a state space with continuous and discrete components. The problem of controller synthesis for such systems then can be cast as finding optimal strategies for Markov decision processes over a Euclidean state space. We develop two different reinforcement learning strategies that tackle the problem of continuous state spaces via online partition refinement techniques. We provide theoretical insights into the convergence of partition refinement schemes. Our techniques are implemented in Open image in new window . Experimental results show the advantages of our new techniques over previous optimization algorithms of Open image in new window .",
author = "Manfred Jaeger and Jensen, {Peter Gj{\o}l} and Larsen, {Kim Guldstrand} and Legay, {Axel Bernard E} and Sean Sedwards and Taankvist, {Jakob Haahr}",
year = "2019",
month = "10",
day = "28",
doi = "10.1007/978-3-030-31784-3_5",
language = "English",
isbn = "978-3-030-31783-6",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "81--97",
editor = "Yu-Fang Chen and Chih-Hong Cheng and Javier Esparza",
booktitle = "Automated Technology for Verification and Analysis- 17th International Symposium, AVTA 2019, Proceedings",
address = "Germany",

}

Jaeger, M, Jensen, PG, Larsen, KG, Legay, ABE, Sedwards, S & Taankvist, JH 2019, Teaching Stratego to Play Ball: Optimal Synthesis for Continuous Space MDPs. in Y-F Chen, C-H Cheng & J Esparza (eds), Automated Technology for Verification and Analysis- 17th International Symposium, AVTA 2019, Proceedings: ATVA 2019: Automated Technology for Verification and Analysis. Springer, Lecture Notes in Computer Science, vol. 11781, pp. 81-97, International Symposium on Automated Technology for Verification and Analysis, Taipei, Taiwan, Province of China, 28/10/2019. https://doi.org/10.1007/978-3-030-31784-3_5

Teaching Stratego to Play Ball : Optimal Synthesis for Continuous Space MDPs. / Jaeger, Manfred; Jensen, Peter Gjøl; Larsen, Kim Guldstrand; Legay, Axel Bernard E; Sedwards, Sean; Taankvist, Jakob Haahr.

Automated Technology for Verification and Analysis- 17th International Symposium, AVTA 2019, Proceedings: ATVA 2019: Automated Technology for Verification and Analysis. ed. / Yu-Fang Chen; Chih-Hong Cheng; Javier Esparza. Springer, 2019. p. 81-97 (Lecture Notes in Computer Science, Vol. 11781).

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

TY - GEN

T1 - Teaching Stratego to Play Ball

T2 - Optimal Synthesis for Continuous Space MDPs

AU - Jaeger, Manfred

AU - Jensen, Peter Gjøl

AU - Larsen, Kim Guldstrand

AU - Legay, Axel Bernard E

AU - Sedwards, Sean

AU - Taankvist, Jakob Haahr

PY - 2019/10/28

Y1 - 2019/10/28

N2 - Formal models of cyber-physical systems, such as priced timed Markov decision processes, require a state space with continuous and discrete components. The problem of controller synthesis for such systems then can be cast as finding optimal strategies for Markov decision processes over a Euclidean state space. We develop two different reinforcement learning strategies that tackle the problem of continuous state spaces via online partition refinement techniques. We provide theoretical insights into the convergence of partition refinement schemes. Our techniques are implemented in Open image in new window . Experimental results show the advantages of our new techniques over previous optimization algorithms of Open image in new window .

AB - Formal models of cyber-physical systems, such as priced timed Markov decision processes, require a state space with continuous and discrete components. The problem of controller synthesis for such systems then can be cast as finding optimal strategies for Markov decision processes over a Euclidean state space. We develop two different reinforcement learning strategies that tackle the problem of continuous state spaces via online partition refinement techniques. We provide theoretical insights into the convergence of partition refinement schemes. Our techniques are implemented in Open image in new window . Experimental results show the advantages of our new techniques over previous optimization algorithms of Open image in new window .

U2 - 10.1007/978-3-030-31784-3_5

DO - 10.1007/978-3-030-31784-3_5

M3 - Article in proceeding

SN - 978-3-030-31783-6

T3 - Lecture Notes in Computer Science

SP - 81

EP - 97

BT - Automated Technology for Verification and Analysis- 17th International Symposium, AVTA 2019, Proceedings

A2 - Chen, Yu-Fang

A2 - Cheng, Chih-Hong

A2 - Esparza, Javier

PB - Springer

ER -

Jaeger M, Jensen PG, Larsen KG, Legay ABE, Sedwards S, Taankvist JH. Teaching Stratego to Play Ball: Optimal Synthesis for Continuous Space MDPs. In Chen Y-F, Cheng C-H, Esparza J, editors, Automated Technology for Verification and Analysis- 17th International Symposium, AVTA 2019, Proceedings: ATVA 2019: Automated Technology for Verification and Analysis. Springer. 2019. p. 81-97. (Lecture Notes in Computer Science, Vol. 11781). https://doi.org/10.1007/978-3-030-31784-3_5