License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ICALP.2020.121
URN: urn:nbn:de:0030-drops-125282
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12528/
Go to the corresponding LIPIcs Volume Portal

Clemente, Lorenzo ; Lasota, Sławomir ; Piórkowski, Radosław

Timed Games and Deterministic Separability

pdf-format:
LIPIcs-ICALP-2020-121.pdf (0.6 MB)

Abstract

We study a generalisation of Büchi-Landweber games to the timed setting. The winning condition is specified by a non-deterministic timed automaton with epsilon transitions and only Player I can elapse time. We show that for fixed number of clocks and maximal numerical constant available to Player II, it is decidable whether she has a winning timed controller using these resources. More interestingly, we also show that the problem remains decidable even when the maximal numerical constant is not specified in advance, which is an important technical novelty not present in previous literature on timed games. We complement these two decidability result by showing undecidability when the number of clocks available to Player II is not fixed.
As an application of timed games, and our main motivation to study them, we show that they can be used to solve the deterministic separability problem for nondeterministic timed automata with epsilon transitions. This is a novel decision problem about timed automata which has not been studied before. We show that separability is decidable when the number of clocks of the separating automaton is fixed and the maximal constant is not. The problem whether separability is decidable without bounding the number of clocks of the separator remains an interesting open problem.

BibTeX - Entry

@InProceedings{clemente_et_al:LIPIcs:2020:12528,
  author =	{Lorenzo Clemente and Sławomir Lasota and Radosław Pi{\'o}rkowski},
  title =	{{Timed Games and Deterministic Separability}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{121:1--121:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Artur Czumaj and Anuj Dawar and Emanuela Merelli},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/12528},
  URN =		{urn:nbn:de:0030-drops-125282},
  doi =		{10.4230/LIPIcs.ICALP.2020.121},
  annote =	{Keywords: Timed automata, separability problems, timed games}
}

Keywords: Timed automata, separability problems, timed games
Collection: 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)
Issue Date: 2020
Date of publication: 29.06.2020

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI