Abstract: We prove that the isomorphism of scattered tree-automatic linear orders as well as the existence of automorphisms of scattered word-automatic linear orders are undecidable problems. Both these results will be derived from a sharpening of Krob's theorem on the undecidability of the equivalence problem for weighted automata over the (max,+)-semiring that we present first.

Abstract: This talk is based on a joint work with Prakash Panangaden and Gordon Plotkin that will be presented at LICS2016. It is an attempt of developing a quantitative equational reasoning that generalizes the classic equational reasoning and focusses on a semantics based on the concept of Quantitative Universal Algebra that we will introduce. We use these equational theories to study various monads over the category of metric spaces that bring meaningful quantitative semantics for systems. As a result, we axiomatize a series of relevant distances such as the Hausdorff metrics over quantitive semilattices; the p-Wasserstein metrics (hence also the Kantorovich metric) over barycentric algebras and also over pointed barycentric algebras; and the total variation distance over subprobabilistic barycentric algebras.

Abstract: Quantitative models and quantitative analysis in Computer Science are receiving increased attention. The goal of this talk is to investigate quantitative automata and quantitative logics. Weighted automata on finite words have already been investigated in seminal work of Schützenberger (1961). They consist of classical finite automata in which the transitions carry weights. These weights may model, e.g., the cost, the consumption of resources, or the reliability or probability of the successful execution of the transitions. This concept soon developed a flourishing theory and has been extended to weighted automata acting on trees, traces, pictures, and nested words.
Here, we present a general model of weighted automata acting on graphs, which form a quantitative version of Thomas' unweighted model of graph acceptors. We present syntax and semantics of a quantitative logic; the semantics counts 'how often' a formula is true in a given graph. Our main result, extending the classical result of Büchi, shows that if the weights are taken from an arbitrary commutative semiring, then weighted graph automata and a syntactically defined fragment of our weighted logic are expressively equivalent. As a consequence, we obtain corresponding Büchi-type equivalence results known from recent literature for weighted automata and weighted logics on words, trees, pictures, and nested words. Establishing such a general result has been an open problem for weighted logic for some time.
Joint work with Stefan Dück (Leipzig).

Abstract: I will talk about a variant of MSO on infinite trees which can talk about probabilities. When adding probability to MSO, one has to be very careful to avoid undecidability, e.g. one has to avoid encoding the undecidable emptiness problem for probabilistic automata on ω-words. Michalewski and Mio managed to find a logic which is not immediately seen to be undecidable, and this is the logic I will talk about. The logic is the extension of MSO with a quantifier that says "there is zero probability of choosing a path π in the tree so that property φ(π) is satisfied".

Abstract: For the study of qualitative behaviour the use of calculi seems to be the predominant approach; for the study of quantitative behaviour the use of automata seems to be the predominant approach; and for formal languages there was a useful duality between grammatical formalisms (calculi) and automata. This talk argues the value of grammatical formalisms (calculi) also for quantitative behaviour. We survey the Stochastic Quality Calculus along two facets: pragmatic concerns about how to reason about safety and security of systems being designed; and theoretical concerns about how to gradually and syntactically limit the expressiveness from generalised semi-markov decision processes to slight generalisations of continous time Markov processes, that can be model checked.

Abstract: We will review standard approaches to statistical machine translation with a strong focus on the difference between phrase-based and syntax-based machine translation. After the basic exposition we will review a recently introduced syntax-based translation model that can alleviate some of the standard problems in syntax-based models. We will provide a quantitative evaluation of the new model and some qualitative insights from the evaluation as well. However, some problems remain and we will also discuss some approaches to address them. Finally, we will also demonstrate a recently developed new proof technique that can successfully be used to prove results on the expressive power of translation models.

Abstract: This tutorial reviews some of the significant results established in the field of weighted automata by taking the problem of equivalence as a leading thread. It will start with the computation of reduced representations for automata with weights taken in a field and its generalisation to an exploration procedure. It will then mention in particular the following points: the decidability of the equivalence of deterministic transducers, the undecidability of the equivalence of tropical automata. It will end with the sketch of the relationship between equivalence and conjugacy of weighted automata for certain weight semirings.

