In recent times, satisfiability modulo theories (SMT) techniques gained increasing attention and obtained remarkable success in model-checking infinite-state systems. Still, we believe that whenever more expressivity is needed in order to specify the systems to be verified, more and more support is needed from mathematical logic and model theory. This is the case of the applications considered in this paper: we study verification over a general model of relational, data-aware processes, to assess (parameterized) safety properties irrespectively of the initial database (DB) instance. Toward this goal, we take inspiration from array-based systems and tackle safety algorithmically via backward reachability. To enable the adoption of this technique in our rich setting, we make use of the model-theoretic machinery of model completion, which surprisingly turns out to be an effective tool for verification of relational systems and represents the main original contribution of this paper. In this way, we pursue a twofold purpose. On the one hand, we isolate three notable classes for which backward reachability terminates, in turn witnessing decidability. Two of such classes relate our approach to conditions singled out in the literature, whereas the third one is genuinely novel. On the other hand, we are able to exploit SMT technology in implementations, building on the well-known MCMT (Model Checker Modulo Theories) model checker for array-based systems and extending it to make all our foundational results fully operational. All in all, the present contribution is deeply rooted in the long-standing tradition of the application of model theory in computer science. In particular, this paper applies these ideas in an original mathematical context and shows how these techniques can be used for the first time to empower algorithmic techniques for the verification of infinite-state systems based on arrays, so as to make such techniques applicable to the timely, challenging settings of data-aware processes.

We prove model completeness for the expansion of the real field by the Weierstrass ℘ function as a function of the variable z and the parameter (or period) τ. We need to existentially define the partial derivatives of the ℘ function with respect to the variable z and the parameter τ. To obtain this result, it is necessary to include in the structure function symbols for the unrestricted exponential function and restricted sine function, the Weierstrass ζ function and the quasi-modular form E2 (we conjecture that these functions are not existentially definable from the functions ℘ alone or even if we use the exponential and restricted sine functions). We prove some auxiliary model-completeness results with the same functions composed with appropriate change of variables. In the conclusion, we make some remarks about the non-effectiveness of our proof and the difficulties to be overcome to obtain an effective model-completeness result, and how to extend these results to appropriate expansion of the real field by automorphic forms.

Monadic second order logic and linear temporal logic are two logical formalisms that can be used to describe classes of infinite words, i.e., first-order models based on the natural numbers with order, successor, and finitely many unary predicate symbols.

Monadic second order logic over infinite words (S1S) can alternatively be described as a first-order logic interpreted in ${\cal P}\left( \omega \right)$, the power set Boolean algebra of the natural numbers, equipped with modal operators for ‘initial’, ‘next’, and ‘future’ states. We prove that the first-order theory of this structure is the model companion of a class of algebras corresponding to a version of linear temporal logic (LTL) without until.

The proof makes crucial use of two classical, nontrivial results from the literature, namely the completeness of LTL with respect to the natural numbers, and the correspondence between S1S-formulas and Büchi automata.

We let R be an o-minimal expansion of a field, V a convex subring, and (R0,V0) an elementary substructure of (R,V). Our main result is that (R,V) considered as a structure in a language containing constants for all elements of R0 is model complete relative to quantifier elimination in R, provided that kR (the residue field with structure induced from R) is o-minimal. Along the way we show that o-minimality of kR implies that the sets definable in kR are the same as the sets definable in k with structure induced from (R,V). We also give a criterion for a superstructure of (R,V) being an elementary extension of (R,V).

A box type is an n-type of an o-minimal structure which is uniquely determined by the projections to the coordinate axes. We characterize heirs of box types of a polynomially bounded o-minimal structure M. From this, we deduce various structure theorems for subsets of Mk, definable in the expansion of M by all convex subsets of the line. We show that after naming constants, is model complete provided M is model complete.

We show that the field of real numbers with multisummable real power series is model complete, o-minimal and polynomially bounded. Further expansion by the exponential function yields again a model complete and o-minimal structure which is exponentially bounded, and in which the Gamma function on the positive real line is definable. 2000 Mathematics Subject Classification: primary 03C10, 32B05, 32B20; secondary, 26E05.