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.
Timetable
Abstracts
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
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.
Zoltán Fülöp: Decidability of Finite-Image Property of Weighted Tree Automata over Past-finite Monotonic Strong Bimonoids
The semantics of a weighted tree automaton (wta) is a mapping from the set of trees to a weight structure. In this talk the weight structure is a strong bimonoid and we focus on the question whether a wta has the finite image property, i.e., the image of its semantics is finite. (1) We introduce past-finite monotonic strong bimonoids and give natural examples of them. (2) We give a characterization of wta over past-finite monotonic strong bimonoids which have the finite-image property. Using this result (3) we give sufficient conditions for the decidability of the finite-image property of such wta. Finally, (4) we show that the finite-image property is decidable for wta over past-finite monotonic semirings.
Giuseppe De Giacomo: Linear-time Temporal Logics over Finite Traces (World Logic Day)
In this talk we look at temporal logics on traces that are assumed to be finite, as typical of action planning in Artificial Intelligence and of processes modeling in Business Process Management. Having to deal with finite traces has been considered a sort of accident in much of the AI and BPM literature, and standard temporal logics (on infinite traces) have been hacked to fit this assumption. Only recently a specific interest in studying the impact of such an assumption has emerged. We first introduce the notion of Temporal Logic, and then we delve into the detail of Linear-time Temporal Logics on Finite Traces, reviewing the main results on satisfiability, verification, and synthesis, and also drawing connections with work in AI planning. The main catch is that working with these logics can be based on manipulation of regular automata on finite strings, simplifying greatly reasoning and especially synthesis.
Yvo Meeres: Finite State Automata for Directed Acyclic Graphs
Analogously to regular string and tree languages, regular directed graph (DAG) languages had been defined in literature. Although called regular, those DAG-languages are way more powerful and, consequently, standard problems have a higher complexity than in the string case. Top-down as well as bottom-up deterministic DAG languages are subclasses of the regular DAG languages. We refine this hierarchy by providing a weaker subclass of the deterministic DAG languages. Obviously, this weaker class exhibits beneficial algorithmic properties. For a DAG-automaton recognizing a language in this new DAG language class, a classical finite state automaton (FSA) can be constructed whose states enumerate the dangling edges throughout an appropriate run of the DAG-automaton. An edge is called dangling if not yet all of its vertices have been read in the run. This means that an FSA can be used for deciding membership of such DAGs.
The motivation behind this joint work with Johannes Blum and Frank Drewes is the transfer of results about regular string languages to graphs. Furthermore, we provide a characterization of the class via the DAG-automaton's rules.
Fan Feng: Two-way Weighted Transducers
To generalize the theory of two-way finite state transducers and weighted automata, we define the two-way weighted transducers over a complete semiring. Following the constructions for unweighted transducers and weighted automata, we get some similar results for weighted transducers in terms of union and composition. But for the Hadamard product there is still some problem and we are looking for a construction with the least restrictions.
