Parity Games Benchmark Suite

Parity Games Benchmark Suite是由Jeroen J.A. Keiren在阿姆斯特丹自由大学和开放大学创建的一个综合数据集，包含1037个奇偶游戏实例，用于评估奇偶游戏算法的性能。数据集涵盖了从2个顶点到4000万个顶点的游戏，以及从2条边到1.67亿条边的范围。该数据集包括了多种类型的奇偶游戏，如模型检查、等价检查和随机游戏，旨在提供一个全面的标准化测试平台，以促进奇偶游戏算法的研究和开发。

Parity Games Benchmark Suite is a comprehensive dataset developed by Jeroen J.A. Keiren from Vrije Universiteit Amsterdam and Open Universiteit Nederland, consisting of 1037 parity game instances for performance evaluation of parity game algorithms. The dataset spans parity games ranging from 2 vertices up to 40 million vertices, with edge counts varying from 2 to 167 million. It encompasses multiple categories of parity games, including model checking games, equivalence checking games, and random games, aiming to provide a comprehensive standardized testbed to promote research and development in parity game algorithms.

搜集汇总

数据集介绍

构建方式

Parity Games Benchmark Suite数据集的构建方式涉及将各种验证问题编码为博弈游戏，并收集具有不同结构特性的博弈游戏。数据集包括从模型检验、等价性检验、决策过程和合成问题中编码得到的博弈游戏，以及为特定算法设计难以解决的博弈游戏和随机博弈。为了生成这些博弈游戏，研究人员使用了多种外部工具，如PGSolver、MLSolver和mCRL2工具集，并开发了pginfo工具来收集博弈游戏的结构信息。所有博弈游戏均以bzip2压缩的PGSolver格式提供，并包含收集到的结构信息。

特点

Parity Games Benchmark Suite数据集的特点在于其多样性，包含了来自不同验证问题的博弈游戏，并涵盖了在文献中被用于实验评估算法的博弈游戏。数据集涵盖了从2个顶点到4000万个顶点的各种规模的博弈游戏，平均每个游戏约有9.5万个顶点。边数从2条到1.67亿条不等，平均每个游戏约有310万条边。数据集还包括了具有不同结构特性的博弈游戏，如具有不同顶点度数、强连通分量、搜索策略特性和局部结构的游戏。此外，数据集还引入了交替深度这一新的结构特性，用于描述博弈游戏中不同优先级之间的交替情况。

使用方法

Parity Games Benchmark Suite数据集的使用方法包括下载并解压数据集文件，然后使用PGSolver格式读取博弈游戏。用户可以使用pginfo工具收集博弈游戏的结构信息，并使用这些信息来评估不同博弈游戏算法的性能。数据集的结构特性可以为博弈游戏算法的设计和优化提供有用的参考。此外，数据集还可以用于比较不同博弈游戏算法的实现和启发式方法的有效性。

背景与挑战

背景概述

Parity Games Benchmark Suite数据集的研究背景是模型检验研究，特别是在μ-计算模型检验问题的决定性胜利者方面。该数据集由Jeroen J.A.Keiren等人于2015年创建，旨在为Parity Games提供一个基准测试套件。这个套件包含了从文献中使用的各种Parity Games，并在线提供。数据集提供了Parity Games的概述，包括它们的生成方式以及它们的结构特性。通过这些特性，作者展示了他们的基准测试是具有代表性的，为Parity Games的进一步实验提供了一个起点。

当前挑战

Parity Games Benchmark Suite面临的挑战包括：1)解决领域问题的挑战，如模型检验、等价性检查和时序逻辑的合成、可满足性和有效性；2)构建过程中的挑战，如Parity Games解决算法的复杂性属于N$P ∩co −NP$，并且没有已知的多项式时间算法，这使得算法评估变得困难。此外，由于缺乏标准的基准测试集，难以比较不同的工具和算法。因此，创建一个多样化的、包含来自不同验证问题的游戏的基准测试集对于比较和评估Parity Games算法至关重要。

常用场景

经典使用场景

Parity Games Benchmark Suite作为模型检查研究中的重要工具，常用于评估和比较不同算法的性能。该数据集包含了从文献中选取的基准游戏，涵盖了各种不同的验证问题，如模型检查、等价性检查、决策过程和合成问题。通过对这些游戏的实验性评估，研究者可以了解算法在实际问题中的表现，从而为算法的改进和优化提供依据。

实际应用

Parity Games Benchmark Suite在实际应用中，可以为模型检查工具的开发和优化提供支持。通过对基准集的测试，开发者可以了解工具在不同类型问题上的表现，从而进行针对性的改进。此外，Parity Games Benchmark Suite还可以用于教学和研究，帮助学生和研究者更好地理解和掌握模型检查技术。

衍生相关工作

Parity Games Benchmark Suite的提出推动了模型检查研究的发展，衍生了许多相关的研究工作。例如，研究者们基于该数据集提出了新的算法和启发式方法，以解决模型检查中的难题。此外，Parity Games Benchmark Suite还促进了不同模型检查工具之间的比较和评估，为工具的改进和优化提供了重要依据。