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.

Date Time Topic Speaker Room
2020 April 7 13:15-16:15 canceled due to Corona lockdown Johannes Fichte
(TU Dresden)
2020 April 21 12:45‑15:45 canceled due to Corona lockdown Rafael Penaloza  
2020 April 28 13:15-16:15 canceled due to Corona lockdown Robin Hirsch  
2020 May 5 12:45‑15:45 Reasoning about Finite Sets and Cardinality Constraints via Column Generation Filippo De Bortoli
(TU Dresden)
video conference
2020 May 12 12:45‑15:45 canceled due to Corona lockdown Martin Davis  
2020 May 19 13:15-16:15 A decomposition of finitely ambiguous weighted tree automata Kevin Stier
(Universität Leipzig)
video conference
2020 May 26 12:45‑15:45 canceled due to Corona lockdown Frank Wolter  
2020 June 9 13:15-16:15 About learning weighted automata Laure Daviaud video conference
2020 June 16 12:45‑15:45 Sequentiality of Group-Weighted Tree Automata Thomas Feller (TU Dresden) video conference
2020 June 30 13:15-16:15 PrIC3: Property Directed Reachability for MDPs Benjamin Kaminski
University College London)
video conference
2020 July 7 13:15‑16:15 The Bose-Nelson Sorting Problem for 11 and 12 Inputs Jannis Harder video conference
2020 July 14 12:45‑15:45 canceled Guillermo Alberto Perez  


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.


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.