18.06.2024
The workshop starts at 4:15 pm and there will be a total of three speakers giving about 3 conference-length (25 min.) talks. This time the workshop will take place at the TU Dortmund: Otto-Hahn-Str. 12, room 3.031.
Jedrzej Kolodziejski (Lehrstuhl Informatik 1, TU Dortmund): Countdown logic, games and automata: bisimulation-invariant approach to (un)boundedness
Abstract: The modal mu-calculus, an extension of modal logic with fixpoint operators, is a widely applicable formalism valued for its good model-theoretic and algorithmic properties. It encompasses virtually all bisimulation-invariant logics such as LTL or CTL and is well-suited for describing infinitary properties such as ``there exists an infinite path''. However, (un)boundedness properties such as ``there exist arbitrarily long finite paths'' lie beyond the expressive power of the mu-calculus.
I will present the countdown mu-calculus, a novel extension of the mu-calculus with ordinal approximations of fixpoints, which captures such (un)boundedness properties. I will show how the classical logic~games~automata correspondence extends to suitably defined countdown games and countdown automata. Results obtained using this correspondence, as well as its limitations and open problems, will be discussed.
Based on joint work with Bartek Klin.
Benjamin Bordais (RC Trust, TU Dortmund): Comparing the Complexity of Learning LTL, CTL and ATL formulas
Abstract: We consider the problem of learning temporal logic formulas from examples of system behavior. Although learning temporal properties has crystallized as an effective mean to explain complex temporal behaviors, the theoretical understanding of the complexity of the learning decision problems remains largely unexplored. To address this, we study the complexity of the passive learning problems of three prominent temporal logics, Linear Temporal Logic (LTL), Computation Tree Logic (CTL) and Alternating-time Temporal Logic (ATL) and several of their fragments. In this talk, I will present some of our complexity results.
Fabian Vehlken (Ruhr University Bochum): Learning Tree-Pattern Transformations
Abstract: We are interested in the following algorithmic problem: given pairs {(t_i , t^* i )} i of labelled, ordered trees, learn a set of rules that explain common (structural) differences for all pairs of trees. More precisely, the learnt set of rules shall allow to transform t_i into t^*_i in few steps for each i in {1, . . . , n}.
We approach this problem by (1) introducing a pattern-based specification language for tree transformations; (2) studying the computational complexity of variants of the above algorithmic problem, e.g. showing NP-hardness for very restricted variants; and (3) solving the problem for datasets from CS education research by encoding it into propositional satisfiability and using a propositional SAT solver.
This talk is based on joint work with Daniel Neider, Leif Saballek, Johannes Schmidt und Thomas Zeume.
Further information can be found here.