Output details
11 - Computer Science and Informatics
Royal Holloway, University of London
A saturation method for the modal μ-calculus over pushdown systems
<07>This paper was an invited (peer reviewed) Information and Computation submission of a Concur 2009 article. It solves a 12 year open problem (a partial solution first appeared in "Reachability Analysis of Pushdown Automata" in Concur 1997). The work was later implemented in PDSolver (http://www.cs.rhul.ac.uk/~hague/files/implementations/pdsolver.html), presented at SPIN 2010. The paper introduces new techniques later used by the author to develop an algorithm (in ICALP 2012) underpinning the new C-SHORe tool (http://www.cshore.cs.rhul.ac.uk), which forms the basis of a recent EPSRC Early Career Fellowship awarded to the author (EP/K009907/1).