×

Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes). (English) Zbl 07433024

Summary: 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 S. Gulwani and M. Musuvathi [Lect. Notes Comput. Sci. 4960, 193–207 (2008; Zbl 1133.68318)], 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.

MSC:

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Citations:

Zbl 1133.68318

Software:

VERIFAS; Mcmt; Cubicle
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Baader, F., Ghilardi, S., Tinelli, C.: A new combination procedure for the word problem that generalizes fusion decidability results in modal logics. Inf. Comput. pp. 1413-1452 (2006) · Zbl 1098.03048
[2] Baader, F.; Nipkow, T., Term Rewriting and All That (1998), United Kingdom: Cambridge University Press, United Kingdom · Zbl 0948.68098 · doi:10.1017/CBO9781139172752
[3] Bachmair, L.; Ganzinger, H., Rewrite-based equational theorem proving with selection and simplification, J. Log. Comput., 4, 3, 217-247 (1994) · Zbl 0814.68117 · doi:10.1093/logcom/4.3.217
[4] Bachmair, L.; Ganzinger, H.; Lynch, C.; Snyder, W., Basic paramodulation, Inf. Comput., 121, 2, 172-192 (1995) · Zbl 0833.68115 · doi:10.1006/inco.1995.1131
[5] Bachmair, L.; Ganzinger, H.; Waldmann, U., Refutational theorem proving for hierarchic first-order theories, Appl. Algebra Eng. Commun. Comput., 5, 193-212 (1994) · Zbl 0797.03008 · doi:10.1007/BF01190829
[6] Baumgartner, P.; Waldmann, U., Hierarchic superposition with weak abstraction, Proc. CADE LNCS (LNAI), 7898, 39-57 (2013) · Zbl 1381.03017
[7] Bílková, M., Uniform interpolation and propositional quantifiers in modal logics, Studia Logica, 85, 1, 1-31 (2007) · Zbl 1113.03017 · doi:10.1007/s11225-007-9021-5
[8] Bojańczyk, M., Segoufin, L., Toruńczyk, S.: Verification of database-driven systems via amalgamation. In: Proc. of PODS, pp. 63-74 (2013)
[9] Bruttomesso, R.; Ghilardi, S.; Ranise, S., Quantifier-free interpolation in combinations of equality interpolating theories, ACM Trans. Comput. Log., 15, 1, 5:1-5:34 (2014) · Zbl 1287.03068 · doi:10.1145/2490253
[10] Calvanese, D., De Giacomo, G., Montali, M.: Foundations of data aware process analysis: a database theory perspective. In: Proc. of PODS (2013)
[11] Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Verification of data-aware processes via array-based systems (extended version). Technical Report arXiv:1806.11459 (2018) · Zbl 1495.68129
[12] Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Formal modeling and SMT-based parameterized verification of data-aware BPMN. In: Proc. of BPM, LNCS, vol. 11675, pp. 157-175. Springer (2019) · Zbl 1443.68103
[13] Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: From model completeness to verification of data aware processes. In: Description Logic, Theory Combination, and All That, LNCS, vol. 11560, pp. 212-239. Springer (2019) · Zbl 1443.68103
[14] Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Model completeness, covers and superposition. In: Proc. of CADE, LNCS (LNAI), vol. 11716, pp. 142-160. Springer (2019) · Zbl 07178974
[15] Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Verification of data-aware processes: challenges and opportunities for automated reasoning. In: Proceedings of the 2nd International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE), vol. 311. EPTCS (2019) · Zbl 1443.68103
[16] Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Combined covers and Beth definability. In: Proc. of IJCAR, LNCS (LNAI), vol. 12166, pp. 181-200. Springer (2020) · Zbl 07178974
[17] Calvanese, D.; Ghilardi, S.; Gianola, A.; Montali, M.; Rivkin, A., SMT-based verification of data-aware processes: a model-theoretic approach, Math. Struct. Comput. Sci., 30, 3, 271-313 (2020) · Zbl 1495.68129 · doi:10.1017/S0960129520000067
[18] Chang, CC; Keisler, JH, Model Theory (1990), Amsterdam-London: North-Holland Publishing Co., Amsterdam-London · Zbl 0697.03022
[19] Conchon, S., Goel, A., Krstic, S., Mebsout, A., Zaïdi, F.: Cubicle: a parallel SMT-based model checker for parameterized systems - tool paper. In: Proc. of CAV, pp. 718-724 (2012)
[20] Deutsch, A., Hull, R., Patrizi, F., Vianu, V.: Automatic verification of data-centric business processes. In: Proc. of ICDT, pp. 252-267 (2009)
[21] Deutsch, A., Li, Y., Vianu, V.: Verification of hierarchical artifact systems. In: Proc. of PODS, pp. 179-194. ACM Press (2016)
[22] Ghilardi, S., An algebraic theory of normal forms, Ann. Pure Appl. Logic, 71, 3, 189-245 (1995) · Zbl 0815.03010 · doi:10.1016/0168-0072(93)E0084-2
[23] Ghilardi, S., Model theoretic methods in combined constraint satisfiability, J. Autom. Reason., 33, 3-4, 221-249 (2004) · Zbl 1069.03008 · doi:10.1007/s10817-004-6241-5
[24] Ghilardi, S., Gianola, A.: Interpolation, amalgamation and combination (the non-disjoint signatures case). In: Proc. of FroCoS, LNCS (LNAI), vol. 10483, pp. 316-332. Springer (2017) · Zbl 1495.03054
[25] Ghilardi, S.; Gianola, A., Modularity results for interpolation, amalgamation and superamalgamation, Ann. Pure Appl. Logic, 169, 8, 731-754 (2018) · Zbl 1469.03092 · doi:10.1016/j.apal.2018.04.001
[26] Ghilardi, S., Gianola, A., Kapur, D.: Compactly representing uniform interpolants for EUF using (conditional) DAGS. Technical Report arXiv:2002.09784 (2020)
[27] Ghilardi, S., Gianola, A., Kapur, D.: Computing uniform interpolants for EUF via (conditional) DAG-based compact representations. In: Proc. of CILC, CEUR Workshop Proceedings, vol. 2710, pp. 67-81. CEUR-WS.org (2020)
[28] Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Petri nets with parameterised data - modelling and verification. In: Proc. of BPM, LNCS, vol. 12168, pp. 55-74. Springer (2020) · Zbl 1495.68129
[29] Ghilardi, S., van Gool, S.J.: Monadic second order logic as the model companion of temporal logic. In: Proc. of LICS, pp. 417-426 (2016) · Zbl 1394.03033
[30] Ghilardi, S.; van Gool, SJ, A model-theoretic characterization of monadic second order logic on infinite words, J. Symb. Log., 82, 1, 62-76 (2017) · Zbl 1432.03047 · doi:10.1017/jsl.2016.70
[31] Ghilardi, S., Nicolini, E., Zucchelli, D.: A comprehensive framework for combined decision procedures. ACM Trans. Comput. Log. pp. 1-54 (2008) · Zbl 1171.03306
[32] Ghilardi, S., Ranise, S.: MCMT: A model checker modulo theories. In: Proc. of IJCAR, LNCS (LNAI), vol. 6173, pp. 22-29. Springer (2010) · Zbl 1291.68257
[33] Ghilardi, S., Zawadowski, M.: Sheaves, games, and model completions, Trends in Logic—Studia Logica Library, vol. 14. Kluwer Academic Publishers, Dordrecht (2002). A categorical approach to nonclassical propositional logics · Zbl 1036.03001
[34] Ghilardi, S.; Zawadowski, MW, A sheaf representation and duality for finitely presenting heyting algebras, J. Symb. Log., 60, 3, 911-939 (1995) · Zbl 0837.03047 · doi:10.2307/2275765
[35] Ghilardi, S.; Zawadowski, MW, Undefinability of propositional quantifiers in the modal system S4, Studia Logica, 55, 2, 259-271 (1995) · Zbl 0831.03008 · doi:10.1007/BF01061237
[36] Ghilardi, S.; Zawadowski, MW, Model completions, r-Heyting categories, Ann. Pure Appl. Logic, 88, 1, 27-46 (1997) · Zbl 0888.03024 · doi:10.1016/S0168-0072(97)00012-2
[37] Gulwani, S., Musuvathi, M.: Cover algorithms and their combination. In: Proc. of ESOP, Held as Part of ETAPS, pp. 193-207 (2008) · Zbl 1133.68318
[38] Hoder, K., Bjørner, N.: Generalized property directed reachability. In: Proc. of SAT, pp. 157-171 (2012) · Zbl 1273.68229
[39] Hsiang, J.; Rusinowitch, M., Proving refutational completeness of theorem-proving strategies: the transfinite semantic tree method, J. ACM, 38, 3, 559-587 (1991) · Zbl 0799.68170 · doi:10.1145/116825.116833
[40] Kapur, D.: Shostak’s congruence closure as completion. In: Proc. of RTA, pp. 23-37 (1997) · Zbl 1379.68196
[41] Kapur, D.: Nonlinear polynomials, interpolants and invariant generation for system analysis. In: Proc. of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation co-located with ISSAC (2017)
[42] Kovács, L., Voronkov, A.: Interpolation and symbol elimination. In: Proc. of CADE, LNCS (LNAI), vol. 5663, pp. 199-213. Springer (2009) · Zbl 1250.68193
[43] Kowalski, T.; Metcalfe, G., Uniform interpolation and coherence, Ann. Pure Appl. Logic, 170, 7, 825-841 (2019) · Zbl 07049926 · doi:10.1016/j.apal.2019.02.004
[44] Li, Y.; Deutsch, A.; Vianu, V., VERIFAS: a practical verifier for artifact systems, PVLDB, 11, 3, 283-296 (2017)
[45] Lipparini, P.: Locally finite theories with model companion. In: Atti della Accademia Nazionale dei Lincei. Classe di Scienze Fisiche, Matematiche e Naturali. Rendiconti, Serie 8, vol. 72. Accademia Nazionale dei Lincei (1982) · Zbl 0524.03021
[46] Ludwig, M., Waldmann, U.: An extension of the Knuth-Bendix ordering with lPO-like properties. In: Proc. of LPAR, pp. 348-362 (2007) · Zbl 1137.03306
[47] McMillan, K.L.: Lazy abstraction with interpolants. In: Proc. of CAV, pp. 123-136 (2006) · Zbl 1188.68196
[48] Nelson, G.; Oppen, DC, Fast decision procedures based on congruence closure, J. ACM, 27, 2, 356-364 (1980) · Zbl 0441.68111 · doi:10.1145/322186.322198
[49] Nicolini, E., Ringeissen, C., Rusinowitch, M.: Data structures with arithmetic constraints: a non-disjoint combination. In: Proc. of FroCoS, LNCS (LNAI), vol. 5749, pp. 319-334. Springer (2009) · Zbl 1193.68090
[50] Nicolini, E., Ringeissen, C., Rusinowitch, M.: Satisfiability procedures for combination of theories sharing integer offsets. In: Proc. of TACAS, LNCS, vol. 5505, pp. 428-442. Springer (2009) · Zbl 1234.68262
[51] Nicolini, E., Ringeissen, C., Rusinowitch, M.: Combining satisfiability procedures for unions of theories with a shared counting operator. Fund. Inform. pp. 163-187 (2010) · Zbl 1215.03051
[52] Nieuwenhuis, R.; Oliveras, A., Fast congruence closure and extensions, Inf. Comput., 205, 4, 557-580 (2007) · Zbl 1112.68116 · doi:10.1016/j.ic.2006.08.009
[53] Nieuwenhuis, R.; Rubio, A., Theorem proving with ordering and equality constrained clauses, J. Symb. Comput., 19, 4, 321-351 (1995) · Zbl 0844.68107 · doi:10.1006/jsco.1995.1020
[54] Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Handbook of Automated Reasoning (in 2 volumes), pp. 371-443. MIT Press (2001) · Zbl 0997.03012
[55] Pitts, AM, On an interpretation of second order quantification in first order intuitionistic propositional logic, J. Symb. Log., 57, 1, 33-52 (1992) · Zbl 0763.03009 · doi:10.2307/2275175
[56] Robinson, A., On the Metamathematics of Algebra. Studies in Logic and the Foundations of Mathematics (1951), Amsterdam: North-Holland Publishing Co., Amsterdam · Zbl 0043.24702
[57] Rybina, T., Voronkov, A.: A logical reconstruction of reachability. In: Perspectives of Systems Informatics, 5th International Andrei Ershov Memorial Conference, PSI 2003, Revised Papers, pp. 222-237 (2003) · Zbl 1254.68153
[58] Shavrukov, V.: Subalgebras of diagonalizable algebras of theories containing arithmetic. Dissertationes Mathematicae CCCXXIII (1993) · Zbl 0803.03044
[59] Sofronie-Stokkermans, V.: On interpolation and symbol elimination in theory extensions. In: Proc. of IJCAR, LNCS (LNAI), vol. 9706, pp. 273-289. Springer (2016) · Zbl 1476.03042
[60] Sofronie-Stokkermans, V.: On interpolation and symbol elimination in theory extensions. Log. Methods Comput. Sci. 14(3) (2018) · Zbl 1476.03043
[61] Vianu, V.: Automatic verification of database-driven systems: a new frontier. In: Proc. of ICDT, pp. 1-13 (2009)
[62] van Gool, SJ; Metcalfe, G.; Tsinakis, C., Uniform interpolation and compact congruences, Ann. Pure Appl. Logic, 168, 10, 1927-1948 (2017) · Zbl 1422.03061 · doi:10.1016/j.apal.2017.05.001
[63] Visser, A.: Uniform interpolation and layered bisimulation. In: P. Hájek (ed.) Gödel 96: logical foundations on mathematics, computer science and physics - Kurt Gödel’s legacy. Springer Verlag (1996) · Zbl 0854.03026
[64] Wheeler, WH, Model-companions and definability in existentially complete structures, Israel J. Math., 25, 3-4, 305-330 (1976) · Zbl 0398.03023 · doi:10.1007/BF02757007
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.