The color coding means:

: all participate
: Doctoral students participate
: next seminar

Please find the abstracts below the schedule and note that some of the slides are made available here, internally.

Abstracts

Laure Daviaud: About learning weighted automata

In this talk, I will present algorithms to learn deterministic finite automata (due to Angluin) and weigthed automata over the usual semiring R with addition and multiplication (due to Beimel, Bergadano, Bshouty, Kushilevitz and Varricchio). I will then present some related open questions and pinpoint the difficulty that arise when trying to generalise these algorithms to any semiring.

Thomas Feller: Sequentiality of Group-Weighted Tree Automata

We extend a paper by Laure Daviaud to weighted tree automata over commutative groups. We first define a fitting notion for the tree distance, introduce our automata model, and ultimately prove the equivalence between sequentiality, the Lipschitz property, and the twinning property.

Benjamin Kaminski: PrIC3: Property Directed Reachability for MDPs

IC3 has been a leap forward in symbolic model checking. We present PrIC3 (pronounced pricy-three), a conservative extension of IC3 to symbolic model checking of MDPs. Our main focus is to develop the theory underlying PrIC3. Alongside, we present a first implementation of PrIC3 including the key ingredients from IC3 such as generalization, repushing, and propagation.

Preprint: https://arxiv.org/abs/2004.14835

Jannis Harder: The Bose-Nelson Sorting Problem for 11 and 12 Inputs

Sorting networks are circuits that sort a fixed number of inputs using a single type of gate, a so called comparator that outputs the minimum and maximum of its two inputs.  
Determining the minimal number of comparators required for a sorting network with n inputs is known as the Bose-Nelson sorting problem, named after R.C. Bose and R.J. Nelson who first explored this problem in 1963. Computing this number is a very challenging problem, even for small n.  
In 1966, D.E. Knuth and R.W. Floyd first computed the answers for up to 8 inputs. The required computation took 20 hours on a CDC G-21 computer.  
It took almost 50 years for further progress to be made. In 2014, M. Codish, L. Cruz-Filipe, M. Frank and P. Schneider-Kamp computed the answers for 9 and 10 inputs using a new approach. Their computation took over 7 days on a 288-thread cluster.  
In this talk I will present a new search procedure for the Bose-Nelson sorting problem based on a new bound for partial sorting networks. This enabled the computation for 11 and 12 inputs in 5 hours on a single 24-core server. Using this approach, the previously known results can be computed within 5 seconds on a quad-core laptop.
 I will also present the strategy I used to formally verify this result.