An implementation of a polynomial time under-approximation framework for solving parity games is presented. The aim of the framework is to provide a tool for local model checking and a user interface for researchers studying algorithms for solving parity games. The implementation is done in Java with a supporting infrastructure using agents and servers to conduct data mining on statistical patterns found with various characterizations and features of parity games.
The framework offers the advantage of allowing algorithms with different characteristics to be combined for systematically studying their strengths and interactions and for exploiting their differences. Redundancies in computational power of an algorithm against problems can be revealed by the framework and avoided when this framework is used as a pre-processor for algorithm whose worst case running time is exponential. We also give an analysis of various components in this framework on their strengths and interactions. Relevance of 0-1 laws and a descriptive complexity measure "entanglement" are also studied.
pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.