Schedule #

  • Wednesday, Oct 4

    • 09.30-10.30 Invited talk: Anne-Kathrin Schmuck
      The Power of Feedback in a Cyber-Physical World (click for abstract)
      Feedback allows systems to seamlessly and instantaneously adapt their
      behavior to their environment and is thereby the fundamental principle of life
      and technology -- it lets animals breathe, it stabilizes the climate, it allows
      airplanes to fly, and the energy grid to operate. During the last century,
      control technology excelled at using this power of feedback to engineer
      extremely stable, robust, and reliable technological systems.  With the
      ubiquity of computing devices in modern technological systems, feedback loops
      become cyber-physical -- the laws of physics governing technological, social or
      biological processes interact with (cyber) computing systems in a highly
      nontrivial manner, pushing towards higher and higher levels of autonomy and
      self-regulation. While stability, reliability and robustness remain to be of
      uppermost importance in these systems, a control-inspired utilization of
      cyber-physical feedback loops for this purpose is lacking far behind.  In this
      talk, I will discuss how a control-inspired view on formal methods for reliable
      software design can enable us to utilize the power of feedback for robust and
      adaptable cyber-physical system design. 
    • 10.30-11.00 Coffee break
    • 11.00-12.40 Morning Session “Beyond finite words”, Chair: Henning Fernau
    • 12.40-14.00 Lunch break
    • 14.00-15.00 Invited talk: Daniel Neider Slides (PDF)
      Reinforcement Learning with Reward Machines (click for abstract)
      Despite its great success, reinforcement learning struggles
      when the reward signal is sparse and temporally extended (e.g., in cases where
      the agent has to perform a complex series of tasks over a prolonged period of
      time). To expedite the learning process in such situations, a particular form
      of finite-state machines, called reward machines, has recently been shown to
      help immensely. However, designing a proper reward machine for the task at hand
      is challenging and remains a tedious and error-prone manual task.
      In this presentation, we will survey recent approaches that intertwine
      reinforcement learning and the inference of reward machines, thereby
      eliminating the need to craft a reward machine by hand. At their heart, these
      methods transform the inference task into a series of constraint satisfaction
      problems that can be solved using off-the-shelf SAT and SMT solvers. We will
      see how this idea can be used to integrate user-provided advice into the
      learning process and how it deals with stochastic reward signals. Moreover, we
      will briefly discuss theoretical properties and hint at empirical evidence
      demonstrating that reinforcement learning with reward machines outperforms
      existing methods, such as hierarchical and deep reinforcement learning.
    • 15.00-15.30 Coffee break
    • 15.30-16.30 Afternoon Session “Regular Separability”, Chair: Dietrich Kuske
    • 16.30-17.30 Open Problems Session
    • 18.30 Dinner at Spinnrädl (included in registration)
  • Thursday, Oct 5

    • 09.30-10.30 Invited talk: Christoph Haase Slides (PDF)
      Automata giving small certificates for big solutions (click for abstract)
      This talk will survey recent results and underlying techniques showing
      that finite-state automata and generalizations thereof allow to decide
      existential formulas of various extensions of Presburger arithmetic, the
      first-order theory of the integers with addition and order. Concretely, we will
      see an NP upper bound for existential Büchi arithmetic based on finite-state
      automata, and an EXPSPACE upper bound for Semenov arithmetic based on affine
      vector addition systems with states. I will also briefly touch some very recent
      work showing that existential Presburger arithmetic augmented with gcd
      constraints is decidable in NP. 
    • 10.30-11.00 Coffee break
    • 11.00-12.40 Morning Session “Subwords I”, Chair: Moses Ganardi
    • 12.40-14.00 Lunch break
    • 14.00-15.00 Invited talk: Sandra Kiefer Slides (PDF)
      Properties of Polyregular Functions (click for abstract)
      Regular functions are a well-studied robust class of string-to-string
      functions, one of whose characterisations is that they are exactly the
      functions recognisable by two-way deterministic finite automata with output.
      This implies that their growth rate --- i.e. the function describing the output
      length in terms of the input length --- is always linear. To go beyond linear
      growth, one can equip the two-way automata with multiple reading heads
      (pebbles), the number of which then still constitutes a bound on the degree of
      the polynomial describing the growth rate. The functions recognised by these
      pebble automata are called polyregular.
      Over the past years, the properties of polyregular functions have been studied
      intensively and various equivalent characterisations have been found. In the
      talk, I will give an introduction to the realm of polyregular functions by
      discussing some of those characterisations, with a focus on the logical one. I
      will also present simple constructions which refute that the aforementioned
      link between the growth exponent and number of heads is symmetric. That is, in
      general, the degree of the growth rate of a polyregular function is not (equal
      to or even a bound on) the minimum number of pebbles needed in an automaton to
      compute the function.
    • 15.00-15.30 Coffee break
    • 15.30-16.30 Afternoon Session “Subwords II”, Chair: Sandra Kiefer
    • 16.30-17.00 Fachgruppensitzung Slides (PDF)
    • 18.00-20.00 Dinner at Kullman’s Diner (not included, optional)
    • 20.00-22.00 Bowling at Planet Bowling (included)
  • Friday, Oct 6

    • 09.30-10.30 Invited talk: Joël Ouaknine Slides (PDF)
      What’s Decidable about Discrete Linear Dynamical Systems? (click for abstract)
      Discrete linear dynamical systems (LDS) are a fundamental modelling
      paradigm in several branches of science, and have been the subject of extensive
      research for many decades. Within Computer Science, LDS are used, for example,
      to analyse linear loops and Markov chains, and also arise in areas such as
      automata theory, differential privacy, control theory, and the study of formal
      power series, among others.
      Perhaps surprisingly, many decision problems concerning LDS (such as
      reachability of a given hyperplane, known as the *Skolem Problem*) have
      been open for many decades. In this talk, we explore the landscape of such
      problems, focussing in particular on model-checking questions.
    • 10.30-11.00 Coffee break
    • 11.00-12.20 Morning Session “Pumping, Parsing, and Playing”, Chair: Martin Kutrib
    • 12.20-14.00 Lunch break

Imprint | Data protection