Abstract The symmetric strict implication calculus $\mathsf{S}^{2}\mathsf{IC}$ is a modal calculus for compact Hausdorff spaces. This is established through de Vries duality, linking compact Hausdorff spaces with de Vries algebras—complete Boolean algebras equipped with a special relation. Modal compact Hausdorff spaces are compact Hausdorff spaces enriched with a continuous relation. These spaces correspond, via modalized de Vries duality, to upper continuous modal de Vries algebras. In this paper, we introduce the modal symmetric strict implication calculus $\mathsf{MS}^{2}\mathsf{IC}$, which extends $\mathsf{S}^{2}\mathsf{IC}$. We prove that $\mathsf{MS}^{2}\mathsf{IC}$ is strongly sound and complete with respect to upper continuous modal de Vries algebras, thereby providing a logical calculus for modal compact Hausdorff spaces. We also develop a relational semantics for $\mathsf{MS}^{2}\mathsf{IC}$ that we employ to show admissibility of various $\Pi_{2}$-rules in this system.

Abstract We analyze the theory of rational trees with finitely many constructors, infinitely many atoms and an atomicity predicate. We design a new decision procedure, proving in addition that this theory is model-complete. We also show that the enrichment of the language with selectors and simultaneous parametric fixpoints enjoys quantifier elimination.

Modeling and verification of dynamic systems operating over a relational representation of states are increasingly investigated problems in AI, Business Process Management and Database Theory. To make these systems amenable to verification, the amount of information stored in each state needs to be bounded, or restrictions are imposed on the preconditions and effects of actions. We lift these restrictions by introducing the framework of Relational Action Bases (RABs), which generalizes existing frameworks and in which unbounded relational states are evolved through actions that can (1) quantify both existentially and universally over the data, and (2) use arithmetic constraints. We then study parameterized safety of RABs via (approximated) SMT-based backward search, singling out essential meta-properties of the resulting procedure, and showing how it can be realized by an off-the-shelf combination of existing verification modules of the state-of-the-art MCMT model checker. We demonstrate the effectiveness of this approach on a benchmark of data-aware business processes. Finally, we show how universal invariants can be exploited to make this procedure fully correct.

In this article, we enrich McCarthy’s theory of extensional arrays with a length and a maxdiff operation. As is well-known, some diff operation (i.e., some kind of difference function showing where two unequal arrays differ) is needed to keep interpolants quantifier free in array theories. Our maxdiff operation returns the max index where two arrays differ; thus, it has a univocally determined semantics. The length function is a natural complement of such a maxdiff operation and is needed to handle real arrays. Obtaining interpolation results for such a rich theory is a surprisingly hard task. We get such results via a thorough semantic analysis of the models of the theory and of their amalgamation and strong amalgamation properties. The results are modular with respect to the index theory; we show how to convert them into concrete interpolation algorithms via a hierarchical approach realizing a polynomial reduction to interpolation in linear arithmetics endowed with free function symbols.

Abstract Uniform interpolants were largely studied in non-classical propositional logics since the nineties, and their connection to model completeness was pointed out in the literature. A successive parallel research line inside the automated reasoning community investigated uniform quantifier-free interpolants (sometimes referred to as “covers”) in first-order theories. 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 needed to transfer quantifier-free interpolation (i.e., the equality interpolating property, aka strong amalgamation property). The key feature of our algorithm relies on the extensive usage of the Beth definability property for primitive fragments to convert implicitly defined variables into their explicitly defining terms. 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 ‘tame combinations’) concern multi-sorted theories arising in many model-checking applications (in particular, the ones oriented to verification of data-aware processes).

The concept of uniform interpolant for a quantifier-free formula from a given formula with a list of symbols, while well-known in the logic literature, has been unknown to the formal methods and automated reasoning community for a long time. This concept is precisely defined. Two algorithms for computing quantifier-free uniform interpolants in the theory of equality over uninterpreted symbols (EUF) endowed with a list of symbols to be eliminated are proposed. The first algorithm is non-deterministic and generates a uniform interpolant expressed as a disjunction of conjunctions of literals, whereas the second algorithm gives a compact representation of a uniform interpolant as a conjunction of Horn clauses. Both algorithms exploit efficient dedicated DAG representations of terms. Correctness and completeness proofs are supplied, using arguments combining rewrite techniques with model theory.

