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.FSCD.2020.14
URN: urn:nbn:de:0030-drops-123369
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12336/
Go to the corresponding LIPIcs Volume Portal

Bohrer, Rose ; Platzer, André

Refining Constructive Hybrid Games

pdf-format:
LIPIcs-FSCD-2020-14.pdf (0.6 MB)

Abstract

We extend the constructive differential game logic (CdGL) of hybrid games with a refinement connective that relates two hybrid games. In addition to CdGL’s ability to prove the existence of winning strategies for specific postconditions of hybrid games, game refinements relate two games to one another. That makes it possible to prove that any winning strategy for any postcondition of one game carries over to a winning strategy for the other. Since CdGL is constructive, a computable winning strategy can be extracted from a proof that a player wins a game. A folk theorem says that any such winning strategy for a hybrid game gives rise to a corresponding hybrid system satisfying the same property. We make this precise using CdGL’s game refinements and prove correct the construction of hybrid systems from winning strategies of hybrid games.

BibTeX - Entry

@InProceedings{bohrer_et_al:LIPIcs.FSCD.2020.14,
  author =	{Bohrer, Rose and Platzer, Andr\'{e}},
  title =	{{Refining Constructive Hybrid Games}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{14:1--14:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/12336},
  URN =		{urn:nbn:de:0030-drops-123369},
  doi =		{10.4230/LIPIcs.FSCD.2020.14},
  annote =	{Keywords: Hybrid Games, Constructive Logic, Refinement, Game Logic}
}

Keywords: Hybrid Games, Constructive Logic, Refinement, Game Logic
Collection: 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Issue Date: 2020
Date of publication: 28.06.2020

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