کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
422021 | 685001 | 2008 | 16 صفحه PDF | دانلود رایگان |

We describe a parallel algorithm for solving parity games, with applications in, e.g., modal μ-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 μ-calculus model checking problems for a set of communication protocols, randomly generated problem instances, and parametric problem instances from the literature.
Journal: Electronic Notes in Theoretical Computer Science - Volume 220, Issue 2, 11 December 2008, Pages 19-34