The color coding means:

: all participate
: Doctoral students participate

Please find the abstracts below the schedule and note that some of the slides are made available here, internally.

Plenary seminar sessions are hosted on Zoom. Student seminar sessions are hosted on a local instance of BigBlueButton. Access links can be found in the timetable below. Passcodes are going to be sent via e-mail, to the internal mailing list.

The passcodes to the virtual meetings can also be inquired from Sandy Seifarth.


Date Time Topic Speaker Room
Nov 3 2021 14:00 UTC Good-for-games vs. history-determinism in quantitative automata
(event from Online Worldwide Seminar on Logic and Semantics)
Karoliina Lehtinen
(Aix-Marseille University)
Link (Zoom)
Nov 9 2021 13:00-16:00

Mining EL Bases with Adaptable Role Depth

Ana Ozaki
(University of Bergen)
Link (Zoom)
Nov 16 2021 13:00-16:00 Parallel Parameterized Algorithms for Odd Cycle Transversal Max Bannach
(Universität zu Lübeck)
Link (BBB)
Nov 23 2021 13:00-16:00 Holonomic sequences Joël Ouaknine
(Max Planck Institute for Software Systems)
Link (Zoom)
Nov 30 2021 13:00-16:00 Trace Alignment and Timed-Trace Alignment: an Automata-based Approach Giuseppe Perelli
(Università di Roma, La Sapienza)
Link (Zoom)
Dec 7 2021 13:00-16:00 Model Checking Temporal Properties of Recursive Probabilistic Programs Tobias Winkler
(RWTH Aachen University)
Link (BBB)
Be Lazy and Don’t Care: Faster CTL Model Checking for Recursive State Machines Patrick Wienhöft
(TU Dresden)
Dec 14 2021 13:00-16:00 TBA TBA
Link (Zoom)
Jan 14 2022 13:00-16:00 World Logic Day TBA
Jan 18 2022 13:00-16:00 TBA Zoltán Fülöp
(University of Szeged)
Link (Zoom)
Jan 25 2022 13:00-16:00 TBA Yvo Meeres
(Universität Leipzig)
Link (BBB) 

Fan Feng
(Universität Leipzig)



Ana OzakI: Mining EL Bases with Adaptable Role Depth

In Formal Concept Analysis, a base for a finite structure is a set of implications that characterizes all valid implications of the structure. This notion can be adapted to the context of Description Logic, where the base consists of a set of concept inclusions instead of implications. In this setting, concept expressions can be arbitrarily large. Thus, it is not clear whether a finite base exists and, if so, how large concept expressions may need to be. We first revisit results in the literature for mining EL bases from finite interpretations. Those mainly focus on finding a finite base or on fixing the role depth but potentially losing some of the valid concept inclusions with higher role depth. We then present a new strategy for mining EL bases which is adaptable in the sense that it can bound the role depth of concepts depending on the local structure of the interpretation. Our strategy guarantees to capture all EL concept inclusions holding in the interpretation, not only the ones up to a fixed role depth.

Max Bannach: Parallel Parameterized Algorithms for Odd Cycle Transversal

The objective of the odd cycle transversal problem is to make a graph bipartite by removing just a few vertices. I motivate studying the family of graphs with bounded OCT number, provide some applications, and sketch the standard iterative compression method to find such sets in fpt-time. Only to find out, disappointed, that this algorithm is inherently sequential.
In the main part of the talk, I develop a parallel fpt-algorithm based on repetitive flow-computations. We will first observe that a small graph flow can be computed by a parallel fpt-algorithm. This insight allows us to implement a parallel algorithm for the vertex cover problem parameterized by tighter parameters than the vertex cover number, namely by the difference between this number and some lower bound such as the size of a maximal matching. While we are presumably not able to compute these lower bounds in parallel in general, we obtain them implicitly if we apply the framework to the odd cycle transversal problem – yielding the sought parallel parameterized algorithm.

Joël Ouaknine: Holonomic sequences

Holonomic techniques have deep roots going back to Wallis, Euler, and Gauss, and have evolved in modern times as an important subfield of computer algebra, thanks in large part to the work of Zeilberger and others over the past three decades. In this talk, I give an overview of the area, and in particular present a select survey of known and original results on decision problems for holonomic sequences and functions. I also discuss some surprising connections to the theory of periods and exponential periods, which are classical objects of study in algebraic geometry and number theory; in particular, I relate the decidability of certain decision problems for holonomic sequences to deep conjectures about periods and exponential periods, notably those due to Kontsevich and Zagier. No prior knowledge of any of the above is expected or required.

Giuseppe Perelli: Trace Alignment and Timed-Trace Alignment: an Automata-based Approach

One major task in business process management is that of "aligning" real traces of process executions with a process model, by minimally adding and deleting events.
This talk introduces the problem in the context of Declarative Process Mining, where specifications are expressed in Temporal Logics on finite traces.
First, we analyze an untimed version of the problem, using Linear-Time Temporal Logic over finite traces (LTLf) as a specification language and providing a sound and complete technique to synthesize the alignment instructions, which relies on finite automata-theoretic manipulations. The technique can be effectively implemented by resorting to planning technology, notably leading to a system that significantly outperforms all current state-of-the-art ad-hoc solutions.
Secondly a Timed-Trace version is also discussed, where we extend the approach to metric LTLf (MTLf), i.e., the extension of LTLf where time is dealt with numerically. The resulting setting introduces significant technical challenges and requires a more sophisticated machinery than that for finite-state automata. We conclude by discussing possible future developments.

Tobias Winkler: Model Checking Temporal Properties of Recursive Probabilistic Programs

Probabilistic pushdown automata (pPDA) are a standard operational model for programming languages involving discrete random choices, procedures, and returns. Temporal properties are useful for gaining insight into the chronological order of events during program execution. Existing approaches in the literature have focused mostly on omega-regular and LTL properties. In this paper, we study the model checking problem of pPDA against omega-visibly pushdown languages that can be described by specification logics such as CaRet and are strictly more expressive than omega-regular properties. With these logical formulae, it is possible to specify properties that explicitly take the structured computations arising from procedural programs into account. For example, CaRet is able to match procedure calls with their corresponding future returns, and thus allows to express fundamental program properties like total and partial correctness.

Patrick Wienhöft: Be Lazy and Don’t Care: Faster CTL Model Checking for Recursive State Machines

Recursive state machines (RSMs) are state-based models for procedural programs with wide-ranging applications in program verification and interprocedural analysis. Model-checking algorithms for RSMs and related formalisms and various temporal logic specifications have been intensively studied in the literature.
In this paper, we devise a new model-checking algorithm for RSMs and requirements in computation tree logic (CTL) that exploits the compositional structure of RSMs by ternary model checking in combination with a lazy evaluation scheme. Specifically, a procedural component is only analyzed in those cases in which it might influence the satisfaction of the CTL requirement. We evaluate our prototypical implementation on randomized scalability benchmarks and on an interprocedural data-flow analysis of Java programs, showing both practical applicability and significant speedups in comparison to state-of-the-art model-checking tools for procedural programs.