Reachability Problems - 8th International Workshop, RP 2014, Oxford, UK, September 22-24, 2014. Proceedings
Reachability Problems - 8th International Workshop, RP 2014, Oxford, UK, September 22-24, 2014. Proceedings
复制标题
可达性问题 - 第 8 届国际研讨会，RP 2014，英国牛津，2014 年 9 月 22-24 日。会议记录
DOI：
10.1007/978-3-319-11439-2_5
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Carayol A
中科院分区：
文献类型：
--
作者：
Carayol A
我们表明，位置获胜策略下推可达性游戏可以实现的指数大小的确定性有限状态自动机。这种自动机读取给定下推配置的堆栈和控制状态，并输出从该位置可玩的获胜移动集合。这个结果最初可以归因于Kupferman，Piterman和Vardi使用基于双向树自动机的方法。我们提出了一个更直接的方法，建立在流行的饱和技术。Moped和WALi已经成功地实现了分析下推系统的饱和。因此，我们的方法具有潜在的实际应用，分子筛合成问题。
We show that positional winning strategies in pushdown reachability games can be implemented by deterministic finite state automata 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.