Domains for Higher-Order Games. / Hague, Matthew; Meyer, Roland; Muskalla, Sebastian.

42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). LIPIcs, 2017. p. 59:1-59:15 59.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Published

Standard

Domains for Higher-Order Games. / Hague, Matthew; Meyer, Roland; Muskalla, Sebastian.

42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). LIPIcs, 2017. p. 59:1-59:15 59.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Harvard

Hague, M, Meyer, R & Muskalla, S 2017, Domains for Higher-Order Games. in 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)., 59, LIPIcs, pp. 59:1-59:15. https://doi.org/10.4230/LIPIcs.MFCS.2017.59

APA

Hague, M., Meyer, R., & Muskalla, S. (2017). Domains for Higher-Order Games. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017) (pp. 59:1-59:15). [59] LIPIcs. https://doi.org/10.4230/LIPIcs.MFCS.2017.59

Vancouver

Hague M, Meyer R, Muskalla S. Domains for Higher-Order Games. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). LIPIcs. 2017. p. 59:1-59:15. 59 https://doi.org/10.4230/LIPIcs.MFCS.2017.59

Author

Hague, Matthew ; Meyer, Roland ; Muskalla, Sebastian. / Domains for Higher-Order Games. 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). LIPIcs, 2017. pp. 59:1-59:15

BibTeX

@inproceedings{841602c6f0e34cd2b2c6e6a2d6f768cf,
title = "Domains for Higher-Order Games",
abstract = "We study two-player inclusion games played over word-generating higher-order recursion schemes. While inclusion checks are known to capture verification problems, two-player games generalize this relationship to program synthesis. In such games, non-terminals of the grammar are controlled by opposing players. The goal of the existential player is to avoid producing a word that lies outside of a regular language of safe words. We contribute a new domain that provides a representation of the winning region of such games. Our domain is based on (functions over) potentially infinite Boolean formulas with words as atomic propositions. We develop an abstract interpretation framework that we instantiate to abstract this domain into a domain where the propositions are replaced by states of a finite automaton. This second domain is therefore finite and we obtain, via standard fixed-point techniques, a direct algorithm for the analysis of two-player inclusion games. We show, via a second instantiation of the framework, that our finite domain can be optimized, leading to a (k+1)EXP algorithm for order-k recursion schemes. We give a matching lower bound, showing that our approach is optimal. Since our approach is based on standard Kleene iteration, existing techniques and tools for fixed-point computations can be applied.",
author = "Matthew Hague and Roland Meyer and Sebastian Muskalla",
year = "2017",
doi = "10.4230/LIPIcs.MFCS.2017.59",
language = "English",
isbn = "978-3-95977-046-0",
pages = "59:1--59:15",
booktitle = "42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)",
publisher = "LIPIcs",

}

RIS

TY - GEN

T1 - Domains for Higher-Order Games

AU - Hague, Matthew

AU - Meyer, Roland

AU - Muskalla, Sebastian

PY - 2017

Y1 - 2017

N2 - We study two-player inclusion games played over word-generating higher-order recursion schemes. While inclusion checks are known to capture verification problems, two-player games generalize this relationship to program synthesis. In such games, non-terminals of the grammar are controlled by opposing players. The goal of the existential player is to avoid producing a word that lies outside of a regular language of safe words. We contribute a new domain that provides a representation of the winning region of such games. Our domain is based on (functions over) potentially infinite Boolean formulas with words as atomic propositions. We develop an abstract interpretation framework that we instantiate to abstract this domain into a domain where the propositions are replaced by states of a finite automaton. This second domain is therefore finite and we obtain, via standard fixed-point techniques, a direct algorithm for the analysis of two-player inclusion games. We show, via a second instantiation of the framework, that our finite domain can be optimized, leading to a (k+1)EXP algorithm for order-k recursion schemes. We give a matching lower bound, showing that our approach is optimal. Since our approach is based on standard Kleene iteration, existing techniques and tools for fixed-point computations can be applied.

AB - We study two-player inclusion games played over word-generating higher-order recursion schemes. While inclusion checks are known to capture verification problems, two-player games generalize this relationship to program synthesis. In such games, non-terminals of the grammar are controlled by opposing players. The goal of the existential player is to avoid producing a word that lies outside of a regular language of safe words. We contribute a new domain that provides a representation of the winning region of such games. Our domain is based on (functions over) potentially infinite Boolean formulas with words as atomic propositions. We develop an abstract interpretation framework that we instantiate to abstract this domain into a domain where the propositions are replaced by states of a finite automaton. This second domain is therefore finite and we obtain, via standard fixed-point techniques, a direct algorithm for the analysis of two-player inclusion games. We show, via a second instantiation of the framework, that our finite domain can be optimized, leading to a (k+1)EXP algorithm for order-k recursion schemes. We give a matching lower bound, showing that our approach is optimal. Since our approach is based on standard Kleene iteration, existing techniques and tools for fixed-point computations can be applied.

U2 - 10.4230/LIPIcs.MFCS.2017.59

DO - 10.4230/LIPIcs.MFCS.2017.59

M3 - Conference contribution

SN - 978-3-95977-046-0

SP - 59:1-59:15

BT - 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

PB - LIPIcs

ER -