Pushdown Solver

Tool for computing the winning region of pushdown parity games or mu-calculus formulas over pushdown systems. May be analysed as games or directly evaluate formulas.

More details and a user guide available here. This repository contains PDSolver-1.1.1.tgz and PDSolver-examples-1.0.0.tgz.

Based on papers by M. Hague and C.-H. L. Ong in Spin 2010 and Information and Computation 2010.

Also implemented are reachability games using a corrected version of Schwoon et al (ATVA 2006) (similar to Broadbent et al (ICFP 2013)). Least fixed-point mu-calculus problems can be converted to reachability also.

Additional implementation: pushdown parity translation to a reachability game that is the negation of the original game (use -ct safety). Hence constructs Abelards winning region. I.e. a positive answer means Abelard can have win the parity game.