Schedule

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