Being Correct Is Not Enough: Efficient Verification Using Robust Linear Temporal Logic

While most approaches in formal methods address system correctness, ensuring robustness has remained a challenge. In this article, we present and study the logic rLTL, which provides a means to formally reason about both correctness and robustness in system design. Furthermore, we identify a large fragment of rLTL for which the verification problem can be efficiently solved, i.e., verification can be done by using an automaton, recognizing the behaviors described by the rLTL formula φ, of size at most O(3 |φ |), where |φ | is the length of φ. This result improves upon the previously known bound of O(5|φ |) for rLTL verification and is closer to the LTL bound of O(2|φ |). The usefulness of this fragment is demonstrated by a number of case studies showing its practical significance in terms of expressiveness, the ability to describe robustness, and the fine-grained information that rLTL brings to the process of system verification. Moreover, these advantages come at a low computational overhead with respect to LTL verification.

O-Minimal Invariants for Discrete-Time Dynamical Systems

Termination analysis of linear loops plays a key rôle in several areas of computer science, including program verification and abstract interpretation. Already for the simplest variants of linear loops the question of termination relates to deep open problems in number theory, such as the decidability of the Skolem and Positivity Problems for linear recurrence sequences, or equivalently reachability questions for discrete-time linear dynamical systems. In this article, we introduce the class of o-minimal invariants , which is broader than any previously considered, and study the decidability of the existence and algorithmic synthesis of such invariants as certificates of non-termination for linear loops equipped with a large class of halting conditions. We establish two main decidability results, one of them conditional on Schanuel’s conjecture is transcendental number theory.

Logics with Multiteam Semantics

Team semantics is the mathematical basis of modern logics of dependence and independence. In contrast to classical Tarski semantics, a formula is evaluated not for a single assignment of values to the free variables, but on a set of such assignments, called a team. Team semantics is appropriate for a purely logical understanding of dependency notions, where only the presence or absence of data matters, but being based on sets, it does not take into account multiple occurrences of data values. It is therefore insufficient in scenarios where such multiplicities matter, in particular for reasoning about probabilities and statistical independencies. Therefore, an extension from teams to multiteams (i.e. multisets of assignments) has been proposed by several authors. In this paper we aim at a systematic development of logics of dependence and independence based on multiteam semantics. We study atomic dependency properties of finite multiteams and discuss the appropriate meaning of logical operators to extend the atomic dependencies to full-fledged logics for reasoning about dependence properties in a multiteam setting. We explore properties and expressive power of a wide spectrum of different multiteam logics and compare them to second-order logic and to logics with team semantics. In many cases the results resemble what is known in team semantics, but there are also interesting differences. While in team semantics, the combination of inclusion and exclusion dependencies leads to a logic with the full power of both independence logic and existential second-order logic, independence properties of multiteams are not definable by any combination of properties that are downwards closed or union closed and thus are strictly more powerful than inclusion-exclusion logic. We also study the relationship of logics with multiteam semantics with existential second-order logic for a specific class of metafinite structures. It turns out that inclusion-exclusion logic can be characterised in a precise sense by the Presburger fragment of this logic, but for capturing independence, we need to go beyond it and add some form of multiplication. Finally, we also consider multiteams with weights in the reals and study the expressive power of formulae by means of topological properties.

Coalgebraic Reasoning with Global Assumptions in Arithmetic Modal Logics

We establish a generic upper bound ExpTime for reasoning with global assumptions (also known as TBoxes) in coalgebraic modal logics. Unlike earlier results of this kind, our bound does not require a tractable set of tableau rules for the instance logics, so that the result applies to wider classes of logics. Examples are Presburger modal logic, which extends graded modal logic with linear inequalities over numbers of successors, and probabilistic modal logic with polynomial inequalities over probabilities. We establish the theoretical upper bound using a type elimination algorithm. We also provide a global caching algorithm that potentially avoids building the entire exponential-sized space of candidate states, and thus offers a basis for practical reasoning. This algorithm still involves frequent fixpoint computations; we show how these can be handled efficiently in a concrete algorithm modelled on Liu and Smolka’s linear-time fixpoint algorithm. Finally, we show that the upper complexity bound is preserved under adding nominals to the logic, i.e., in coalgebraic hybrid logic.

Symmetric Circuits for Rank Logic

Fixed-point logic with rank (FPR) is an extension of fixed-point logic with counting (FPC) with operators for computing the rank of a matrix over a finit field. The expressive power of FPR properly extends that of FPC and is contained in P, but it is not known if that containment is proper. We give a circuit characterization for FPR in terms of families of symmetric circuits with rank gates, along the lines of that for FPC given by Anderson and Dawar in 2017. This requires the development of a broad framework of circuits in which the individual gates compute functions that are not symmetric (i.e., invariant under all permutations of their inputs). This framework also necessitates the development of novel techniques to prove the equivalence of circuits and logic. Both the framework and the techniques are of greater generality than the main result.

Universal Equivalence and Majority of Probabilistic Programs over Finite Fields

