ABSTRACT. Quantitative algebras, for a given signature with countable arities, are algebras equipped with a metric making all operations nonexpanding. They have been studied by Mardare, Panangaden and Plotkin who also introduced $c$-basic quantitative equations for regular cardinals $c$. Categories of quantitative algebras that can be presented by such equations for $c=\aleph_1$ are called $\omega_1$-varieties. We prove that they are precisely the monadic categories $\Met^\T$, where $\T$ is a countably basic monad on the category $\Met$ of metric spaces.

For finitary signatures one speaks about $\omega$-varieties in case $c= \aleph_0$. If all metrics used are restricted to $\bf{UMet}$, the category of ultrametric spaces, then $\omega$-varieties are precisely the monadic categories $\bf{UMet}^\T$ , where $\T$ is a finitely basic monad.

ABSTRACT. The framework of quantitative equational logic has been successfully applied to reason about algebras whose carriers are metric spaces and operations are nonexpansive. We extend this framework in two orthogonal directions: algebras endowed with generalised metric space structures, and operations being nonexpansive up to a lifting. We apply our results to the algebraic axiomatisation of the Łukaszyk--Karmowski distance on probability distributions, which has recently found application in the field of representation learning on Markov processes.

ABSTRACT. We study concrete sheaf models for a call-by-value higher-order language with recursion. Our family of sheaf models is a generalization of many examples from the literature, such as models for probabilistic and differentiable programming, and fully abstract logical relations models. We treat recursion in the spirit of synthetic domain theory. We provide a general construction of a lifting monad starting from a class of admissible monomorphisms in the site of the sheaf category. In this way, we obtain a family of models parametrized by a concrete site and a class of monomorphisms, for which we prove a general computational adequacy theorem.

ABSTRACT. Probability theory can be studied synthetically as the computational effect embodied by a commutative monad. In the recently proposed Markov categories, one works with an abstraction of the Kleisli category and then defines deterministic morphisms equationally in terms of copying and discarding. The resulting difference between `pure' and `deterministic' leads us to investigate the `sober' objects for a probability monad, for which the two concepts coincide. We propose natural conditions on a probability monad which allow us to identify the sober objects and define an idempotent sobrification functor. Our framework applies to many examples of interest, including the Giry monad on measurable spaces, and allows us to sharpen a previously given version of de Finetti's theorem for Markov categories.

ABSTRACT. We introduce monoidal streams: a generalization of synchronous stream processes to monoidal categories. Monoidal streams over a symmetric monoidal category form a feedback monoidal category. In the same way that classical streams provide semantics to dataflow programming with pure functions; monoidal streams provide semantics to dataflow programming where theories of processes are represented by a symmetric monoidal category. As an example, we study a stochastic dataflow language.

ABSTRACT. This article redevelops and deepens the probability theory of Ewens and others from the 1970s in population biology. At the heart of this theory are the so-called Ewens distributions describing biolological mutations. These distributions have a particularly rich (and beautiful) mathematical structure. The original work is formulated in terms of partitions, which are special multisets on natural numbers. The current redevelopment starts from multisets on arbitrary sets, with partitions as a special form that captures only the multiplicities of multiplicities, without naming the elements themselves. This `element-free' approach will be developed in parallel to the usual element-based theory. Ewens' famous sampling formula describes a cone of (parametrised) distributions on partitions. Another cone for this chain is described in terms of new (element-free) multinomials. They are well-defined because of a novel `partitions multinomial theorem' that extends the familiar multinomial theorem. This is based on a new concept of `division', as element-free distribution, in terms of multisets of probabilities.

ABSTRACT. A timed network is a parallel composition of timed automata synchronizing on common actions. We develop a methodology that allows to use partial-order methods for the reachability problem in timed networks. It is based on a local-time semantics [Bengtsson et al. (1998)]. A new simulation based abstraction of local-time zones is proposed. An efficient algorithm for testing subsumption with respect to this abstraction is developed. The abstraction is not finite in general. We show that, under some weak assumptions, there is no finite abstraction for local-time zones that works for arbitrary networks. We introduce a notion of bounded spread networks, where it is possible to use subsumption and partial-order methods at the same time.

