Abstract
We study the problem of finding optimal strategies in Markov decision processes with lexicographic ω -regular objectives, which are ordered collections of ordinary ω -regular objectives. The goal is to compute strategies that maximise the probability of satisfaction of the first ω -regular objective; subject to that, the strategy should also maximise the probability of satisfaction of the second ω -regular objective; then the third and so forth. For instance, one may want to guarantee critical requirements first, functional ones second and only then focus on the non-functional ones. We show how to harness the classic off-the-shelf model-free reinforcement learning techniques to solve this problem and evaluate their performance on four case studies.
Original language | English |
---|---|
Title of host publication | 24th International Symposium on Formal Methods, FM 2021 |
Subtitle of host publication | Virtual Event, November 20–26, 2021, Proceedings |
Editors | Marieke Huisman, Corina S. Pasareanu, Naijun Zhan |
Publisher | Springer |
Pages | 142-159 |
Number of pages | 18 |
DOIs | |
Publication status | Published - 10 Nov 2021 |
Event | 24th International Symposium on Formal Methods, FM 2021 - Virtual, Online Duration: 20 Nov 2021 → 26 Nov 2021 Conference number: 24 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 13047 |
Conference
Conference | 24th International Symposium on Formal Methods, FM 2021 |
---|---|
Abbreviated title | FM 2021 |
City | Virtual, Online |
Period | 20/11/21 → 26/11/21 |
Keywords
- 22/1 OA procedure