We study decidability problems for equivalence of probabilistic programs for a core probabilistic programming language over finite fields of fixed characteristic. The programming language supports uniform sampling, addition, multiplication, and conditionals and thus is sufficiently expressive to encode Boolean and arithmetic circuits. We consider two variants of equivalence: The first one considers an interpretation over the finite field F q , while the second one, which we call universal equivalence, verifies equivalence over all extensions F q k of F q . The universal variant typically arises in provable cryptography when one wishes to prove equivalence for any length of bitstrings, i.e., elements of F 2 k for any k . While the first problem is obviously decidable, we establish its exact complexity, which lies in the counting hierarchy. To show decidability and a doubly exponential upper bound of the universal variant, we rely on results from algorithmic number theory and the possibility to compare local zeta functions associated to given polynomials. We then devise a general way to draw links between the universal probabilistic problems and widely studied problems on linear recurrence sequences. Finally, we study several variants of the equivalence problem, including a problem we call majority, motivated by differential privacy. We also define and provide some insights about program indistinguishability, proving that it is decidable for programs always returning 0 or 1.

Piecewise Linear Valued CSPs Solvable by Linear Programming Relaxation

Valued constraint satisfaction problems (VCSPs) are a large class of combinatorial optimisation problems. The computational complexity of VCSPs depends on the set of allowed cost functions in the input. Recently, the computational complexity of all VCSPs for finite sets of cost functions over finite domains has been classified. Many natural optimisation problems, however, cannot be formulated as VCSPs over a finite domain. We initiate the systematic investigation of the complexity of infinite-domain VCSPs with piecewise linear homogeneous cost functions. Such VCSPs can be solved in polynomial time if the cost functions are improved by fully symmetric fractional operations of all arities. We show this by reducing the problem to a finite-domain VCSP which can be solved using the basic linear program relaxation. It follows that VCSPs for submodular PLH cost functions can be solved in polynomial time; in fact, we show that submodular PLH functions form a maximally tractable class of PLH cost functions.

Lower Bounds on OBDD Proofs with Several Orders

This article is motivated by seeking lower bounds on OBDD(∧, w, r) refutations, namely, OBDD refutations that allow weakening and arbitrary reorderings. We first work with 1 - NBP ∧ refutations based on read-once nondeterministic branching programs. These generalize OBDD(∧, r) refutations. There are polynomial size 1 - NBP(∧) refutations of the pigeonhole principle, hence 1-NBP(∧) is strictly stronger than OBDD}(∧, r). There are also formulas that have polynomial size tree-like resolution refutations but require exponential size 1-NBP(∧) refutations. As a corollary, OBDD}(∧, r) does not simulate tree-like resolution, answering a previously open question. The system 1-NBP(∧, ∃) uses projection inferences instead of weakening. 1-NBP(∧, ∃ k is the system restricted to projection on at most k distinct variables. We construct explicit constant degree graphs G n on n vertices and an ε > 0, such that 1-NBP(∧, ∃ ε n ) refutations of the Tseitin formula for G n require exponential size. Second, we study the proof system OBDD}(∧, w, r ℓ ), which allows ℓ different variable orders in a refutation. We prove an exponential lower bound on the complexity of tree-like OBDD(∧, w, r ℓ ) refutations for ℓ = ε log n , where n is the number of variables and ε > 0 is a constant. The lower bound is based on multiparty communication complexity.

Reiterman’s Theorem on Finite Algebras for a Monad

Profinite equations are an indispensable tool for the algebraic classification of formal languages. Reiterman’s theorem states that they precisely specify pseudovarieties, i.e., classes of finite algebras closed under finite products, subalgebras and quotients. In this article, Reiterman’s theorem is generalized to finite Eilenberg-Moore algebras for a monad T on a category D: we prove that a class of finite T -algebras is a pseudovariety iff it is presentable by profinite equations. As a key technical tool, we introduce the concept of a profinite monad T ^ associated to the monad T , which gives a categorical view of the construction of the space of profinite terms.

The Complexity of Counting Problems Over Incomplete Databases

We study the complexity of various fundamental counting problems that arise in the context of incomplete databases, i.e., relational databases that can contain unknown values in the form of labeled nulls. Specifically, we assume that the domains of these unknown values are finite and, for a Boolean query q , we consider the following two problems: Given as input an incomplete database D , (a) return the number of completions of D that satisfy q ; or (b) return the number of valuations of the nulls of D yielding a completion that satisfies q . We obtain dichotomies between #P-hardness and polynomial-time computability for these problems when q is a self-join–free conjunctive query and study the impact on the complexity of the following two restrictions: (1) every null occurs at most once in D (what is called Codd tables ); and (2) the domain of each null is the same. Roughly speaking, we show that counting completions is much harder than counting valuations: For instance, while the latter is always in #P, we prove that the former is not in #P under some widely believed theoretical complexity assumption. Moreover, we find that both (1) and (2) can reduce the complexity of our problems. We also study the approximability of these problems and show that, while counting valuations always has a fully polynomial-time randomized approximation scheme (FPRAS), in most cases counting completions does not. Finally, we consider more expressive query languages and situate our problems with respect to known complexity classes.