Regular Strategies In Pushdown Reachability Games

Abstract : We show that positional winning strategies in pushdown reachability games can be implemented by deterministic finite state au-tomata of exponential size. Such automata read the stack and control state of a given pushdown configuration and output the set of winning moves playable from that position. This result can originally be attributed to Kupferman, Piterman and Vardi using an approach based on two-way tree automata. We present a more direct approach that builds upon the popular saturation technique. Saturation for analysing pushdown systems has been successfully implemented by Moped and WALi. Thus, our approach has the potential for practical applications to controller-synthesis problems.
Document type :
Conference papers
Complete list of metadatas

Cited literature [20 references]  Display  Hide  Download

https://hal-upec-upem.archives-ouvertes.fr/hal-01719810
Contributor : Arnaud Carayol <>
Submitted on : Wednesday, February 28, 2018 - 3:00:19 PM
Last modification on : Thursday, August 9, 2018 - 4:41:52 PM
Long-term archiving on : Monday, May 28, 2018 - 1:22:07 PM

File

rp2014.pdf
Files produced by the author(s)

Identifiers

Citation

Arnaud Carayol, Matthew Hague. Regular Strategies In Pushdown Reachability Games. RP 2014, 2014, Oxford, United Kingdom. pp.58-71, ⟨10.1007/978-3-319-11439-2_5⟩. ⟨hal-01719810⟩

Share

Metrics

Record views

70

Files downloads

74