DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2021.25

Time Flies When Looking out of the Window: Timed Games with Window Parity Objectives

Authors: James C. A. Main, Mickael Randour, and Jeremy Sproston

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract

The window mechanism was introduced by Chatterjee et al. to reinforce mean-payoff and total-payoff objectives with time bounds in two-player turn-based games on graphs [Krishnendu Chatterjee et al., 2015]. It has since proved useful in a variety of settings, including parity objectives in games [Véronique Bruyère et al., 2016] and both mean-payoff and parity objectives in Markov decision processes [Thomas Brihaye et al., 2020]. We study window parity objectives in timed automata and timed games: given a bound on the window size, a path satisfies such an objective if, in all states along the path, we see a sufficiently small window in which the smallest priority is even. We show that checking that all time-divergent paths of a timed automaton satisfy such a window parity objective can be done in polynomial space, and that the corresponding timed games can be solved in exponential time. This matches the complexity class of timed parity games, while adding the ability to reason about time bounds. We also consider multi-dimensional objectives and show that the complexity class does not increase. To the best of our knowledge, this is the first study of the window mechanism in a real-time setting.

Cite as

James C. A. Main, Mickael Randour, and Jeremy Sproston. Time Flies When Looking out of the Window: Timed Games with Window Parity Objectives. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 25:1-25:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{main_et_al:LIPIcs.CONCUR.2021.25,
  author =	{Main, James C. A. and Randour, Mickael and Sproston, Jeremy},
  title =	{{Time Flies When Looking out of the Window: Timed Games with Window Parity Objectives}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{25:1--25:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.25},
  URN =		{urn:nbn:de:0030-drops-144021},
  doi =		{10.4230/LIPIcs.CONCUR.2021.25},
  annote =	{Keywords: Window objectives, timed automata, timed games, parity games}
}

Search Results

Documents authored by Sproston, Jeremy

Time Flies When Looking out of the Window: Timed Games with Window Parity Objectives

Abstract

Cite as

Thanks for your feedback!

Could not send message