Uniform interpolants have been largely studied in non-classical propositional logics since the nineties; a successive research line within the automated reasoning community investigated uniform quantifier-free interpolants (sometimes referred to as "covers") in first-order theories. This further research line is motivated by the fact that uniform interpolants offer an effective solution to tackle quantifier elimination and symbol elimination problems, which are central in model checking infinite state systems. This was first pointed out in ESOP 2008 by Gulwani and Musuvathi, and then by the authors of the present contribution in the context of recent applications to the verification of data-aware processes. In this paper, we show how covers are strictly related to model completions, a well-known topic in model theory. We also investigate the computation of covers within the Superposition Calculus, by adopting a constrained version of the calculus and by defining appropriate settings and reduction strategies. In addition, we show that computing covers is computationally tractable for the fragment of the language used when tackling the verification of data-aware processes. This observation is confirmed by analyzing the preliminary results obtained using the mcmt tool to verify relevant examples of data-aware processes. These examples can be found in the last version of the tool distribution.

Model Completeness, Uniform Interpolants and Superposition Calculus (With Applications to Verification of Data-Aware Processes) / D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, A. Rivkin. - In: JOURNAL OF AUTOMATED REASONING. - ISSN 0168-7433. - 65:7(2021), pp. 941-969. [10.1007/s10817-021-09596-x]

Model Completeness, Uniform Interpolants and Superposition Calculus (With Applications to Verification of Data-Aware Processes)

S. Ghilardi;
2021

Abstract

Uniform interpolants have been largely studied in non-classical propositional logics since the nineties; a successive research line within the automated reasoning community investigated uniform quantifier-free interpolants (sometimes referred to as "covers") in first-order theories. This further research line is motivated by the fact that uniform interpolants offer an effective solution to tackle quantifier elimination and symbol elimination problems, which are central in model checking infinite state systems. This was first pointed out in ESOP 2008 by Gulwani and Musuvathi, and then by the authors of the present contribution in the context of recent applications to the verification of data-aware processes. In this paper, we show how covers are strictly related to model completions, a well-known topic in model theory. We also investigate the computation of covers within the Superposition Calculus, by adopting a constrained version of the calculus and by defining appropriate settings and reduction strategies. In addition, we show that computing covers is computationally tractable for the fragment of the language used when tackling the verification of data-aware processes. This observation is confirmed by analyzing the preliminary results obtained using the mcmt tool to verify relevant examples of data-aware processes. These examples can be found in the last version of the tool distribution.
Covers; Uniform interpolation; Model completeness; Superposition calculus; Verification of data-aware processes
Settore MAT/01 - Logica Matematica
Article (author)
File in questo prodotto:
File Dimensione Formato  
main.pdf

accesso aperto

Tipologia: Pre-print (manoscritto inviato all'editore)
Dimensione 463.57 kB
Formato Adobe PDF
463.57 kB Adobe PDF Visualizza/Apri
Calvanese2021_Article_ModelCompletenessUniformInterp.pdf

accesso aperto

Tipologia: Publisher's version/PDF
Dimensione 525.94 kB
Formato Adobe PDF
525.94 kB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

Caricamento pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/2434/866500
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? 4
social impact