Parity games

A set of parity games for benchmarking purposes. See https://github.com/jkeiren/paritygame-generator Model checking: Parity games encoding model checking problems.Equivalence checking: Parity games encoding equivalence checking problems.PGSolver: Parity games generated using PGSolver. These include: random games, and games that are hard for certain algorithms.MLSolver Parity games generated using MLSolver. These are games that encode satisfiability and validity problems for modal logics.Data (YAML) This is a file in YAML format that includes high-level information about <em>all</em> parity games described before. Detailed (structural) information about the games can be found as separate YAML files in the respectipe ZIP archives.Data (SQLite) This contains a database in SQLite format that was derived from the YAML files provided in the archives, and the previous data file. The sole purpose of this derived data is to enable efficient plotting of results. The plots in the paper have been based on this file.

本数据集为一套用于基准测试的偶对博弈（parity games）集合，详见 https://github.com/jkeiren/paritygame-generator。
模型检测：用于编码模型检测问题的偶对博弈。
等价性验证：用于编码等价性验证问题的偶对博弈。
PGSolver生成偶对博弈：通过PGSolver工具生成的偶对博弈，包含随机生成博弈以及针对特定算法具有高复杂度的博弈。
MLSolver生成偶对博弈：通过MLSolver工具生成的偶对博弈，此类博弈用于编码模态逻辑的可满足性与有效性判定问题。
YAML格式数据：该文件采用YAML格式，包含前文所述全部偶对博弈的高层级元信息。各博弈的详细（结构）信息可在对应ZIP压缩包内的独立YAML文件中获取。
SQLite格式数据：该数据集包含基于归档内YAML文件与前述数据文件衍生得到的SQLite格式数据库。此衍生数据的唯一用途是支持高效的结果绘图，论文中的实验绘图均基于该文件生成。