Abstract: This talk gives an overview of our work on learning probabilistic automata from observational data. The first part of the talk describes our adaptation of the "Alergia" algorithm for learning probabilistic deterministic automata, and presents experimental results on the accuracy of the learned models with regard to probabilistic LTL model checking. A main concern in a learning approach to automata construction is the evaluation of the accuracy of a learned model. The definition of a suitable error or distance measure between a true automaton and its learned approximation turns out to be surprisingly difficult, and raises fundamental issues that also are relevant for the definition of distance measures in other contexts than model learning. In the second part of the talk I will introduce two fundamental continuity properties for distance functions, and discuss the problem of the joint satisfiability of these properties. Joint work with Hua Mao, Yingke Chen, Thomas D. Nielsen, Kim G. Larsen, Radu Mardare and Brian Nielsen

Abstract: Groups and semigroups generated by automata were formally introduced in the early 60's. They revealed their full potential over the years, by contributing to important conjectures in group theory. In particular the simplest known answer to the general Burnside problem (does there exist infinite finitetly generated groups whose all elements have finite order) is given by an automaton group. It is remarkable that any automaton known to generate an infinite Burnside group is reversible. In this talk I will prove that connected automata with prime number of states cannot in fact generate infinite Burnside groups (joint work with Th. Godin), and explain how the tool used to prove this result might be used to prove that such an automaton generates either a finite semigroup or a semigroup of exponential growth.

Abstract: We consider finite-state automata which are equipped with a storage. Moreover, the transitions are weighted by elements of a unital valuation monoid. A weighted automaton with storage recognizes a weighted language, which is a mapping from input strings to elements of the carrier set of the unital valuation monoid. For the class of weighted languages recognizable by such automata we prove a Chomsky-Schützenberger theorem and a Büchi-Elgot-Trakhtenbrot theorem.

Abstract: Timed automata and games, priced timed automata and energy automata have emerged as useful formalisms for modeling real-time and energy-aware systems as found in several embedded and cyber-physical systems. During the last 20 years the real-time model checker UPPAAL has been developed allowing for efficient verification of hard timing constraints of timed automata. Moreover a number of significant branches exists, e.g. UPPAAL CORA providing efficient support for optimization, UPPAAL TIGA allowing for automatic synthesis of strategies for given safety and liveness objectives, and UPPAAL SMC offering a highly scalable statistical model checking engine supporting performance analysis of stochastic hybrid automata. Most recently the branch UPPAAL STRATEGO has been released supporting synthesis (using machine learning) and evaluation of near-optimal strategies for stochastic priced timed games. The lecture will review the various branches of UPPAAL and indicate their concerted applications to a range of real-time and cyber-physical examples.

Abstract: We investigate to which extent Metric Temporal Logic (MTL, for short), an extension of Linear Temporal Logic that is popular in the real-time community, can be used for model checking weighted automata with weights in the integers.

Abstract: We have recently introduced a new algebraic structure of star-continuous Kleene omega-algebras, motivated by certain Büchi-type problems in so-called energy automata. Star-continuous Kleene omega-algebras are semimodules over star-continuous Kleene algebras with an infinite product which satisfies certain axioms. Their relation to continuous Kleene omega-algebras is similar to the relation of star-continuous Kleene algebras to continuous Kleene algebras.
We will introduce star-continuous Kleene omega-algebras and develop their properties. We will motivate this by a comprehensive example of their application to energy problems.
This is joint work with Zoltán Ésik, Axel Legay and Karin Quaas.

Abstract: A weighted timed game is a timed game with extra quantitative information representing e.g. energy consumption. Optimizing the weight for reaching a target is a natural question, which has already been investigated for ten years. Existence of optimal strategies is known to be undecidable in general, but the value problem (whether the optimal weight is less than a given value) had not been properly investigated. We prove that the value problem is undecidable as well, and introduce a large subclass of weighted timed games (to which the undecidability proof above applies) for which arbitrary-precise approximations of the optimal weight can be computed.
This is joint work with Patricia Bouyer and Samy Jaziri.

Abstract: A transformation mapping a labelled Markov chain to a simple stochastic game is presented. In the resulting simple stochastic game, each vertex corresponds to a pair of states of the labelled Markov chain. The value of a vertex of the simple stochastic game is shown to be equal to the probabilistic bisimilarity distance, a notion due to Desharnais, Gupta, Jagadeesan and Panangaden, of the corresponding pair of states of the labelled Markov chain. Bacci, Bacci, Larsen and Mardare introduced an algorithm to compute the probabilistic bisimilarity distances for a labelled Markov chain. A modification of a basic version of their algorithm for a labelled Markov chain is shown to be the policy iteration algorithm applied to the corresponding simple stochastic game. Furthermore, it is shown that this algorithm takes exponential time in the worst case. Finally, experimental results confirm that it performs better in practice than other algorithms to compute the probabilistic bisimilarity distances.
Joint work with Qiyi Tang.