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.
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.
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.
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 […]
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 […]
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.
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.
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.
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.
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.
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 […]
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.
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.
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.
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.
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.
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.
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.
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.
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.
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 in […]
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.
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.
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.
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
R$?" […]
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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 all […]
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)$.
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.
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.
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.