Counter Simulations via Higher Order Quantifier Elimination: a preliminary report

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 quant...

Full description

Bibliographic Details
Main Authors: Silvio Ghilardi, Elena Pagani
Format: Article
Language:English
Published: Open Publishing Association 2017-12-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1712.01487v1