Symbolic computational techniques for solving games
Symbolic computational techniques for solving games
复制标题
解决博弈的符号计算技术
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
Wonhong Nam
中科院分区：
文献类型：
--
作者：
R. Alur;P. Madhusudan;Wonhong Nam
游戏对系统的模块化规范和分析很有用，在本文中，我们对不同组件控制的选项（例如，系统及其环境）进行了明确的启动。获胜的策略。形式的安全游戏“始终为p。对于用户指定的绑定k，通过减少量化布尔公式的满意度。我们讨论了两种技术，一种基于编码策略树的技术，另一个基于编码证人子图，以减少SAT。他们在两个示例中进行了可及性游戏，以及用于安全游戏的Tinyos片段的界面合成示例。 Semp [19]，Qube [12]和Berkmin [13]并对比结果。
Games are useful in modular specification and analysis of systems where the distinction among the choices controlled by different components (for instance, the system and its environment) is made explicit. In this paper, we formulate and compare various symbolic computational techniques for deciding the existence of winning strategies. The game structure is given implicitly, and the winning condition is either a reachability game of the form “p until q” (for state predicates p and q) or a safety game of the form “Always p.”For reachability games, the first technique employs symbolic fixed-point computation using ordered binary decision diagrams (BDDs) [9]. The second technique checks for the existence of strategies that ensure winning within k steps, for a user-specified bound k, by reduction to the satisfiability of quantified boolean formulas. Finally, the bounded case can also be solved by reduction to satisfiability of ordinary boolean formulas, and we discuss two techniques, one based on encoding the strategy tree and one based on encoding a witness subgraph, for reduction to Sat. We also show how some of these techniques can be adopted to solve safety games. We compare the various approaches by evaluating them on two examples for reachability games, and on an interface synthesis example for a fragment of TinyOS [15] for safety games. We use existing tools such as Mocha [4], Mucke [7], Semprop [19], Qube [12], and Berkmin [13] and contrast the results.