View: session overviewtalk overviewside by side with other conferences

"Quantitative Algebra, Probabilities and Monads": 6 papers (12 min presentation + 2-3 min Q&A)

09:00 | Varieties of quantitative algebras and their monads 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. |

09:15 | Beyond Nonexpansive Operations in Quantitative Algebraic Reasoning PRESENTER: Matteo Mio 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. |

09:30 | Concrete categories and higher-order recursion (with applications including probability, differentiability, and full abstraction) PRESENTER: Cristina Matache 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. |

09:45 | Probability monads with submonads of deterministic states PRESENTER: Sean Moss 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. |

10:00 | Monoidal Streams for Dataflow Programming PRESENTER: Mario Román 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. |

10:15 | Partitions and Ewens Distributions in element-free Probability Theory 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. |

"Automata, Transducers and Games": 6 papers (12 min presentation + 2-3 min Q&A)

11:00 | Abstractions for the local-time semantics of timed automata: a foundation for partial-order methods PRESENTER: Igor Walukiewicz 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. |

11:15 | The boundedness and zero isolation problems for weighted automata over nonnegative rationals PRESENTER: David Purser 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. |

11:30 | Efficient Construction of Reversible Transducers from Regular Transducer Expressions PRESENTER: Govind R 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. |

11:45 | Active learning for sound negotiations PRESENTER: Igor Walukiewicz 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. |

12:00 | Stochastic Games with Synchronizing Objectives 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). |

12:15 | Characterizing Positionality in Games of Infinite Duration over Infinite Graphs 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. |

Lunch will be held in Taub lobby (CP, LICS, ICLP) and in The Grand Water Research Institute (KR, FSCD, SAT).

Semantic Intermediate Representations for the Working Metatheoretician:

Abstract: Designers of typed programming languages commonly prove meta-theoretic properties such as type soundness for at least a core of their language. But any practical language implementation must provide some way of interoperating with code written in other languages -- usually via a foreign-function interface (FFI) -- which opens the door to new, potentially unsafe, behaviors that aren't accounted for in the original type soundness proof. Despite the prevalence of interoperability in practical software, principled foundations for the end-to-end design, implementation, and verification of interoperability mechanisms have been largely neglected. In this talk, I'll advocate a proof technique for _working metatheoreticians_ seeking to ensure soundness or security properties of real languages, which implement interoperability using glue code that mediates interaction between languages after compilation to a common lower-level intermediate representation (IR). This proof technique involves building a _semantic intermediate representation_: a semantic model of source-language types as relations on terms of the lower-level IR. Semantic IRs can be used to guide the design and implementation of sound FFIs and to verify that the IR glue code used to implement conversions ensures type soundness. More interestingly, semantic IRs provide a basis for numerous avenues of future work on the principled design of language interoperability: how to support the inclusion of libraries whose behavior is foreign to the original language, how to prove soundness and security properties that are robust to behaviors (attackers) outside of the semantic IR, and how to develop a semantic-IR compiler backend that makes it easier to implement and verify sound interoperability for a wide array of source languages.

Linear recurrences and Skolem problem (rescheduled talks from Tuesday)

**Edon Kelmendi**. Computing the Density of the Positivity Set for Linear Recurrence Sequences15 min

**Richard Lipton, Florian Luca, Joris Nieuwveld, Joel Ouaknine, David Purser and James Worrell**. On the Skolem Problem and the Skolem Conjecture15 min

Mario Roman. Monoidal Streams for Dataflow Programming

Paolo Pistone. Curry and Howard Meet Borel

Pascal Schweitzer. Choiceless Polynomial Time with Witnessed Symmetric Choice

Yoàv Montacute. The Pebble-Related Comonad in Finite Model Theory

Felipe Ferreira Santos. Separating LREC from LFP

Nikolas Mählmann. Model Checking on Interpretations of Classes of Bounded Local Cliquewidth

pickup at 18:00 from the Technion (Tour at Haifa, no food will be provided)