Quantifier elimination

Project and Conquer: Fast Quantifier Elimination for Checking Petri Net Reachability

We propose a method for checking generalized reachability properties in Petri nets that takes advantage of structural reductions and that can be used, transparently, as a pre-processing step of existing model-checkers. Our approach is based on a new …