Higher-Order Quantifier Elimination, Counter Simulations and Fault-Tolerant Systems
- PDF / 557,662 Bytes
- 36 Pages / 439.37 x 666.142 pts Page_size
- 104 Downloads / 229 Views
Higher-Order Quantifier Elimination, Counter Simulations and Fault-Tolerant Systems Silvio Ghilardi1
· Elena Pagani2
Received: 3 January 2019 / Accepted: 5 August 2020 © The Author(s) 2020
Abstract We develop quantifier elimination procedures for fragments of higher order logic arising from the formalization of distributed systems (especially of fault-tolerant ones). Such procedures can be used in symbolic manipulations like the computation of pre/post images and of projections. We show in particular that our procedures are quite effective in producing counter abstractions that can be model-checked using standard SMT technology. In fact, very often in the current literature 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 our technique for second order quantifier elimination. We implemented our procedure for a simplified (but still expressive) subfragment and we showed that our method is able to successfully handle verification benchmarks from various sources with interesting performances. Keywords 2nd order quantifier elimination · Satisfiability Modulo theories · Verification of parameterized distributed systems · Counter abstractions
1 Introduction There is an increasing interest concerning algorithmic methods (and, in particular, quantifier elimination methods) applying to second order logic, as witnessed by recent dedicated workshops [40]. Quoting from the textbook [25] “In recent years there has been an increasing use of logical methods and significant new developments have been spawned in several areas of computer science, ranging from artificial intelligence and software engineering to agent-
Electronic supplementary material The online version of this article (https://doi.org/10.1007/s10817-02009578-5) contains supplementary material, which is available to authorized users.
B
Elena Pagani [email protected] Silvio Ghilardi [email protected]
1
Università degli Studi di Milano, Via C. Saldini 50, 20133 Milan, Italy
2
Università degli Studi di Milano, Via G. Celoria 18, 20133 Milan, Italy
123
S. Ghilardi, E. Pagani
based systems and the semantic web. In the investigation and application of logical methods there is a tension between: (i) the need for a representational language strong enough to express domain knowledge of a particular application, and the need for a logical formalism general enough to unify several reasoning facilities relevant to the application, on the one hand, and (ii) the need to enable computationally feasible reasoning facilities, on the other hand. Second-order logics are very expressive and allow us to represent domain knowledge with ease, but there is a high price to pay for the expressiveness. Most second-order logics are incomplete and highly undecidable. It is the quantifiers which bind relation symbols that make second-order logics computationally unfriendly. It is therefore d
Data Loading...
