 |
 |
Volume 18, Issue 1
2022
1. On the Taylor expansion of $\lambda$-terms and the groupoid structure of their rigid approximants
We show that the normal form of the Taylor expansion of a $\lambda$-term is isomorphic to its Böhm tree, improving Ehrhard and Regnier's original proof along three independent directions. First, we simplify the final step of the proof by following the left reduction strategy directly in the resource calculus, avoiding to introduce an abstract machine ad hoc. We also introduce a groupoid of permutations of copies of arguments in a rigid variant of the resource calculus, and relate the coefficients of Taylor expansion with this structure, while Ehrhard and Regnier worked with groups of permutations of occurrences of variables. Finally, we extend all the results to a nondeterministic setting: by contrast with previous attempts, we show that the uniformity property that was crucial in Ehrhard and Regnier's approach can be preserved in this setting.
2. The Dichotomy of Evaluating Homomorphism-Closed Queries on Probabilistic Graphs
We study the problem of query evaluation on probabilistic graphs, namely, tuple-independent probabilistic databases over signatures of arity two. We focus on the class of queries closed under homomorphisms, or, equivalently, the infinite unions of conjunctive queries. Our main result states that the probabilistic query evaluation problem is #P-hard for all unbounded queries from this class. As bounded queries from this class are equivalent to a union of conjunctive queries, they are already classified by the dichotomy of Dalvi and Suciu (2012). Hence, our result and theirs imply a complete data complexity dichotomy, between polynomial time and #P-hardness, on evaluating homomorphism-closed queries over probabilistic graphs. This dichotomy covers in particular all fragments of infinite unions of conjunctive queries over arity-two signatures, such as negation-free (disjunctive) Datalog, regular path queries, and a large class of ontology-mediated queries. The dichotomy also applies to a restricted case of probabilistic query evaluation called generalized model counting, where fact probabilities must be 0, 0.5, or 1. We show the main result by reducing from the problem of counting the valuations of positive partitioned 2-DNF formulae, or from the source-to-target reliability problem in an undirected graph, depending on properties of minimal models for the query.
3. Good-for-games $\omega$-Pushdown Automata
We introduce good-for-games $\omega$-pushdown automata ($\omega$-GFG-PDA). These are automata whose nondeterminism can be resolved based on the input processed so far. Good-for-gameness enables automata to be composed with games, trees, and other automata, applications which otherwise require deterministic automata. Our main results are that $\omega$-GFG-PDA are more expressive than deterministic $\omega$- pushdown automata and that solving infinite games with winning conditions specified by $\omega$-GFG-PDA is EXPTIME-complete. Thus, we have identified a new class of $\omega$-contextfree winning conditions for which solving games is decidable. It follows that the universality problem for $\omega$-GFG-PDA is in EXPTIME as well. Moreover, we study closure properties of the class of languages recognized by $\omega$-GFG- PDA and decidability of good-for-gameness of $\omega$-pushdown automata and languages. Finally, we compare $\omega$-GFG-PDA to $\omega$-visibly PDA, study the resources necessary to resolve the nondeterminism in $\omega$-GFG-PDA, and prove that the parity index hierarchy for $\omega$-GFG-PDA is infinite. This is a corrected version of the paper arXiv:2001.04392v6 published originally on January 7, 2022.
4. A Logic for Monitoring Dynamic Networks of Spatially-distributed Cyber-Physical Systems
Cyber-Physical Systems (CPS) consist of inter-wined computational (cyber) and physical components interacting through sensors and/or actuators. Computational elements are networked at every scale and can communicate with each other and with humans. Nodes can join and leave the network at any time or they can move to different spatial locations. In this scenario, monitoring spatial and temporal properties plays a key role in the understanding of how complex behaviors can emerge from local and dynamic interactions. We revisit here the Spatio-Temporal Reach and Escape Logic (STREL), a logic-based formal language designed to express and monitor spatio-temporal requirements over the execution of mobile and spatially distributed CPS. STREL considers the physical space in which CPS entities (nodes of the graph) are arranged as a weighted graph representing their dynamic topological configuration. Both nodes and edges include attributes modeling physical and logical quantities that can evolve over time. STREL combines the Signal Temporal Logic with two spatial modalities reach and escape that operate over the weighted graph. From these basic operators, we can derive other important spatial modalities such as everywhere, somewhere and surround. We propose both qualitative and quantitative semantics based on constraint semiring algebraic structure. We provide an offline monitoring algorithm for STREL and we show the feasibility of our approach with the application to two case studies: […]
5. Integrity Constraints Revisited: From Exact to Approximate Implication
Integrity constraints such as functional dependencies (FD) and multi-valued dependencies (MVD) are fundamental in database schema design. Likewise, probabilistic conditional independences (CI) are crucial for reasoning about multivariate probability distributions. The implication problem studies whether a set of constraints (antecedents) implies another constraint (consequent), and has been investigated in both the database and the AI literature, under the assumption that all constraints hold exactly. However, many applications today consider constraints that hold only approximately. In this paper we define an approximate implication as a linear inequality between the degree of satisfaction of the antecedents and consequent, and we study the relaxation problem: when does an exact implication relax to an approximate implication? We use information theory to define the degree of satisfaction, and prove several results. First, we show that any implication from a set of data dependencies (MVDs+FDs) can be relaxed to a simple linear inequality with a factor at most quadratic in the number of variables; when the consequent is an FD, the factor can be reduced to 1. Second, we prove that there exists an implication between CIs that does not admit any relaxation; however, we prove that every implication between CIs relaxes "in the limit". Then, we show that the implication problem for differential constraints in market basket analysis also admits a relaxation with a factor […]
6. Conditional Bisimilarity for Reactive Systems
Reactive systems à la Leifer and Milner, an abstract categorical framework for rewriting, provide a suitable framework for deriving bisimulation congruences. This is done by synthesizing interactions with the environment in order to obtain a compositional semantics. We enrich the notion of reactive systems by conditions on two levels: first, as in earlier work, we consider rules enriched with application conditions and second, we investigate the notion of conditional bisimilarity. Conditional bisimilarity allows us to say that two system states are bisimilar provided that the environment satisfies a given condition. We present several equivalent definitions of conditional bisimilarity, including one that is useful for concrete proofs and that employs an up-to-context technique, and we compare with related behavioural equivalences. We consider examples based on DPO graph rewriting, an instantiation of reactive systems.
7. $\sigma$-locales in Formal Topology
A $\sigma$-frame is a poset with countable joins and finite meets in which binary meets distribute over countable joins. The aim of this paper is to show that $\sigma$-frames, actually $\sigma$-locales, can be seen as a branch of Formal Topology, that is, intuitionistic and predicative point-free topology. Every $\sigma$-frame $L$ is the lattice of Lindelöf elements (those for which each of their covers admits a countable subcover) of a formal topology of a specific kind which, in its turn, is a presentation of the free frame over $L$. We then give a constructive characterization of the smallest (strongly) dense $\sigma$-sublocale of a given $\sigma$-locale, thus providing a "$\sigma$-version" of a Boolean locale. Our development depends on the axiom of countable choice.
8. A Recursive Approach to Solving Parity Games in Quasipolynomial Time
Zielonka's classic recursive algorithm for solving parity games is perhaps the simplest among the many existing parity game algorithms. However, its complexity is exponential, while currently the state-of-the-art algorithms have quasipolynomial complexity. Here, we present a modification of Zielonka's classic algorithm that brings its complexity down to $n^{O\left(\log\left(1+\frac{d}{\log n}\right)\right)}$, for parity games of size $n$ with $d$ priorities, in line with previous quasipolynomial-time solutions.
9. Rast: A Language for Resource-Aware Session Types
Traditional session types prescribe bidirectional communication protocols for concurrent computations, where well-typed programs are guaranteed to adhere to the protocols. However, simple session types cannot capture properties beyond the basic type of the exchanged messages. In response, recent work has extended session types with refinements from linear arithmetic, capturing intrinsic attributes of processes and data. These refinements then play a central role in describing sequential and parallel complexity bounds on session-typed programs. The Rast language provides an open-source implementation of session-typed concurrent programs extended with arithmetic refinements as well as ergometric and temporal types to capture work and span of program execution. To further support generic programming, Rast also enhances arithmetically refined session types with recently developed nested parametric polymorphism. Type checking relies on Cooper's algorithm for quantifier elimination in Presburger arithmetic with a few significant optimizations, and a heuristic extension to nonlinear constraints. Rast furthermore includes a reconstruction engine so that most program constructs pertaining the layers of refinements and resources are inserted automatically. We provide a variety of examples to demonstrate the expressivity of the language.
10. Normalization for planar string diagrams and a quadratic equivalence algorithm
In the graphical calculus of planar string diagrams, equality is generated by exchange moves, which swap the heights of adjacent vertices. We show that left- and right-handed exchanges each give strongly normalizing rewrite strategies for connected string diagrams. We use this result to give a linear-time solution to the equivalence problem in the connected case, and a quadratic solution in the general case. We also give a stronger proof of the Joyal-Street coherence theorem, settling Selinger's conjecture on recumbent isotopy.
11. Games Where You Can Play Optimally with Arena-Independent Finite Memory
For decades, two-player (antagonistic) games on graphs have been a framework of choice for many important problems in theoretical computer science. A notorious one is controller synthesis, which can be rephrased through the game-theoretic metaphor as the quest for a winning strategy of the system in a game against its antagonistic environment. Depending on the specification, optimal strategies might be simple or quite complex, for example having to use (possibly infinite) memory. Hence, research strives to understand which settings allow for simple strategies. In 2005, Gimbert and Zielonka provided a complete characterization of preference relations (a formal framework to model specifications and game objectives) that admit memoryless optimal strategies for both players. In the last fifteen years however, practical applications have driven the community toward games with complex or multiple objectives, where memory -- finite or infinite -- is almost always required. Despite much effort, the exact frontiers of the class of preference relations that admit finite-memory optimal strategies still elude us. In this work, we establish a complete characterization of preference relations that admit optimal strategies using arena-independent finite memory, generalizing the work of Gimbert and Zielonka to the finite-memory case. We also prove an equivalent to their celebrated corollary of great practical interest: if both players have optimal (arena-independent-)finite-memory […]
12. Universal Algebraic Methods for Constraint Satisfaction Problems
After substantial progress over the last 15 years, the "algebraic CSP-dichotomy conjecture" reduces to the following: every local constraint satisfaction problem (CSP) associated with a finite idempotent algebra is tractable if and only if the algebra has a Taylor term operation. Despite the tremendous achievements in this area (including recently announce proofs of the general conjecture), there remain examples of small algebras with just a single binary operation whose CSP resists direct classification as either tractable or NP-complete using known methods. In this paper we present some new methods for approaching such problems, with particular focus on those techniques that help us attack the class of finite algebras known as "commutative idempotent binars" (CIBs). We demonstrate the utility of these methods by using them to prove that every CIB of cardinality at most 4 yields a tractable CSP.
13. No-Go Theorems for Distributive Laws
Monads are commonplace in computer science, and can be composed using Beck's distributive laws. Unfortunately, finding distributive laws can be extremely difficult and error-prone. The literature contains some general principles for constructing distributive laws. However, until now there have been no such techniques for establishing when no distributive law exists. We present three families of theorems for showing when there can be no distributive law between two monads. The first widely generalizes a counterexample attributed to Plotkin. It covers all the previous known no-go results for specific pairs of monads, and includes many new results. The second and third families are entirely novel, encompassing various new practical situations. For example, they negatively resolve the open question of whether the list monad distributes over itself, reveal a previously unobserved error in the literature, and confirm a conjecture made by Beck himself in his first paper on distributive laws. In addition, we establish conditions under which there can be at most one possible distributive law between two monads, proving various known distributive laws to be unique.
14. Conformance Relations and Hyperproperties for Doping Detection in Time and Space
We present a novel and generalised notion of doping cleanness for cyber-physical systems that allows for perturbing the inputs and observing the perturbed outputs both in the time- and value-domains. We instantiate our definition using existing notions of conformance for cyber-physical systems. As a formal basis for monitoring conformance-based cleanness, we develop the temporal logic HyperSTL*, an extension of Signal Temporal Logics with trace quantifiers and a freeze operator. We show that our generalised definitions are essential in a data-driven method for doping detection and apply our definitions to a case study concerning diesel emission tests.
15. On the Axiomatisability of Parallel Composition
This paper studies the existence of finite equational axiomatisations of the interleaving parallel composition operator modulo the behavioural equivalences in van Glabbeek's linear time-branching time spectrum. In the setting of the process algebra BCCSP over a finite set of actions, we provide finite, ground-complete axiomatisations for various simulation and (decorated) trace semantics. We also show that no congruence over BCCSP that includes bisimilarity and is included in possible futures equivalence has a finite, ground-complete axiomatisation; this negative result applies to all the nested trace and nested simulation semantics.
16. A duality theoretic view on limits of finite structures: Extended version
A systematic theory of structural limits for finite models has been developed by Nesetril and Ossona de Mendez. It is based on the insight that the collection of finite structures can be embedded, via a map they call the Stone pairing, in a space of measures, where the desired limits can be computed. We show that a closely related but finer grained space of (finitely additive) measures arises -- via Stone-Priestley duality and the notion of types from model theory -- by enriching the expressive power of first-order logic with certain "probabilistic operators". We provide a sound and complete calculus for this extended logic and expose the functorial nature of this construction. The consequences are two-fold. On the one hand, we identify the logical gist of the theory of structural limits. On the other hand, our construction shows that the duality theoretic variant of the Stone pairing captures the adding of a layer of quantifiers, thus making a strong link to recent work on semiring quantifiers in logic on words. In the process, we identify the model theoretic notion of types as the unifying concept behind this link. These results contribute to bridging the strands of logic in computer science which focus on semantics and on more algorithmic and complexity related areas, respectively.
17. An extensible equality checking algorithm for dependent type theories
We present a general and user-extensible equality checking algorithm that is applicable to a large class of type theories. The algorithm has a type-directed phase for applying extensionality rules and a normalization phase based on computation rules, where both kinds of rules are defined using the type-theoretic concept of object-invertible rules. We also give sufficient syntactic criteria for recognizing such rules, as well as a simple pattern-matching algorithm for applying them. A third component of the algorithm is a suitable notion of principal arguments, which determines a notion of normal form. By varying these, we obtain known notions, such as weak head-normal and strong normal forms. We prove that our algorithm is sound. We implemented it in the Andromeda 2 proof assistant, which supports user-definable type theories. The user need only provide the equality rules they wish to use, which the algorithm automatically classifies as computation or extensionality rules, and select appropriate principal arguments.
18. On the Nielsen-Schreier Theorem in Homotopy Type Theory
We give a formulation of the Nielsen-Schreier theorem (subgroups of free groups are free) in homotopy type theory using the presentation of groups as pointed connected 1-truncated types. We show the special case of finite index subgroups holds constructively and the full theorem follows from the axiom of choice. We give an example of a boolean infinity topos where our formulation of the theorem does not hold and show a stronger "untruncated" version of the theorem is provably false in homotopy type theory.
19. Bounded Reachability Problems are Decidable in FIFO Machines
The undecidability of basic decision problems for general FIFO machines such as reachability and unboundedness is well-known. In this paper, we provide an underapproximation for the general model by considering only runs that are input-bounded (i.e. the sequence of messages sent through a particular channel belongs to a given bounded language). We prove, by reducing this model to a counter machine with restricted zero tests, that the rational-reachability problem (and by extension, control-state reachability, unboundedness, deadlock, etc.) is decidable. This class of machines subsumes input-letter-bounded machines, flat machines, linear FIFO nets, and monogeneous machines, for which some of these problems were already shown to be decidable. These theoretical results can form the foundations to build a tool to verify general FIFO machines based on the analysis of input-bounded machines.
20. Quantifying over Boolean announcements
Various extensions of public announcement logic have been proposed with quantification over announcements. The best-known extension is called arbitrary public announcement logic, APAL. It contains a primitive language construct Box phi intuitively expressing that "after every public announcement of a formula, formula phi is true". The logic APAL is undecidable and it has an infinitary axiomatization. Now consider restricting the APAL quantification to public announcements of Boolean formulas only, such that Box phi intuitively expresses that "after every public announcement of a Boolean formula, formula phi is true". This logic can therefore called Boolean arbitrary public announcement logic, BAPAL. The logic BAPAL is the subject of this work. Unlike APAL it has a finitary axiomatization. Also, BAPAL is not at least as expressive as APAL. A further claim that BAPAL is decidable is deferred to a companion paper.
21. Weight Annotation in Information Extraction
The framework of document spanners abstracts the task of information extraction from text as a function that maps every document (a string) into a relation over the document's spans (intervals identified by their start and end indices). For instance, the regular spanners are the closure under the Relational Algebra (RA) of the regular expressions with capture variables, and the expressive power of the regular spanners is precisely captured by the class of VSet-automata -- a restricted class of transducers that mark the endpoints of selected spans. In this work, we embark on the investigation of document spanners that can annotate extractions with auxiliary information such as confidence, support, and confidentiality measures. To this end, we adopt the abstraction of provenance semirings by Green et al., where tuples of a relation are annotated with the elements of a commutative semiring, and where the annotation propagates through the positive RA operators via the semiring operators. Hence, the proposed spanner extension, referred to as an annotator, maps every string into an annotated relation over the spans. As a specific instantiation, we explore weighted VSet-automata that, similarly to weighted automata and transducers, attach semiring elements to transitions. We investigate key aspects of expressiveness, such as the closure under the positive RA, and key aspects of computational complexity, such as the enumeration of annotated answers and their ranked enumeration […]
22. Verifying liquidity of recursive Bitcoin contracts
Smart contracts - computer protocols that regulate the exchange of crypto-assets in trustless environments - have become popular with the spread of blockchain technologies. A landmark security property of smart contracts is liquidity: in a non-liquid contract, it may happen that some assets remain frozen, i.e. not redeemable by anyone. The relevance of this issue is witnessed by recent liquidity attacks to Ethereum, which have frozen hundreds of USD millions. We address the problem of verifying liquidity on BitML, a DSL for smart contracts with a secure compiler to Bitcoin, featuring primitives for currency transfers, contract renegotiation and consensual recursion. Our main result is a verification technique for liquidity. We first transform the infinite-state semantics of BitML into a finite-state one, which focusses on the behaviour of a chosen set of contracts, abstracting from the moves of the context. With respect to the chosen contracts, this abstraction is sound, i.e. if the abstracted contract is liquid, then also the concrete one is such. We then verify liquidity by model-checking the finite-state abstraction. We implement a toolchain that automatically verifies liquidity of BitML contracts and compiles them to Bitcoin, and we assess it through a benchmark of representative contracts.
23. Quotients of Bounded Natural Functors
The functorial structure of type constructors is the foundation for many definition and proof principles in higher-order logic (HOL). For example, inductive and coinductive datatypes can be built modularly from bounded natural functors (BNFs), a class of well-behaved type constructors. Composition, fixpoints, and, under certain conditions, subtypes are known to preserve the BNF structure. In this article, we tackle the preservation question for quotients, the last important principle for introducing new types in HOL. We identify sufficient conditions under which a quotient inherits the BNF structure from its underlying type. Surprisingly, lifting the structure in the obvious manner fails for some quotients, a problem that also affects the quotients of polynomial functors used in the Lean proof assistant. We provide a strictly more general lifting scheme that supports such problematic quotients. We extend the Isabelle/HOL proof assistant with a command that automates the registration of a quotient type as a BNF, reducing the proof burden on the user from the full set of BNF axioms to our inheritance conditions. We demonstrate the command's usefulness through several case studies.
24. Satisfiability and Model Checking for the Logic of Sub-Intervals under the Homogeneity Assumption
The expressive power of interval temporal logics (ITLs) makes them one of the most natural choices in a number of application domains, ranging from the specification and verification of complex reactive systems to automated planning. However, for a long time, because of their high computational complexity, they were considered not suitable for practical purposes. The recent discovery of several computationally well-behaved ITLs has finally changed the scenario. In this paper, we investigate the finite satisfiability and model checking problems for the ITL D, that has a single modality for the sub-interval relation, under the homogeneity assumption (that constrains a proposition letter to hold over an interval if and only if it holds over all its points). We first prove that the satisfiability problem for D, over finite linear orders, is PSPACE-complete, and then we show that the same holds for its model checking problem, over finite Kripke structures. In such a way, we enrich the set of tractable interval temporal logics with a new meaningful representative.
25. Regular matching problems for infinite trees
We study the matching problem of regular tree languages, that is, "$\exists \sigma:\sigma(L)\subseteq R$?" where $L,R$ are regular tree languages over the union of finite ranked alphabets $\Sigma$ and $\mathcal{X}$ where $\mathcal{X}$ is an alphabet of variables and $\sigma$ is a substitution such that $\sigma(x)$ is a set of trees in $T(\Sigma\cup H)\setminus H$ for all $x\in \mathcal{X}$. Here, $H$ denotes a set of "holes" which are used to define a "sorted" concatenation of trees. Conway studied this problem in the special case for languages of finite words in his classical textbook "Regular algebra and finite machines" published in 1971. He showed that if $L$ and $R$ are regular, then the problem "$\exists \sigma \forall x\in \mathcal{X}: \sigma(x)\neq \emptyset\wedge \sigma(L)\subseteq R$?" is decidable. Moreover, there are only finitely many maximal solutions, the maximal solutions are regular substitutions, and they are effectively computable. We extend Conway's results when $L,R$ are regular languages of finite and infinite trees, and language substitution is applied inside-out, in the sense of Engelfriet and Schmidt (1977/78). More precisely, we show that if $L\subseteq T(\Sigma\cup\mathcal{X})$ and $R\subseteq T(\Sigma)$ are regular tree languages over finite or infinite trees, then the problem "$\exists \sigma \forall x\in \mathcal{X}: \sigma(x)\neq \emptyset\wedge \sigma_{\mathrm{io}}(L)\subseteq […]
26. Optimizing tree decompositions in MSO
The classic algorithm of Bodlaender and Kloks [J. Algorithms, 1996] solves the following problem in linear fixed-parameter time: given a tree decomposition of a graph of (possibly suboptimal) width k, compute an optimum-width tree decomposition of the graph. In this work, we prove that this problem can also be solved in mso in the following sense: for every positive integer k, there is an mso transduction from tree decompositions of width k to tree decompositions of optimum width. Together with our recent results [LICS 2016], this implies that for every k there exists an mso transduction which inputs a graph of treewidth k, and nondeterministically outputs its tree decomposition of optimum width. We also show that mso transductions can be implemented in linear fixed-parameter time, which enables us to derive the algorithmic result of Bodlaender and Kloks as a corollary of our main result.
27. Duality for powerset coalgebras
Let CABA be the category of complete and atomic boolean algebras and complete boolean homomorphisms, and let CSL be the category of complete meet-semilattices and complete meet-homomorphisms. We show that the forgetful functor from CABA to CSL has a left adjoint. This allows us to describe an endofunctor H on CABA such that the category Alg(H) of algebras for H is dually equivalent to the category Coalg(P) of coalgebras for the powerset endofunctor P on Set. As a consequence, we derive Thomason duality from Tarski duality, thus paralleling how Jónsson-Tarski duality is derived from Stone duality.
28. Canonicity and homotopy canonicity for cubical type theory
Cubical type theory provides a constructive justification of homotopy type theory. A crucial ingredient of cubical type theory is a path lifting operation which is explained computationally by induction on the type involving several non-canonical choices. We present in this article two canonicity results, both proved by a sconing argument: a homotopy canonicity result, every natural number is path equal to a numeral, even if we take away the equations defining the lifting operation on the type structure, and a canonicity result, which uses these equations in a crucial way. Both proofs are done internally in a presheaf model.
29. Residuality and Learning for Nondeterministic Nominal Automata
We are motivated by the following question: which data languages admit an active learning algorithm? This question was left open in previous work by the authors, and is particularly challenging for languages recognised by nondeterministic automata. To answer it, we develop the theory of residual nominal automata, a subclass of nondeterministic nominal automata. We prove that this class has canonical representatives, which can always be constructed via a finite number of observations. This property enables active learning algorithms, and makes up for the fact that residuality -- a semantic property -- is undecidable for nominal automata. Our construction for canonical residual automata is based on a machine-independent characterisation of residual languages, for which we develop new results in nominal lattice theory. Studying residuality in the context of nominal languages is a step towards a better understanding of learnability of automata with some sort of nondeterminism.
30. Fixed Points Theorems for Non-Transitive Relations
In this paper, we develop an Isabelle/HOL library of order-theoretic fixed-point theorems. We keep our formalization as general as possible: we reprove several well-known results about complete orders, often with only antisymmetry or attractivity, a mild condition implied by either antisymmetry or transitivity. In particular, we generalize various theorems ensuring the existence of a quasi-fixed point of monotone maps over complete relations, and show that the set of (quasi-)fixed points is itself complete. This result generalizes and strengthens theorems of Knaster-Tarski, Bourbaki-Witt, Kleene, Markowsky, Pataraia, Mashburn, Bhatta-George, and Stouti-Maaden.
31. Reachability and liveness in parametric timed automata
We study timed systems in which some timing features are unknown parameters. Parametric timed automata (PTAs) are a classical formalism for such systems but for which most interesting problems are undecidable. Notably, the parametric reachability emptiness problem, i.e., the emptiness of the parameter valuations set allowing to reach some given discrete state, is undecidable. Lower-bound/upper-bound parametric timed automata (L/U-PTAs) achieve decidability for reachability properties by enforcing a separation of parameters used as upper bounds in the automaton constraints, and those used as lower bounds. In this paper, we first study reachability. We exhibit a subclass of PTAs (namely integer-points PTAs) with bounded rational-valued parameters for which the parametric reachability emptiness problem is decidable. Using this class, we present further results improving the boundary between decidability and undecidability for PTAs and their subclasses such as L/U-PTAs. We then study liveness. We prove that: (1) deciding the existence of at least one parameter valuation for which there exists an infinite run in an L/U-PTA is PSpace-complete; (2) the existence of a parameter valuation such that the system has a deadlock is however undecidable; (3) the problem of the existence of a valuation for which a run remains in a given set of locations exhibits a very thin border between decidability and undecidability.
32. Proof Theory of Riesz Spaces and Modal Riesz Spaces
We design hypersequent calculus proof systems for the theories of Riesz spaces and modal Riesz spaces and prove the key theorems: soundness, completeness and cut elimination. These are then used to obtain completely syntactic proofs of some interesting results concerning the two theories. Most notably, we prove a novel result: the theory of modal Riesz spaces is decidable. This work has applications in the field of logics of probabilistic programs since modal Riesz spaces provide the algebraic semantics of the Riesz modal logic underlying the probabilistic mu-calculus.
33. A tier-based typed programming language characterizing Feasible Functionals
The class of Basic Feasible Functionals BFF$_2$ is the type-2 counterpart of the class FP of type-1 functions computable in polynomial time. Several characterizations have been suggested in the literature, but none of these present a programming language with a type system guaranteeing this complexity bound. We give a characterization of BFF$_2$ based on an imperative language with oracle calls using a tier-based type system whose inference is decidable. Such a characterization should make it possible to link higher-order complexity with programming theory. The low complexity (cubic in the size of the program) of the type inference algorithm contrasts with the intractability of the aforementioned methods and does not overly constrain the expressive power of the language.
34. Infinite Probabilistic Databases
Probabilistic databases (PDBs) model uncertainty in data in a quantitative way. In the established formal framework, probabilistic (relational) databases are finite probability spaces over relational database instances. This finiteness can clash with intuitive query behavior (Ceylan et al., KR 2016), and with application scenarios that are better modeled by continuous probability distributions (Dalvi et al., CACM 2009). We formally introduced infinite PDBs in (Grohe and Lindner, PODS 2019) with a primary focus on countably infinite spaces. However, an extension beyond countable probability spaces raises nontrivial foundational issues concerned with the measurability of events and queries and ultimately with the question whether queries have a well-defined semantics. We argue that finite point processes are an appropriate model from probability theory for dealing with general probabilistic databases. This allows us to construct suitable (uncountable) probability spaces of database instances in a systematic way. Our main technical results are measurability statements for relational algebra queries as well as aggregate queries and Datalog queries.
35. Hilbert's Tenth Problem in Coq (Extended Version)
We formalise the undecidability of solvability of Diophantine equations, i.e. polynomial equations over natural numbers, in Coq's constructive type theory. To do so, we give the first full mechanisation of the Davis-Putnam-Robinson-Matiyasevich theorem, stating that every recursively enumerable problem -- in our case by a Minsky machine -- is Diophantine. We obtain an elegant and comprehensible proof by using a synthetic approach to computability and by introducing Conway's FRACTRAN language as intermediate layer. Additionally, we prove the reverse direction and show that every Diophantine relation is recognisable by $\mu$-recursive functions and give a certified compiler from $\mu$-recursive functions to Minsky machines.
36. Verified Approximation Algorithms
We present the first formal verification of approximation algorithms for NP-complete optimization problems: vertex cover, independent set, set cover, center selection, load balancing, and bin packing. We uncover incompletenesses in existing proofs and improve the approximation ratio in one case. All proofs are uniformly invariant based.
37. Sequential Relational Decomposition
The concept of decomposition in computer science and engineering is considered a fundamental component of computational thinking and is prevalent in design of algorithms, software construction, hardware design, and more. We propose a simple and natural formalization of sequential decomposition, in which a task is decomposed into two sequential sub-tasks, with the first sub-task to be executed before the second sub-task is executed. These tasks are specified by means of input/output relations. We define and study decomposition problems, which is to decide whether a given specification can be sequentially decomposed. Our main result is that decomposition itself is a difficult computational problem. More specifically, we study decomposition problems in three settings: where the input task is specified explicitly, by means of Boolean circuits, and by means of automatic relations. We show that in the first setting decomposition is NP-complete, in the second setting it is NEXPTIME-complete, and in the third setting there is evidence to suggest that it is undecidable. Our results indicate that the intuitive idea of decomposition as a system-design approach requires further investigation. In particular, we show that adding a human to the loop by asking for a decomposition hint lowers the complexity of decomposition problems considerably.
38. BDD-Based Algorithm for SCC Decomposition of Edge-Coloured Graphs
Edge-coloured directed graphs provide an essential structure for modelling and analysis of complex systems arising in many scientific disciplines (e.g. feature-oriented systems, gene regulatory networks, etc.). One of the fundamental problems for edge-coloured graphs is the detection of strongly connected components, or SCCs. The size of edge-coloured graphs appearing in practice can be enormous both in the number of vertices and colours. The large number of vertices prevents us from analysing such graphs using explicit SCC detection algorithms, such as Tarjan's, which motivates the use of a symbolic approach. However, the large number of colours also renders existing symbolic SCC detection algorithms impractical. This paper proposes a novel algorithm that symbolically computes all the monochromatic strongly connected components of an edge-coloured graph. In the worst case, the algorithm performs $O(p \cdot n \cdot log~n)$ symbolic steps, where $p$ is the number of colours and $n$ is the number of vertices. We evaluate the algorithm using an experimental implementation based on binary decision diagrams (BDDs). Specifically, we use our implementation to explore the SCCs of a large collection of coloured graphs (up to $2^{48}$) obtained from Boolean networks -- a modelling framework commonly appearing in systems biology.
39. A Scalable Algorithm for Decentralized Actor Termination Detection
Automatic garbage collection (GC) prevents certain kinds of bugs and reduces programming overhead. GC techniques for sequential programs are based on reachability analysis. However, testing reachability from a root set is inadequate for determining whether an actor is garbage: Observe that an unreachable actor may send a message to a reachable actor. Instead, it is sufficient to check termination (sometimes also called quiescence): an actor is terminated if it is not currently processing a message and cannot receive a message in the future. Moreover, many actor frameworks provide all actors with access to file I/O or external storage; without inspecting an actor's internal code, it is necessary to check that the actor has terminated to ensure that it may be garbage collected in these frameworks. Previous algorithms to detect actor garbage require coordination mechanisms such as causal message delivery or nonlocal monitoring of actors for mutation. Such coordination mechanisms adversely affect concurrency and are therefore expensive in distributed systems. We present a low-overhead deferred reference listing technique (called DRL) for termination detection in actor systems. DRL is based on asynchronous local snapshots and message-passing between actors. This enables a decentralized implementation and transient network partition tolerance. The paper provides a formal description of DRL, shows that all actors identified as garbage have indeed terminated (safety), and that […]
40. The Big-O Problem
Given two weighted automata, we consider the problem of whether one is big-O of the other, i.e., if the weight of every finite word in the first is not greater than some constant multiple of the weight in the second. We show that the problem is undecidable, even for the instantiation of weighted automata as labelled Markov chains. Moreover, even when it is known that one weighted automaton is big-O of another, the problem of finding or approximating the associated constant is also undecidable. Our positive results show that the big-O problem is polynomial-time solvable for unambiguous automata, coNP-complete for unlabelled weighted automata (i.e., when the alphabet is a single character) and decidable, subject to Schanuel's conjecture, when the language is bounded (i.e., a subset of $w_1^*\dots w_m^*$ for some finite words $w_1,\dots,w_m$) or when the automaton has finite ambiguity. On labelled Markov chains, the problem can be restated as a ratio total variation distance, which, instead of finding the maximum difference between the probabilities of any two events, finds the maximum ratio between the probabilities of any two events. The problem is related to $\varepsilon$-differential privacy, for which the optimal constant of the big-O notation is exactly $\exp(\varepsilon)$.
41. Higher Order Automatic Differentiation of Higher Order Functions
We present semantic correctness proofs of automatic differentiation (AD). We consider a forward-mode AD method on a higher order language with algebraic data types, and we characterise it as the unique structure preserving macro given a choice of derivatives for basic operations. We describe a rich semantics for differentiable programming, based on diffeological spaces. We show that it interprets our language, and we phrase what it means for the AD method to be correct with respect to this semantics. We show that our characterisation of AD gives rise to an elegant semantic proof of its correctness based on a gluing construction on diffeological spaces. We explain how this is, in essence, a logical relations argument. Throughout, we show how the analysis extends to AD methods for computing higher order derivatives using a Taylor approximation.
42. Register Automata with Extrema Constraints, and an Application to Two-Variable Logic
We introduce a model of register automata over infinite trees with extrema constraints. Such an automaton can store elements of a linearly ordered domain in its registers, and can compare those values to the suprema and infima of register values in subtrees. We show that the emptiness problem for these automata is decidable. As an application, we prove decidability of the countable satisfiability problem for two-variable logic in the presence of a tree order, a linear order, and arbitrary atoms that are MSO definable from the tree order. As a consequence, the satisfiability problem for two-variable logic with arbitrary predicates, two of them interpreted by linear orders, is decidable.
43. A Cubical Language for Bishop Sets
We present XTT, a version of Cartesian cubical type theory specialized for Bishop sets à la Coquand, in which every type enjoys a definitional version of the uniqueness of identity proofs. Using cubical notions, XTT reconstructs many of the ideas underlying Observational Type Theory, a version of intensional type theory that supports function extensionality. We prove the canonicity property of XTT (that every closed boolean is definitionally equal to a constant) using Artin gluing.