Since the nineties, the Man-in-The-Middle (MITM) attack has been one of the most effective strategies adopted for compromising information security in network environments. In this article, we focus our attention on ARP cache poisoning, which is one of the most well-known and more adopted techniques for performing MITM attacks in Ethernet local area networks. More precisely, we will prove that, in network environments with at least one malicious host in the absence of cryptography, an ARP cache poisoning attack cannot be avoided. Subsequently, we advance ArpON, an efficient and effective solution to counteract ARP cache poisoning, and we use a model-checker for verifying its safety property. Our main finding, in accordance with the above impossibility result, is that the only event that compromises the safety of ArpON is a cache poisoning that nevertheless is removed by ArpON itself after a very short period, thus making it practically infeasible to perpetrate an ARP cache poisoning attack on network hosts where ArpON is installed.

Abstract In this paper, the theory of McCarthy’s extensional arrays enriched with a maxdiff operation (this operation returns the biggest index where two given arrays differ) is proposed. It is known from the literature that a diff operation is required for the theory of arrays in order to enjoy the Craig interpolation property at the quantifier-free level. However, the diff operation introduced in the literature is merely instrumental to this purpose and has only a purely formal meaning (it is obtained from the Skolemization of the extensionality axiom). Our maxdiff operation significantly increases the level of expressivity; however, obtaining interpolation results for the resulting theory becomes a surprisingly hard task. We obtain such results via a thorough semantic analysis of the models of the theory and of their amalgamation properties. The results are modular with respect to the index theory and it is shown how to convert them into concrete interpolation algorithms via a hierarchical approach.

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.

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.

Abstract 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.

Abstract Ruitenburg’s Theorem says that every endomorphismfof a finitely generated free Heyting algebra is ultimately periodic ifffixes all the generators but one. More precisely, there isN≥ 0 such thatfN+2=fN, thus the period equals 2. We give a semantic proof of this theorem, using duality techniques and bounded bisimulation ranks. By the same techniques, we tackle investigation of arbitrary endomorphisms of free algebras. We show that they are not, in general, ultimately periodic. Yet, when they are (e.g. in the case of locally finite subvarieties), the period can be explicitly bounded as function of the cardinality of the set of generators.

It follows from known results in the literature that least and greatest fixed-points of monotone polynomials on Heyting algebras—that is, the algebraic models of the Intuitionistic Propositional Calculus—always exist, even when these algebras are not complete as lattices. The reason is that these extremal fixed-points are definable by formulas of the IPC . Consequently, the μ-calculus based on intuitionistic logic is trivial, every μ-formula being equivalent to a fixed-point free formula. In the first part of this article, we give an axiomatization of least and greatest fixed-points of formulas, and an algorithm to compute a fixed-point free formula equivalent to a given μ-formula. The axiomatization of the greatest fixed-point is simple. The axiomatization of the least fixed-point is more complex, in particular every monotone formula converges to its least fixed-point by Kleene’s iteration in a finite number of steps, but there is no uniform upper bound on the number of iterations. The axiomatization yields a decision procedure for the μ-calculus based on propositional intuitionistic logic. The second part of the article deals with closure ordinals of monotone polynomials on Heyting algebras and of intuitionistic monotone formulas; these are the least numbers of iterations needed for a polynomial/formula to converge to its least fixed-point. Mirroring the elimination procedure, we show how to compute upper bounds for closure ordinals of arbitrary intuitionistic formulas. For some classes of formulas, we provide tighter upper bounds that, in some cases, we prove exact.

Abstract The variety of Brouwerian semilattices is amalgamable and locally finite; hence, by well-known results [19], it has a model completion (whose models are the existentially closed structures). In this article, we supply a finite and rather simple axiomatization of the model completion.

