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.
|2020 April 7||13:15-16:15||canceled due to Corona lockdown||Johannes Fichte
|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
|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
|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)
|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.