We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo

Computer Science > Logic in Computer Science

Title: Life is Random, Time is Not: Markov Decision Processes with Window Objectives

Abstract: The window mechanism was introduced by Chatterjee et al. to strengthen classical game objectives with time bounds. It permits to synthesize system controllers that exhibit acceptable behaviors within a configurable time frame, all along their infinite execution, in contrast to the traditional objectives that only require correctness of behaviors in the limit. The window concept has proved its interest in a variety of two-player zero-sum games because it enables reasoning about such time bounds in system specifications, but also thanks to the increased tractability that it usually yields.
In this work, we extend the window framework to stochastic environments by considering Markov decision processes. A fundamental problem in this context is the threshold probability problem: given an objective it aims to synthesize strategies that guarantee satisfying runs with a given probability. We solve it for the usual variants of window objectives, where either the time frame is set as a parameter, or we ask if such a time frame exists. We develop a generic approach for window-based objectives and instantiate it for the classical mean-payoff and parity objectives, already considered in games. Our work paves the way to a wide use of the window mechanism in stochastic models.
Subjects: Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI); Formal Languages and Automata Theory (cs.FL); Computer Science and Game Theory (cs.GT); Probability (math.PR)
Journal reference: Logical Methods in Computer Science, Volume 16, Issue 4 (December 14, 2020) lmcs:5968
DOI: 10.23638/LMCS-16(4:13)2020
Cite as: arXiv:1901.03571 [cs.LO]
  (or arXiv:1901.03571v5 [cs.LO] for this version)

Submission history

From: Mickael Randour [view email] [via LOGICAL proxy]
[v1] Fri, 11 Jan 2019 12:20:34 GMT (50kb)
[v2] Wed, 3 Jul 2019 16:52:04 GMT (39kb)
[v3] Wed, 11 Dec 2019 09:11:52 GMT (51kb)
[v4] Thu, 2 Apr 2020 13:53:51 GMT (46kb)
[v5] Thu, 10 Dec 2020 19:59:49 GMT (47kb,D)

Link back to: arXiv, form interface, contact.