We present our efforts on the formalization and automated formal verification of data-intensive applications based on the Storm technology, a well known and pioneering framework for developing streaming applications. The approach is based on the so-called array-based systems formalism, introduced by Ghilardi et al., a suitable abstraction of infinite-state systems that we used to model the runtime behavior of Storm-based applications. The formalization consists of quantified formulae belonging to a certain fragment of first-order logic to symbolically represent array-based systems.The formalization consists of quantified first-order formulae symbolically representing array-based systems. The verification consists in checking whether some safety property holds or not for the system. Both formalization and verification are performed in the same framework, namely the state-of-the-art Cubicle model checker.

We present our framework for the verification of parameterized infinite-state systems. The framework has been successfully applied in the verification of heterogeneous systems, ranging from distributed fault-tolerant protocols to programs handling unbounded data-structures. In such application doma ins, being able to infer quantified invariants is a mandatory requirement for successful results. Our framework differentiates itself from the state-of-the-art solutions targeting the generation of quantified safe inductive invariants: instead of monolitically exploiting a single static analysis technique, it is based on the effective integration of several analysis strategies. The paper targets the description of the engineering strategies adopted for a successful implementation of such an integrated framework, and presents the extensive experimental evaluation demonstrating its effectiveness.

Abstract 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 investigate proof-theoretic properties of hypersequent calculi for intermediate logics using algebraic methods. More precisely, we consider a new weakly analytic subformula property (the bounded proof property) of such calculi. Despite being strictly weaker than both cut-elimination and the subformula property, this property is sufficient to ensure decidability of finitely axiomatized calculi. We introduce one-step Heyting algebras and establish a semantic criterion characterizing calculi for intermediate logics with the bounded proof property and the finite model property in terms of one-step Heyting algebras. Finally, we show how this semantic criterion can be applied to a number of calculi for well-known intermediate logics such as LC,KC and BD2⁠.

The main focus of this paper is on bisimulation-invariant MSO, and more particularly on giving a novel model-theoretic approach to it. In model theory, a model companion of a theory is a first-order description of the class of models in which all potentially solvable systems of equations and non-equations have solutions. We show that bisimulation-invariant MSO on trees gives the model companion for a new temporal logic, "fair CTL", an enrichment of CTL with local fairness constraints. To achieve this, we give a completeness proof for the logic fair CTL which combines tableaux and Stone duality, and a fair CTL encoding of the automata for the modal μ-calculus. Moreover, we also show that MSO on binary trees is the model companion of binary deterministic fair CTL.

The use of interpolants in verification is gaining more and more importance. Since theories used in applications are usually obtained as (disjoint) combinations of simpler theories, it is important to modularly reuse interpolation algorithms for the component theories. We show that a sufficient and necessary condition to do this for quantifier-free interpolation is that the component theories have the strong ( sub -) amalgamation property. Then, we provide an equivalent syntactic characterization and show that such characterization covers most theories commonly employed in verification. Finally, we design a combined quantifier-free interpolation algorithm capable of handling both convex and nonconvex theories; this algorithm subsumes and extends most existing work on combined interpolation.

Most of the research on temporalized Description Logics (DLs) has concentrated on the case where temporal operators can be applied to concepts, and sometimes additionally to TBox axioms and ABox assertions. The aim of this article is to study temporalized DLs where temporal operators on TBox axioms and ABox assertions are available, but temporal operators on concepts are not. While the main application of existing temporalized DLs is the representation of conceptual models that explicitly incorporate temporal aspects, the family of DLs studied in this article addresses applications that focus on the temporal evolution of data and of ontologies. Our results show that disallowing temporal operators on concepts can significantly decrease the complexity of reasoning. In particular, reasoning with rigid roles (whose interpretation does not change over time) is typically undecidable without such a syntactic restriction, whereas our logics are decidable in elementary time even in the presence of rigid roles. We analyze the effects on computational complexity of dropping rigid roles, dropping rigid concepts, replacing temporal TBoxes with global ones, and restricting the set of available temporal operators. In this way, we obtain a novel family of temporalized DLs whose complexity ranges from 2- ExpTime-complete via NExpTime-complete to ExpTime-complete.

