A Multi-Core Solver for Parity Games

作     者：van de Pol, Jaco Weber, Michael 

作者机构：Univ Twente Formal Methods & Tools Enschede Netherlands 

出 版 物：《ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE》 (理论计算机科学电子札记)

年 卷 期：2008年第220卷第2期

页      面：19-34页

核心收录：

学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：Netherlands Organisation for Scientific Research (NWO) under FOCUS/BRICKS [642.000.05N09] 

主　　题：parity games boolean equation systems model checking multi-core algorithm mu-calculus 

摘      要：We describe a parallel algorithm for solving parity games, with applications in, e.g., modal mu-calculus model checking with arbitrary alternations, and (branching) bisimulation checking. The algorithm is based on Jurdzinski s Small Progress Measures. Actually, this is a class of algorithms, depending on a selection heuristics. Our algorithm operates lock-free, and mostly wait-free (except for infrequent termination detection), and thus allows maximum parallelism. Additionally, we conserve memory by avoiding storage of predecessor edges for the parity graph through strictly forward-looking heuristics. We evaluate our multi-core implementation s behaviour on parity games obtained from mu-calculus model checking problems for a set of communication protocols, randomly generated problem instances, and parametric problem instances from the literature.