Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II
Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II
复制标题
系统构建和分析的工具和算法 - 第 28 届国际会议，TACAS 2022，作为欧洲软件理论与实践联合会议的一部分举行，ETAPS 2022，德国慕尼黑，2022 年 4 月 2-7 日，会议记录，部分
DOI：
10.1007/978-3-030-99527-0_5
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Banerjee T
中科院分区：
文献类型：
--
作者：
Banerjee T
我们考虑具有规则获胜条件的图上基于回合制的随机2人博弈。当获胜条件被表述为Rabin条件时，我们提供了求解这类博弈的直接符号算法。对于一个随机的Rabin游戏，在一个有顶点的游戏图上，我们的算法以象征性的步骤运行，这提高了技术的水平。我们已经在一个名为Fairsyn的基于bdd的合成工具中实现了符号算法，以及包括并行化和加速在内的性能优化。我们在一组来自VLTS基准测试套件的合成基准测试和一个来自文献的控制系统基准测试上，证明了Fairsyn与现有技术相比的优越性。在我们的实验中，Fairsyn在计算时间上显著提高了两个数量级。
We consider turn-based stochastic 2-player games on graphs with-regular winning conditions. We provide a direct symbolic algorithm for solving such games when the winning condition is formulated as a Rabin condition. For a stochastic Rabin game withkpairs over a game graph withnvertices, our algorithm runs insymbolic steps, which improves the state of the art.We have implemented our symbolic algorithm, along with performance optimizations including parallellization and acceleration, in a BDD-based synthesis tool called Fairsyn. We demonstrate the superiority of Fairsyn compared to the state of the art on a set of synthetic benchmarks derived from the VLTS benchmark suite and on a control system benchmark from the literature. In our experiments, Fairsyn performed significantly faster with up totwoorders of magnitude improvement in computation time.