The use of interpolants in model checking is becoming an enabling technology to allow fast and robust verification of hardware and software. The application of encodings based on the theory of arrays, however, is limited by the impossibility of deriving quantifier-free interpolants in general. In this paper, we show that, with a minor extension to the theory of arrays, it is possible to obtain quantifier-free interpolants. We prove this by designing an interpolating procedure, based on solving equations between array updates. Rewriting techniques are used in the key steps of the solver and its proof of correctness. To the best of our knowledge, this is the first successful attempt of computing quantifier-free interpolants for a theory of arrays.

We define a general notion of a fragment within higher-order type theory; a procedure for constraint satisfiability in combined fragments is outlined, following Nelson-Oppen schema. The procedure is in general only sound, but it becomes terminating and complete when the shared fragment enjoys suitable noetherianity conditions and admits an abstract version of a “Keisler-Shelah-like” isomorphism theorem. We show that this general decidability transfer result covers recent work on combination in first-order theories as well as in various intensional logics such as description, modal, and temporal logics.

Abstract Basically, the connection of two many-sorted theories is obtained by taking their disjoint union, and then connecting the two parts through connection functions that must behave like homomorphisms on the shared signature. We determine conditions under which decidability of the validity of universal formulae in the component theories transfers to their connection. In addition, we consider variants of the basic connection scheme. Our results can be seen as a generalization of the so-called -connection approach for combining modal logics to an algebraic setting.

Abstract. We characterize (both from a syntactic and an algebraic point of view) the normalK4-logics for which unification is filtering. We also give a sufficient semantic criterion for existence of most general unifiers, covering natural extensions ofK4.2+(i.e., of the modal system obtained fromK4 by adding to it, as a further axiom schemata, the modal translation of the weak excluded middle principle).

Abstract We show that the variety of Heyting algebras has finitary unification type. We also show that the subvariety obtained by adding it De Morgan law is the biggest variety of Heyting algebras having unitary unification type. Proofs make essential use of suitable characterizations (both from the semantic and the syntactic side) of finitely presented projective algebras.

We introduce an algebraic approach to E-unification, through the notions of finitely presented and projective object. As applications and examples, we determine the unification type of varieties generated by a single finite quasi-primal algebra, of distributive lattices and of some other equational classes of algebras corresponding to fragments of intuitionistic logic.

Abstract In this paper we study the logic of relational and partial variable sets, seen as a generalization of set-valued presheaves, allowing transition functions to be arbitrary relations or arbitrary partial functions. We find that such a logic is the usual intuitionistic and co-intuitionistic first order logic without Beck and Frobenius conditions relative to quantifiers along arbitrary terms. The important case of partial variable sets is axiomatizable by means of the substitutivity schema for equality. Furthermore, completeness, incompleteness and independence results are obtained for different kinds of Beck and Frobenius conditions.

Abstract A. M.Pitts in [Pi] proved that is a bi-Heyting category satisfying the Lawvere condition. We show that the embedding Φ: → Sh(P0, J0) into the topos of sheaves, (P0 is the category of finite rooted posets and open maps, J0 the canonical topology on P0) given by H ↦ HA(H, (−)) : P0 → Set preserves the structure mentioned above, finite coproducts, and subobject classifier; it is also conservative. This whole structure on can be derived from that of Sh(P0, J0) via the embedding Φ. We also show that the equivalence relations in are not effective in general. On the way to these results we establish a new kind of duality between and a category of sheaves equipped with certain structure defined in terms of Ehrenfeucht games. Our methods are model-theoretic and combinatorial as opposed to proof-theoretic as in [Pi].

Abstract By means of models in toposes of C-sets (where C is a small category), necessary conditions are found for the minimum quantified extension of a propositional (intermediate, modal) logic to be complete with respect to Kripke semantics; in particular, many well-known systems turn out to be incomplete.