Counter Simulations via Higher Order Quantifier Elimination: a preliminary report
This work addresses verification challenges for parameterized distributed systems, but it appears incremental as it builds on existing simulation and bisimulation practices.
The paper tackles the verification of distributed systems by providing logical foundations for counter abstractions through a second-order quantifier elimination technique, resulting in a prototype implementation and initial experiments.
Quite often, verification tasks for distributed systems are accomplished via counter abstractions. Such abstractions can sometimes be justified via simulations and bisimulations. In this work, we supply logical foundations to this practice, by a specifically designed technique for second order quantifier elimination. Our method, once applied to specifications of verification problems for parameterized distributed systems, produces integer variables systems that are ready to be model-checked by current SMT-based tools. We demonstrate the feasibility of the approach with a prototype implementation and first experiments.