Monday 25 April 
8:30 
Registration opens 
8:50 
Welcome speech 
9:00 
Dietrich Kuske 
Invited talk: Isomorphisms of automatic linear orders and Krob's undecidability
result
Abstract: We prove that the isomorphism of scattered treeautomatic linear
orders as well as the existence of automorphisms of scattered
wordautomatic 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.

10:00 
M. Hansen, K.G. Larsen, R. Mardare, M.R. Pedersen, B. Xue 
A Complete Approximation Theory for Weighted Transition Systems 
10:30 
Break 
11:00 
Radu Mardare 
Invited talk: Towards a Quantitative Algebraic Theory of Effects
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 Hausdorﬀ metrics over quantitive semilattices; the pWasserstein metrics (hence also the Kantorovich metric) over barycentric algebras and also over pointed barycentric algebras; and the total variation distance over subprobabilistic barycentric algebras.

12:00 
Lunch 
13:30 
Manfred Droste 
Invited talk: Weighted automata and logics on graphs
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üchitype 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).

14:30 
Mikołaj Bojańczyk 
Invited talk: A probabilistic variant of MSO on infinite trees
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".

15:30 
Break 
16:00 
V. Perevoshchikov 
Weight Assignment Logic 
16:30 
U. Fahrenberg, A. Legay, K. Quaas 
Weighted Reachability Games 
17:00 
Program ends 
Tuesday 26 April 
9:00 
JoostPieter Katoen 
Tutorial: Probabilistic Programming: Fun, but Tricky 
10:30 
Break 
11:00 
Flemming Nielson 
Invited talk: Weighted Process Calculi
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 semimarkov decision processes to slight generalisations of continous time Markov processes, that can be model checked.

12:00 
Lunch 
13:30 
Andreas Maletti 
Invited talk: Weighted automata in statistical machine translation
Abstract: We will review standard approaches to statistical machine translation with a strong focus on the difference between phrasebased and syntaxbased machine translation. After the basic exposition we will review a recently introduced syntaxbased translation model that can alleviate some of the standard problems in syntaxbased 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.

14:30 
Z. Fülöp, H. Vogler 
Weighted Iterated Linear Control 
15:00 
Excursion and Danish dinner at Kystens perle 
Wednesday 27 April 
9:00 
Jacques Sakarovitch 
Tutorial: Equivalence of weighted automata
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.

10:30 
Break 
11:00 
Manfred Jaeger 
Invited talk: Learning Probabilistic Automata
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

12:00 
Lunch 
13:30 
Ines Klimann 
Invited talk: Automaton (semi)groups: growth problems and the reversibility
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.

14:30 
Heiko Vogler 
Invited talk: Weighted automata with storage
Abstract: We consider finitestate 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
ChomskySchützenberger theorem and a BüchiElgotTrakhtenbrot theorem.

15:30 
Break 
16:00 
J. Björklund, F. Drewes, A. Jonsson, N. Zechner 
Practical Enumeration of Weighted Tree Languages 
16:30 
G. Bacci, G. Bacci, K.G. Larsen, R. Mardare 
Converging from Branching to Linear Metrics for Weighted Transition Systems 
17:00 
P. Babari, M. Droste, V. Perevoshchikov 
Weighted Register Automata and Weighted Logic for Data Words 
17:30 
Program ends 
Thursday 28 April 
9:00 
Kim G. Larsen 
Invited talk: From Timed Automata to Stochastic Priced Timed Games – Combining Model Checking & Machine Learning
Abstract: Timed automata and games, priced timed automata and energy automata have emerged as useful formalisms for modeling realtime and energyaware systems as found in several embedded and cyberphysical systems. During the last 20 years the realtime 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 nearoptimal strategies for stochastic priced timed games. The lecture will review the various branches of UPPAAL and indicate their concerted applications to a range of realtime and cyberphysical examples.

10:00 
S. Lombardy, V. Marsault, N. Moreira, R. Reis, J. Sakarovitch 
The plateform VaucansonR 
10:30 
Break 
11:00 
Jiří Srba 
Invited talk: Weighted Dependency Graphs: Theory, Applications and Tools 
12:00 
Lunch 
13:30 
Karin Quaas 
Invited talk: MTLModel Checking of Weighted Automata with Weights in the Integers
Abstract: We investigate to which extent Metric Temporal Logic (MTL, for short), an extension of Linear Temporal Logic that is popular in the realtime community, can be used for model checking weighted automata with weights in the integers.

14:30 
Uli Fahrenberg 
Invited talk: StarContinuous Kleene OmegaAlgebras: Theory and Applications
Abstract: We have recently introduced a new algebraic structure of starcontinuous
Kleene omegaalgebras, motivated by certain Büchitype problems in socalled
energy automata. Starcontinuous Kleene omegaalgebras are semimodules over
starcontinuous Kleene algebras with an infinite product which satisfies
certain axioms. Their relation to continuous Kleene omegaalgebras is
similar to the relation of starcontinuous Kleene algebras to continuous
Kleene algebras.
We will introduce starcontinuous Kleene omegaalgebras 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.

15:30 
Break 
16:00 
Nicolas Markey 
Invited talk: Optimal strategies in weighted timed games: undecidability and approximation
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 arbitraryprecise approximations of the optimal weight can be computed.
This is joint work with Patricia Bouyer and Samy Jaziri.

17:00 
T. Denkinger 
An automata characterisation for weighted multiple contextfree grammars 
17:30 
Program ends 
20:00 
Workshop dinner at Duus Aalborg 
Friday 29 April 
9:00 
Axel Legay 
Invited talk: Statistical Model Checking: past, present, and future 
10:00 
D. Heusel, M. Droste, Z. Fülöp 
A Kleene Theorem for Weighted Tree Automata over Tree Valuation Monoids 
10:30 
Break 
11:00 
Franck van Breugel 
Invited talk: Computing Probabilistic Bisimilarity Distances via Policy Iteration
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.

12:00 
Lunch 
13:30 
E. Paul 
On Finite and Polynomial Ambiguity of Weighted Tree Automata 
14:00 
S. Dück 
Weighted Automata and Logics on Graphs 
14:30 
Conference ends 