ABSTRACT. We consider linear cost-register automata (equivalently, weighted automata) over the semiring of nonnegative rationals, which generalise probabilistic automata. The two problems boundedness and zero isolation ask whether there is a sequence of words that converge to infinity and zero, respectively. In the general model both problems are undecidable so we focus on the linear copyless restriction. There, we show that the boundedness problem is decidable.

As for the zero isolation problem we need to further restrict the class. We obtain a model, where zero isolation becomes equivalent to universal coverability of orthant vector addition systems (OVAS), a new model in the VAS family interesting on its own. In standard VAS runs are considered only in the positive orthant, while in OVAS every orthant has its own set of vectors that can be applied in that orthant. Assuming Schanuel’s conjecture is true, we prove decidability of universal coverability for three-dimensional OVAS, which implies decidability of zero isolation in a model with at most three independent registers.

ABSTRACT. The class of regular transformations has several equivalent characterizations such as functional MSO transductions, deterministic two-way transducers, streaming string transducers, as well as regular transducer expressions (RTE).

For algorithmic applications, it is very common and useful to transform a specification, here, an RTE, to a machine, here a transducer. In this paper, we give an efficient construction of a two way reversible transducer (2RFT) equivalent to a given RTE. 2RFTs are a well behaved class of transducers which are deterministic and co-deterministic (hence allow evaluation in linear time wrt the input word), and where composition has only polynomial complexity.

For full RTE, the constructed 2RFT has size doubly exponential in the size of the expression. If the RTE does not use Hadamard product or chained-star, the constructed 2RFT has size exponential, which is a tight bound.

ABSTRACT. We present two active learning algorithms for sound deterministic negotiations. Sound deterministic negotiations are models of distributed systems, a kind of Petri nets or Zielonka automata with additional structure. We show that this additional structure allows to minimize such negotiations. The two active learning algorithms differ in the type of membership queries they use. Both have similar complexity to Angluin’s L* algorithm, in particular, the number of queries is polynomial in the size of the negotiation, and not in the number of configurations.

ABSTRACT. We consider two-player stochastic games played on a finite graph for infinitely many rounds. Stochastic games generalize both Markov decision processes (MDP) by adding an adversary player, and two-player deterministic games by adding stochasticity. The outcome of the game is a sequence of distributions over the states of the game graph. We consider synchronizing objectives, which require the probability mass to accumulate in a set of target states, either always, once, infinitely often, or always after some point in the outcome sequence; and the winning modes of sure winning (if the accumulated probability is equal to 1) and almost-sure winning (if the accumulated probability is arbitrarily close to 1).

We present algorithms to compute the set of winning distributions for each of these synchronizing modes, showing that the corresponding decision problem is PSPACE-complete for synchronizing once and infinitely often, and PTIME-complete for synchronizing always and always after some point. These bounds are remarkably in line with the special case of MDPs, while the algorithmic solution and proof technique are considerably more involved, even for deterministic games. This is because those games have a flavour of imperfect information, in particular they are not determined and randomized strategies need to be considered, even if there is no stochastic choice in the game graph. Moreover, in combination with stochasticity in the game graph, finite-memory strategies are not sufficient in general (for synchronizing infinitely often).

ABSTRACT. We study turn-based quantitative games of infinite duration opposing two antagonistic players and played over graphs. This model is widely accepted as providing the adequate framework for formalizing the synthesis question for reactive systems. This important application motivates the question of strategy complexity: which valuations (or payoff functions) admit optimal positional strategies (without memory)? Valuations for which both players have optimal positional strategies have been characterized by Gimbert and Zielonka for finite graphs and by Colcombet and Niwiński for infinite graphs. However, for reactive synthesis, existence of optimal positional strategies for the opponent (which models an antagonistic environment) is irrelevant. Despite this fact, not much is known about valuations for which the protagonist admits optimal positional strategies, regardless of the opponent. In this work, we characterize valuations which admit such strategies over infinite graphs. Our characterization uses the vocabulary of universal graphs, which has also proved useful in understanding recent breakthrough results regarding the complexity of parity games. More precisely, we show that a valuation admitting universal graphs which are monotonic and well-ordered is positional over all game graphs, and – more surprisingly – that the converse is also true for valuations admitting neutral letters. We prove the applicability and elegance of the framework by unifying a number of known positionality results, establishing stronger ones, and providing a new closure property.