Schedule #

Wednesday, Oct 4
 09.3010.30 Invited talk: AnneKathrin Schmuck
The Power of Feedback in a CyberPhysical 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 cyberphysical  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 selfregulation. While stability, reliability and robustness remain to be of uppermost importance in these systems, a controlinspired utilization of cyberphysical feedback loops for this purpose is lacking far behind. In this talk, I will discuss how a controlinspired view on formal methods for reliable software design can enable us to utilize the power of feedback for robust and adaptable cyberphysical system design.
 10.3011.00 Coffee break
 11.0012.40 Morning Session “Beyond finite words”
 12.4014.00 Lunch break
 14.0015.00 Invited talk: Daniel Neider
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 finitestate 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 errorprone 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 offtheshelf SAT and SMT solvers. We will see how this idea can be used to integrate userprovided 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.0015.30 Coffee break
 15.3016.30 Afternoon Session “Regular Separability”
 16.3017.30 Open Problems Session
 18.30 Dinner at Spinnrädl (included in registration)
 09.3010.30 Invited talk: AnneKathrin Schmuck

Thursday, Oct 5
 09.3010.30 Invited talk: Christoph Haase
Automata giving small certificates for big solutions (click for abstract)
This talk will survey recent results and underlying techniques showing that finitestate automata and generalizations thereof allow to decide existential formulas of various extensions of Presburger arithmetic, the firstorder theory of the integers with addition and order. Concretely, we will see an NP upper bound for existential Büchi arithmetic based on finitestate 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.3011.00 Coffee break
 11.0012.40 Morning Session “Subwords I”
 Pamela Fleischmann: αβFactorisation and the Binary Case of Simon’s Congruence PDF
 Henning Fernau: Synchronization and Diversity of Solutions PDF
 Max Wiedenhöft: Matching Patterns with Variables Under Simon’s Congruence PDF
 C. Aiswarya: On the Satisfiability of Contextfree String Constraints with SubwordOrdering PDF
 Irmak Sağlam: Checking Directedness of Regular and Contextfree Languages PDF
 12.4014.00 Lunch break
 14.0015.00 Invited talk: Sandra Kiefer
Properties of Polyregular Functions (click for abstract)
Regular functions are a wellstudied robust class of stringtostring functions, one of whose characterisations is that they are exactly the functions recognisable by twoway 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 twoway 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.0015.30 Coffee break
 15.3016.30 Afternoon Session “Subwords II”
 16.3017.00 Fachgruppensitzung
 18.0020.00 Dinner at Kullman’s Diner (not included, optional)
 20.0022.00 Bowling at Planet Bowling (included)
 09.3010.30 Invited talk: Christoph Haase

Friday, Oct 6
 09.3010.30 Invited talk: Joël Ouaknine
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 modelchecking questions.
 10.3011.00 Coffee break
 11.0012.20 Morning Session “Pumping, Parsing, and Playing”
 Christian Rauch: The Pumping Lemma for Regular Languages is Hard PDF
 Martin Lange: ErrorCorrecting Parsing – This Time We Want All! PDF
 Bianca Truthe: Strictly Locally Testable and Resources Restricted Control Languages in TreeControlled Grammars PDF
 Daniel Stan: Concurrent Stochastic Lossy Channel Games PDF
 12.2014.00 Lunch break
 09.3010.30 Invited talk: Joël Ouaknine