We study the reachability problem for affine $\mathbb{Z}$-VASS, which are
integer vector addition systems with states in which transitions perform affine
transformations on the counters. This problem is easily seen to be undecidable
in general, and we therefore restrict ourselves to affine $\mathbb{Z}$-VASS
with the finite-monoid property (afmp-$\mathbb{Z}$-VASS). The latter have the
property that the monoid generated by the matrices appearing in their affine
transformations is finite. The class of afmp-$\mathbb{Z}$-VASS encompasses
classical operations of counter machines such as resets, permutations,
transfers and copies. We show that reachability in an afmp-$\mathbb{Z}$-VASS
reduces to reachability in a $\mathbb{Z}$-VASS whose control-states grow
linearly in the size of the matrix monoid. Our construction shows that
reachability relations of afmp-$\mathbb{Z}$-VASS are semilinear, and in
particular enables us to show that reachability in $\mathbb{Z}$-VASS with
transfers and $\mathbb{Z}$-VASS with copies is PSPACE-complete. We then focus
on the reachability problem for affine $\mathbb{Z}$-VASS with monogenic
monoids: (possibly infinite) matrix monoids generated by a single matrix. We
show that, in a particular case, the reachability problem is decidable for this
class, disproving a conjecture about affine $\mathbb{Z}$-VASS with infinite
matrix monoids we raised in a preliminary version of this paper. We complement
this result by presenting an affine $\mathbb{Z}$-VASS with […]
Open bisimilarity is defined for open process terms in which free variables
may appear. The insight is, in order to characterise open bisimilarity, we move
to the setting of intuitionistic modal logics. The intuitionistic modal logic
introduced, called $\mathcal{OM}$, is such that modalities are closed under
substitutions, which induces a property known as intuitionistic hereditary.
Intuitionistic hereditary reflects in logic the lazy instantiation of free
variables performed when checking open bisimilarity. The soundness proof for
open bisimilarity with respect to our intuitionistic modal logic is mechanised
in Abella. The constructive content of the completeness proof provides an
algorithm for generating distinguishing formulae, which we have implemented. We
draw attention to the fact that there is a spectrum of bisimilarity congruences
that can be characterised by intuitionistic modal logics.
Vector addition systems with states (VASS) are widely used for the formal
verification of concurrent systems. Given their tremendous computational
complexity, practical approaches have relied on techniques such as reachability
relaxations, e.g., allowing for negative intermediate counter values. It is
natural to question their feasibility for VASS enriched with primitives that
typically translate into undecidability. Spurred by this concern, we pinpoint
the complexity of integer relaxations with respect to arbitrary classes of
affine operations.
More specifically, we provide a trichotomy on the complexity of integer
reachability in VASS extended with affine operations (affine VASS). Namely, we
show that it is NP-complete for VASS with resets, PSPACE-complete for VASS with
(pseudo-)transfers and VASS with (pseudo-)copies, and undecidable for any other
class. We further present a dichotomy for standard reachability in affine VASS:
it is decidable for VASS with permutations, and undecidable for any other
class. This yields a complete and unified complexity landscape of reachability
in affine VASS. We also consider the reachability problem parameterized by a
fixed affine VASS, rather than a class, and we show that the complexity
landscape is arbitrary in this setting.
We consider Presburger arithmetic (PA) extended by scalar multiplication by
an algebraic irrational number $\alpha$, and call this extension
$\alpha$-Presburger arithmetic ($\alpha$-PA). We show that the complexity of
deciding sentences in $\alpha$-PA is substantially harder than in PA. Indeed,
when $\alpha$ is quadratic and $r\geq 4$, deciding $\alpha$-PA sentences with
$r$ alternating quantifier blocks and at most $c\ r$ variables and inequalities
requires space at least $K 2^{\cdot^{\cdot^{\cdot^{2^{C\ell(S)}}}}}$ (tower of
height $r-3$), where the constants $c, K, C>0$ only depend on $\alpha$, and
$\ell(S)$ is the length of the given $\alpha$-PA sentence $S$. Furthermore
deciding $\exists^{6}\forall^{4}\exists^{11}$ $\alpha$-PA sentences with at
most $k$ inequalities is PSPACE-hard, where $k$ is another constant depending
only on~$\alpha$. When $\alpha$ is non-quadratic, already four alternating
quantifier blocks suffice for undecidability of $\alpha$-PA sentences.
In this paper we introduce sound and strongly complete axiomatizations for
XPath with data constraints extended with hybrid operators. First, we present
HXPath=, a multi-modal version of XPath with data, extended with nominals and
the hybrid operator @. Then, we introduce an axiomatic system for HXPath=, and
we prove it is strongly complete with respect to the class of abstract data
models, i.e., data models in which data values are abstracted as equivalence
relations. We prove a general completeness result similar to the one presented
in, e.g., [BtC06], that ensures that certain extensions of the axiomatic system
we introduce are also complete. The axiomatic systems that can be obtained in
this way cover a large family of hybrid XPath languages over different classes
of frames, for which we present concrete examples. In addition, we investigate
axiomatizations over the class of tree models, structures widely used in
practice. We show that a strongly complete, finitary, first-order
axiomatization of hybrid XPath over trees does not exist, and we propose two
alternatives to deal with this issue. We finally introduce filtrations to
investigate the status of decidability of the satisfiability problem for these
languages.
We introduce a framework for online structure theory. Our approach
generalises notions arising independently in several areas of computability
theory and complexity theory. We suggest a unifying approach using operators
where we allow the input to be a countable object of an arbitrary complexity.
We give a new framework which (i) ties online algorithms with computable
analysis, (ii) shows how to use modifications of notions from computable
analysis, such as Weihrauch reducibility, to analyse finite but uniform
combinatorics, (iii) show how to finitize reverse mathematics to suggest a fine
structure of finite analogs of infinite combinatorial problems, and (iv) see
how similar ideas can be amalgamated from areas such as EX-learning, computable
analysis, distributed computing and the like. One of the key ideas is that
online algorithms can be viewed as a sub-area of computable analysis.
Conversely, we also get an enrichment of computable analysis from classical
online algorithms.
We present pumping lemmas for five classes of functions definable by
fragments of weighted automata over the min-plus semiring, the max-plus
semiring and the semiring of natural numbers. As a corollary we show that the
hierarchy of functions definable by unambiguous, finitely-ambiguous,
polynomially-ambiguous weighted automata, and the full class of weighted
automata is strict for the min-plus and max-plus semirings.
One of the most popular state-space reduction techniques for model checking
is partial-order reduction (POR). Of the many different POR implementations,
stubborn sets are a very versatile variant and have thus seen many different
applications over the past 32 years. One of the early stubborn sets works shows
how the basic conditions for reduction can be augmented to preserve
stutter-trace equivalence, making stubborn sets suitable for model checking of
linear-time properties. In this paper, we identify a flaw in the reasoning and
show with a counter-example that stutter-trace equivalence is not necessarily
preserved. We propose a stronger reduction condition and provide extensive new
correctness proofs to ensure the issue is resolved. Furthermore, we analyse in
which formalisms the problem may occur. The impact on practical implementations
is limited, since they all compute a correct approximation of the theory.
We present a new version of ReLoC: a relational separation logic for proving
refinements of programs with higher-order state, fine-grained concurrency,
polymorphism and recursive types. The core of ReLoC is its refinement judgment
$e \precsim e' : \tau$, which states that a program $e$ refines a program $e'$
at type $\tau$. ReLoC provides type-directed structural rules and symbolic
execution rules in separation-logic style for manipulating the judgment,
whereas in prior work on refinements for languages with higher-order state and
concurrency, such proofs were carried out by unfolding the judgment into its
definition in the model. ReLoC's abstract proof rules make it simpler to carry
out refinement proofs, and enable us to generalize the notion of logically
atomic specifications to the relational case, which we call logically atomic
relational specifications.
We build ReLoC on top of the Iris framework for separation logic in Coq,
allowing us to leverage features of Iris to prove soundness of ReLoC, and to
carry out refinement proofs in ReLoC. We implement tactics for interactive
proofs in ReLoC, allowing us to mechanize several case studies in Coq, and
thereby demonstrate the practicality of ReLoC.
ReLoC Reloaded extends ReLoC (LICS'18) with various technical improvements, a
new Coq mechanization, and support for Iris's prophecy variables. The latter
allows us to carry out refinement proofs that involve reasoning about the
program's future. We also expand ReLoC's notion […]
Probabilistic automata (PA), also known as probabilistic nondeterministic
labelled transition systems, combine probability and nondeterminism. They can
be given different semantics, like strong bisimilarity, convex bisimilarity, or
(more recently) distribution bisimilarity. The latter is based on the view of
PA as transformers of probability distributions, also called belief states, and
promotes distributions to first-class citizens.
We give a coalgebraic account of distribution bisimilarity, and explain the
genesis of the belief-state transformer from a PA. To do so, we make explicit
the convex algebraic structure present in PA and identify belief-state
transformers as transition systems with state space that carries a convex
algebra. As a consequence of our abstract approach, we can give a sound proof
technique which we call bisimulation up-to convex hull.
We introduce MTT, a dependent type theory which supports multiple modalities.
MTT is parametrized by a mode theory which specifies a collection of modes,
modalities, and transformations between them. We show that different choices of
mode theory allow us to use the same type theory to compute and reason in many
modal situations, including guarded recursion, axiomatic cohesion, and
parametric quantification. We reproduce examples from prior work in guarded
recursion and axiomatic cohesion, thereby demonstrating that MTT constitutes a
simple and usable syntax whose instantiations intuitively correspond to
previous handcrafted modal type theories. In some cases, instantiating MTT to a
particular situation unearths a previously unknown type theory that improves
upon prior systems. Finally, we investigate the metatheory of MTT. We prove the
consistency of MTT and establish canonicity through an extension of recent
type-theoretic gluing techniques. These results hold irrespective of the choice
of mode theory, and thus apply to a wide variety of modal situations.
Let p/q be a rational number. Numeration in base p/q is defined by a function
that evaluates each finite word over A_p={0,1,...,p-1} to some rational number.
We let N_p/q denote the image of this evaluation function. In particular, N_p/q
contains all nonnegative integers and the literature on base p/q usually
focuses on the set of words that are evaluated to nonnegative integers; it is a
rather chaotic language which is not context-free. On the contrary, we study
here the subsets of (N_p/q)^d that are p/q-recognisable, i.e. realised by
finite automata over (A_p)^d. First, we give a characterisation of these sets
as those definable in a first-order logic, similar to the one given by the
Büchi-Bruyère Theorem for integer bases numeration systems. Second, we show
that the natural order relation and the modulo-q operator are not
p/q-recognisable.
We describe a way to represent computable functions between coinductive types
as particular transducers in type theory. This generalizes earlier work on
functions between streams by P. Hancock to a much richer class of coinductive
types. Those transducers can be defined in dependent type theory without any
notion of equality but require inductive-recursive definitions. Most of the
properties of these constructions only rely on a mild notion of equality
(intensional equality) and can thus be formalized in the dependently typed
language Agda.
We present syntactic characterisations for the union closed fragments of
existential second-order logic and of logics with team semantics. Since union
closure is a semantical and undecidable property, the normal form we introduce
enables the handling and provides a better understanding of this fragment. We
also introduce inclusion-exclusion games that turn out to be precisely the
corresponding model-checking games. These games are not only interesting in
their own right, but they also are a key factor towards building a bridge
between the semantic and syntactic fragments. On the level of logics with team
semantics we additionally present restrictions of inclusion-exclusion logic to
capture the union closed fragment. Moreover, we define a team based atom that
when adding it to first-order logic also precisely captures the union closed
fragment of existential second-order logic which answers an open question by
Galliani and Hella.
A bisimulation for a coalgebra of a functor on the category of sets can be
described via a coalgebra in the category of relations, of a lifted functor. A
final coalgebra then gives rise to the coinduction principle, which states that
two bisimilar elements are equal. For polynomial functors, this leads to
well-known descriptions. In the present paper we look at the dual notion of
"apartness". Intuitively, two elements are apart if there is a positive way to
distinguish them. Phrased differently: two elements are apart if and only if
they are not bisimilar. Since apartness is an inductive notion, described by a
least fixed point, we can give a proof system, to derive that two elements are
apart. This proof system has derivation rules and two elements are apart if and
only if there is a finite derivation (using the rules) of this fact.
We study apartness versus bisimulation in two separate ways. First, for weak
forms of bisimulation on labelled transition systems, where silent (tau) steps
are included, we define an apartness notion that corresponds to weak
bisimulation and another apartness that corresponds to branching bisimulation.
The rules for apartness can be used to show that two states of a labelled
transition system are not branching bismilar. To support the apartness view on
labelled transition systems, we cast a number of well-known properties of
branching bisimulation in terms of branching apartness and prove them. Next, we
also study the more general […]
We study the decidability of the Skolem Problem, the Positivity Problem, and
the Ultimate Positivity Problem for linear recurrences with real number initial
values and real number coefficients in the bit-model of real computation. We
show that for each problem there exists a correct partial algorithm which halts
for all problem instances for which the answer is locally constant, thus
establishing that all three problems are as close to decidable as one can
expect them to be in this setting. We further show that the algorithms for the
Positivity Problem and the Ultimate Positivity Problem halt on almost every
instance with respect to the usual Lebesgue measure on Euclidean space. In
comparison, the analogous problems for exact rational or real algebraic
coefficients are known to be decidable only for linear recurrences of fairly
low order.
We present the first complete axiomatisation for quantifier-free separation
logic. The logic is equipped with the standard concrete heaplet semantics and
the proof system has no external feature such as nominals/labels. It is not
possible to rely completely on proof systems for Boolean BI as the concrete
semantics needs to be taken into account. Therefore, we present the first
internal Hilbert-style axiomatisation for quantifier-free separation logic. The
calculus is divided in three parts: the axiomatisation of core formulae where
Boolean combinations of core formulae capture the expressivity of the whole
logic, axioms and inference rules to simulate a bottom-up elimination of
separating connectives, and finally structural axioms and inference rules from
propositional calculus and Boolean BI with the magic wand.
An automaton is unambiguous if for every input it has at most one accepting
computation. An automaton is k-ambiguous (for k > 0) if for every input it has
at most k accepting computations. An automaton is boundedly ambiguous if it is
k-ambiguous for some $k \in \mathbb{N}$. An automaton is finitely
(respectively, countably) ambiguous if for every input it has at most finitely
(respectively, countably) many accepting computations.
The degree of ambiguity of a regular language is defined in a natural way. A
language is k-ambiguous (respectively, boundedly, finitely, countably
ambiguous) if it is accepted by a k-ambiguous (respectively, boundedly,
finitely, countably ambiguous) automaton. Over finite words every regular
language is accepted by a deterministic automaton. Over finite trees every
regular language is accepted by an unambiguous automaton. Over $\omega$-words
every regular language is accepted by an unambiguous Büchi automaton and by a
deterministic parity automaton. Over infinite trees Carayol et al. showed that
there are ambiguous languages.
We show that over infinite trees there is a hierarchy of degrees of
ambiguity: For every k > 1 there are k-ambiguous languages that are not k - 1
ambiguous; and there are finitely (respectively countably, uncountably)
ambiguous languages that are not boundedly (respectively finitely, countably)
ambiguous.
Pomset automata are an operational model of weak bi-Kleene algebra, which
describes programs that can fork an execution into parallel threads, upon
completion of which execution can join to resume as a single thread. We
characterize a fragment of pomset automata that admits a decision procedure for
language equivalence. Furthermore, we prove that this fragment corresponds
precisely to series-rational expressions, i.e., rational expressions with an
additional operator for bounded parallelism. As a consequence, we obtain a new
proof that equivalence of series-rational expressions is decidable.
We study the expressive power of successor-invariant first-order logic, which
is an extension of first-order logic where the usage of an additional successor
relation on the structure is allowed, as long as the validity of formulas is
independent of the choice of a particular successor on finite structures.
We show that when the degree is bounded, successor-invariant first-order
logic is no more expressive than first-order logic.
The theory of classical realizability is a framework for the Curry-Howard
correspondence which enables to associate a program with each proof in
Zermelo-Fraenkel set theory. But, almost all the applications of mathematics in
physics, probability, statistics, etc. use Analysis i.e. the axiom of dependent
choice (DC) or even the (full) axiom of choice (AC). It is therefore important
to find explicit programs for these axioms. Various solutions have been found
for DC, for instance the lambda-term called "bar recursion" or the instruction
"quote" of LISP. We present here the first program for AC.
We investigate the application of the Shapley value to quantifying the
contribution of a tuple to a query answer. The Shapley value is a widely known
numerical measure in cooperative game theory and in many applications of game
theory for assessing the contribution of a player to a coalition game. It has
been established already in the 1950s, and is theoretically justified by being
the very single wealth-distribution measure that satisfies some natural axioms.
While this value has been investigated in several areas, it received little
attention in data management. We study this measure in the context of
conjunctive and aggregate queries by defining corresponding coalition games. We
provide algorithmic and complexity-theoretic results on the computation of
Shapley-based contributions to query answers; and for the hard cases we present
approximation algorithms.
Cartesian differential categories are categories equipped with a differential
combinator which axiomatizes the directional derivative. Important models of
Cartesian differential categories include classical differential calculus of
smooth functions and categorical models of the differential $\lambda$-calculus.
However, Cartesian differential categories cannot account for other interesting
notions of differentiation of a more discrete nature such as the calculus of
finite differences. On the other hand, change action models have been shown to
capture these examples as well as more "exotic" examples of differentiation.
But change action models are very general and do not share the nice properties
of Cartesian differential categories. In this paper, we introduce Cartesian
difference categories as a bridge between Cartesian differential categories and
change action models. We show that every Cartesian differential category is a
Cartesian difference category, and how certain well-behaved change action
models are Cartesian difference categories. In particular, Cartesian difference
categories model both the differential calculus of smooth functions and the
calculus of finite differences. Furthermore, every Cartesian difference
category comes equipped with a tangent bundle monad whose Kleisli category is
again a Cartesian difference category.
The dot-depth hierarchy of Brzozowski and Cohen classifies the star-free
languages of finite words. By a theorem of McNaughton and Papert, these are
also the first-order definable languages. The dot-depth rose to prominence
following the work of Thomas, who proved an exact correspondence with the
quantifier alternation hierarchy of first-order logic: each level in the
dot-depth hierarchy consists of all languages that can be defined with a
prescribed number of quantifier blocks. One of the most famous open problems in
automata theory is to settle whether the membership problem is decidable for
each level: is it possible to decide whether an input regular language belongs
to this level?
Despite a significant research effort, membership by itself has only been
solved for low levels. A recent breakthrough was achieved by replacing
membership with a more general problem: separation. Given two input languages,
one has to decide whether there exists a third language in the investigated
level containing the first language and disjoint from the second. The
motivation is that: (1) while more difficult, separation is more rewarding (2)
it provides a more convenient framework (3) all recent membership algorithms
are reductions to separation for lower levels.
We present a separation algorithm for dot-depth two. While this is our most
prominent application, our result is more general. We consider a family of
hierarchies that includes the dot-depth: concatenation hierarchies. They […]
The bisimulation proof method can be enhanced by employing `bisimulations
up-to' techniques. A comprehensive theory of such enhancements has been
developed for first-order (i.e., CCS-like) labelled transition systems (LTSs)
and bisimilarity, based on abstract fixed-point theory and compatible
functions.
We transport this theory onto languages whose bisimilarity and LTS go beyond
those of first-order models. The approach consists in exhibiting fully abstract
translations of the more sophisticated LTSs and bisimilarities onto the
first-order ones. This allows us to reuse directly the large corpus of up-to
techniques that are available on first-order LTSs. The only ingredient that has
to be manually supplied is the compatibility of basic up-to techniques that are
specific to the new languages. We investigate the method on the pi-calculus,
the lambda-calculus, and a (call-by-value) lambda-calculus with references.
In distributed computing, multiple processes interact to solve a problem
together. The main model of interaction is the message-passing model, where
processes communicate by exchanging messages. Nevertheless, there are several
models varying along important dimensions: degree of synchrony, kinds of
faults, number of faults... This variety is compounded by the lack of a general
formalism in which to abstract these models. One way to bring order is to
constrain these models to communicate in rounds. This is the setting of the
Heard-Of model, which captures many models through predicates on the messages
sent in a round and received on time. Yet, it is not easy to define the
predicate that captures a given operational model. The question is even harder
for the asynchronous case, as unbounded message delay means the implementation
of rounds must depend on details of the model. This paper shows that
characterising asynchronous models by heard-of predicates is indeed meaningful.
This characterization relies on delivered predicates, an intermediate
abstraction between the informal operational model and the heard-of predicates.
Our approach splits the problem into two steps: first extract the delivered
model capturing the informal model, and then characterize the heard-of
predicates that are generated by this delivered model. For the first part, we
provide examples of delivered predicates, and an approach to derive more. It
uses the intuition that complex models are a composition of […]
We propose a new approach to querying graph databases. Our approach balances
competing goals of expressive power, language clarity and computational
complexity. A distinctive feature of our approach is the ability to express
properties of minimal (e.g. shortest) and maximal (e.g. most valuable) paths
satisfying given criteria. To express complex properties in a modular way, we
introduce labelling-generating ontologies. The resulting formalism is
computationally attractive - queries can be answered in non-deterministic
logarithmic space in the size of the database.
We present a construction of W-types in the setoid model of extensional
Martin-Löf type theory using dependent W-types in the underlying intensional
theory. More precisely, we prove that the internal category of setoids has
initial algebras for polynomial endofunctors. In particular, we characterise
the setoid of algebra morphisms from the initial algebra to a given algebra as
a setoid on a dependent W-type. We conclude by discussing the case of free
setoids. We work in a fully intensional theory and, in fact, we assume identity
types only when discussing free setoids. By using dependent W-types we can also
avoid elimination into a type universe. The results have been verified in Coq
and a formalisation is available on the author's GitHub page.
