Combined Covers and Beth Definability (Extended Version)

Technical Report, arXiv.org e-Print archive. CoRR Technical Report arXiv:1911.07774 2020. Available at https://arxiv.org/abs/1911.07774.

In ESOP 2008, Gulwani and Musuvathi introduced a notion of cover and exploited it to handle infinite-state model checking problems. Motivated by applications to the verification of data-aware processes, we proved in a previous paper that covers are strictly related to model completions, a well-known topic in model theory. In this paper we investigate cover transfer to theory combinations in the disjoint signatures case. We prove that for convex theories, cover algorithms can be transferred to theory combinations under the same hypothesis (equality interpolation property aka strong amalgamation property) needed to transfer quantifier-free interpolation. In the non-convex case, we show by a counterexample that covers may not exist in the combined theories, even in case combined quantifier-free interpolants do exist. However, we exhibit a cover transfer algorithm operating also in the non-convex case for special kinds of theory combinations; these combinations (called àt me combinations') concern multi-sorted theories arising in many model-checking applications (in particular, the ones oriented to verification of data-aware processes).

@techreport{arXiv-2020-combined-covers,
   title = "Combined Covers and Beth Definability (Extended Version)",
   year = "2020",
   author = "Diego Calvanese and Silvio Ghilardi and Alessandro Gianola and
Marco Montali and Andrey Rivkin",
   institution = "arXiv.org e-Print archive",
   number = "arXiv:1911.07774",
   note = "Available at https://arxiv.org/abs/1911.07774",
}