Most of the the conference has been recorded. The collection of all edited videos can now be accessed through the Panopto instance of the univeristy of Kassel. Next to each recorded session/tutorial/invited talk/tools and open problems session, you can find a link taking you directly to the corresponding video.


Monday 08h00 - 08h55, Badges | lobby

Picking up name badge, registration, material reception.

Monday 08h55 - 09h00, Welcome | HS 3

Welcome and SafeToC guidelines

Monday 09h00 - 10h30, Tutorial | HS 3 | chair: Thomas Colcombet |

Edouard Bonnet - Twin-width and logic (Part 1)

We introduce the contraction sequences, which allow to define the twin-width of a graph and more generally the so-called reduced parameters. To form some intuition, we survey which classes have bounded twin-width and which do not. We first recast the proof of the Courcelle-Makowsky-Rotics theorem (on MSO model checking of classes of bounded clique-width) that uses the Feferman-Vaught theorem in the language of component twin-width --a reduced parameter. We then add a Gaifman-like locality argument to get a fixed-parameter tractable algorithm on classes of bounded twin-width, when given a witness of low twin-width. We show that transductions of bounded twin-width classes have bounded twin-width. We survey other connections of twin-width and logic, notably the characterizations that: -a class has bounded twin-width if and only if it is the transduction of a proper permutation class, -a class of totally ordered graphs has bounded twin-width if and only if it is monadically dependent.

Coffee Break

Monday 11h00 - 12h30, Tutorial | HS 3 | chair: Thomas Colcombet |

Edouard Bonnet - Twin-width and logic (Part 2)


Monday 14h30 - 16h00, Tutorial | HS 3 | chair: Supratik Chakraborty |

Bernd Finkbeiner - Logics and Algorithms for Hyperproperties (Part 1)

System requirements related to concepts like information flow, knowledge, and robustness cannot be judged in terms of individual system executions, but rather require an analysis of the relationship between multiple executions. Such requirements belong to the class of hyperproperties, which generalize classic trace properties to properties of sets of traces. During the past decade, a range of new specification logics has been introduced with the goal of providing a unified theory for reasoning about hyperproperties. This tutorial gives an overview of the current landscape of logics for the specification of hyperproperties and algorithms for satisfiability checking, model checking, monitoring, and synthesis.

Coffee Break

Monday 16h30 - 18h00, Tutorial | HS 3 | chair: Supratik Chakraborty |

Bernd Finkbeiner - Logics and Algorithms for Hyperproperties (Part 2)


Tuesday 08h00 - 08h55, Badges | lobby

Picking up name badge, registration, material reception.

Tuesday 08h55 - 09h00, Welcome | HS 3

Welcome and SafeToC guidelines

Tuesday 09h00 - 10h00, Keynote Speaker | HS 3 | chair: Bernd Finkbeiner |

Nathalie Sznajder - Synthesis of Distributed Synchronous Systems

The problem of distributed synthesis is to automatically generate a distributed algorithm, given a target communication network and a specification of the algorithm’s correct behavior. In this talk, I will first present the work that has been done since 1992 in order to solve the problem for static networks with an a priori fixed message size. I will show where the undecidability comes from, and when it is possible to obtain decidability results. Then I will present a recent work on synthesis of distributed systems with dynamic links. In fact, the classical approach has two shortcomings: Recent work in distributed computing is shifting towards dynamically changing communication networks rather than static ones, and an important class of distributed algorithms are so-called full-information protocols, where nodes piggy-pack previously received messages onto current messages. I will hence consider the synthesis problem for a system of two nodes communicating in rounds over a dynamic link whose message size is not bounded and show a necessary and sufficient condition for decidability of the problem.

Coffee Break

Tuesday 10h30 - 11h42, Contributed Talks

Automata and Languages 1 | HS 3 |
chair: Suguman Bansal
Games 1 | HS 4 |
chair: Alexander Rabinovich
Automata and Languages 1 | HS 3 | chair: Suguman BansalGames 1 | HS 4 | chair: Alexander Rabinovich
10h30-10h40 | Sandra Kiefer | HS 3
Revisiting the growth of polyregular functions
10h30-10h40 | Jakub Svoboda | HS 4
Stochastic Games with Bounded Treewidth
10h42-10h52 | Kyveli Doveri | HS 3
FORQ-based Language Inclusion Formal Testing⋆
10h42-10h52 | Benjamin Bisping | HS 4
Games to Decide All Behavioral Equivalences at Once
10h54-11h04 | David Purser | HS 3
The Big-O Problem for Max-Plus Automata is Decidable (PSPACE-Complete)
10h54-11h04 | Pierre Vandenhove | HS 4
How to Play Optimally for Regular Objectives?
11h06-11h16 | Gaëtan Staquet | HS 3
Automata with Timers
11h06-11h16 | Antonio Casares | HS 4
A characterization of positional omega-regular languages
11h18-11h28 | Amazigh AMRANE | HS 3
Developments in Higher-Dimensional Automata Theory
11h18-11h28 | Irmak Saglam | HS 4
Solving Odd-Fair Parity Games
11h30-11h40 | Michaël Cadilhac | HS 3
Parikh One-Counter Automata
11h30-11h40 | Ashwani Anand | HS 4
Permissiveness for Strategy Adaptation

Tuesday 14h00 - 15h00, Keynote Speaker | HS 3 | chair: Supratik Chakraborty |

Udi Boker - History-Determinism vs. Related Notions

We will explore the similarities and differences between history-determinism and related notions, such as good-for-games, guidability, determinizability-by-pruning, winning-token-games, and residuality.

Coffee Break

Tuesday 15h30 - 16h54, Contributed Talks

Verification, Model Checking, Reachability | HS 3 |
chair: Kuldeep Meel
Model Theory | HS 4 |
chair: Sandra Kiefer
Verification, Model Checking, Reachability | HS 3 | chair: Kuldeep MeelModel Theory | HS 4 | chair: Sandra Kiefer
15h30-15h40 | Suguman Bansal | HS 3
Model Checking Linear Temporal Logic over Finite Traces
15h30-15h40 | Ioannis Eleftheriadis | HS 4
Sparsity: from graphs to relational structures
15h42-15h52 | Nicolas Manini | HS 3
Computing Reachable Simulations
15h42-15h52 | Wojciech Przybyszewski | HS 4
Proving combinatorial properties of graphs using model theory
15h54-16h04 | Nicolas Waldburger | HS 3
Checking Presence Reachability Properties on Parameterized Shared-Memory Systems
15h54-16h04 | Radosław Piórkowski | HS 4
Universal quantification in automatic structures: an ExpSpace-hard nut to crack
16h06-16h16 | Corto Mascle | HS 3
Broadcast networks with local registers
16h06-16h16 | Tim Seppelt | HS 4
Logical Equivalences, Homomorphism Indistinguishability, and Forbidden Minors
16h18-16h28 | Pascal Baumann | HS 3
Checking Refinement of Asynchronous Programs against Context-Free Specifications
16h18-16h28 | Matthias Naaf | HS 4
Zero-One Laws in Semiring Semantics
16h30-16h40 | Ramanathan Thinniyam Srinivasan | HS 3
Context-Bounded Verification of Context-Free Specifications
16h30-16h40 | Benedikt Pago | HS 4
Lower bounds for Choiceless Polynomial Time via Symmetric XOR-circuits
16h42-16h52 | Zhendong Ang | HS 3
New Results of Membership Problems for Trace Languages
16h42-16h52 | Luca Oeljeklaus | HS 4
Simulating Logspace-Recursion with Logarithmic Quantifier Depth
16h54-17h04 | Daniel Mock | HS 4
Evaluating Restricted First-Order Counting Properties on Nowhere Dense Classes and Beyond


Wednesday 09h00 - 10h00, Keynote Speaker | HS 3 | chair: Christof Löding |

Sven Schewe - Automata for Profit and Pleasure

What could be greater fun than toying around with formal structures? One particularly beautiful structure to play with are automata over infinite words, and there is really no need to give any supporting argument for the _pleasure_ part in the title. But how about profit?
When using ω-regular languages as target languages for practical applications like Markov chain model checking, MDP model checking and reinforcement learning, reactive synthesis, or as a target for an infinite word played out in a two player game, the classic approach has been to first produce a deterministic automaton D that recognises that language. This deterministic automaton is quite useful: we can essentially play on the syntactic product of the structure and use the acceptance mechanism it inherits from the automaton as target. This is beautiful and moves all the heavy lifting to the required automata transformations.
But when we want even more profit in addition to the pleasure, the question arises whether deterministic automata are the best we can do. They are clearly good enough: determinism is as restrictive as it gets, and easily guarantees that one can just work on the product. But what we really want is the reverse: we want an automaton, so that we can work on the product, and determinism is just maximally restrictive, and therefore good enough for everything.
At Highlights, all will know that we can lift quite a few restrictions and instead turn to the gains we can make when we focus on the real needs of being able to work on the product. For Markov chains, this could be unambiguous automata, for MDPs this could be good-for-MDP automata, and for synthesis and games, it could be good-for-games automata.
We will shed a light to a few nooks and corners of the vast room available open questions and answers, with a bias MDPs analysis in general and reinforcement learning in particular.

Coffee Break

Wednesday 10h30 - 11h42, Contributed Talks

Games 2 | HS 3 |
chair: Benjamin Bisping
Logic | HS 4 |
chair: Marie Fortin
Games 2 | HS 3 | chair: Benjamin BispingLogic | HS 4 | chair: Marie Fortin
10h30-10h40 | Maximilian P. Weininger | HS 3
Stopping Criteria for Value Iteration on Stochastic~Games with Quantitative Objectives
10h30-10h40 | Benjamin J Scheidt | HS 4
Counting Homomorphisms from Hypergraphs of Bounded Generalised Hypertree Width: A Logical Characterisation
10h42-10h52 | K. S. Thejaswini | HS 3
Rabin Games and Colourful Trees
10h42-10h52 | Dylan Bellier | HS 4
Plan Logic
10h54-11h04 | Julie Parreaux | HS 3
Weighted Timed Games: decidability, stochastic strategies, and robustness
10h54-11h04 | Denis Kuperberg | HS 4
Positive First-Order Logic on Words and Graphs
11h06-11h16 | Alexis Reynouard | HS 3
Solving Timed Parity Games with Surprise
11h06-11h16 | Andrei Draghici | HS 4
Semenov Arithmetic, Affine VASS, and String Constraints
11h18-11h28 | Nathan Thomasset | HS 3
Finite-memory strategies in infinite concurrent two-player games
11h18-11h28 | Dhruv Nevatia | HS 4
An Automata-Theoretic Characterisation of Weighted First-Order Logic
11h30-11h40 | David Lidell | HS 4
ppLTLTT: Temporal testing for pure-past linear temporal logic formulas

Wednesday 14h00 - 15h24, Contributed Talks

Automata and Transducers | HS 3 |
chair: Sophie Pinchinat
VASS, Skolem and Petri Net Problems | HS 4 |
chair: Georg Zetzsche
Automata and Transducers | HS 3 | chair: Sophie PinchinatVASS, Skolem and Petri Net Problems | HS 4 | chair: Georg Zetzsche
14h00-14h10 | Rafał Stefański | HS 3
Monads, comonads, and transducers
14h00-14h10 | Henry Sinclair-Banks | HS 4
Coverability in VASS Revisited: Improving Rackoff’s Bounds to Obtain Conditional Optimaility
14h12-14h22 | Le Thanh Dung NGUYEN | HS 3
Implicit automata in typed λ-calculi (I, II and III)
14h12-14h22 | Mihir J Vahanwala | HS 4
Robust Positivity Problems for low-order Linear Recurrence Sequences
14h24-14h34 | Lia Schütze | HS 3
Unboundedness problems for machines with reversal-bounded counters
14h24-14h34 | A. R. Balasubramanian | HS 4
Reachability in Continuous Pushdown VASS
14h36-14h46 | Yahia Idriss Benalioua | HS 3
Refinement problems for recognizable relations
14h36-14h46 | Roland Guttenberg | HS 4
Geometry of Reachability Sets of Vector Addition Systems
14h48-14h58 | Asaf Yeshurun | HS 3
Dimension-Minimality and Primality of Counter Nets
14h48-14h58 | Sougata Bose | HS 4
History Deterministic Vector Addition Systems
15h00-15h10 | Prince Mathew | HS 3
One deterministic-counter automata
15h00-15h10 | Mihir J Vahanwala | HS 4
Skolem and Positivity Completeness of Ergodic Markov Chains
15h12-15h22 | Saina Sunny | HS 3
Closeness of Finite State Transducers
15h12-15h22 | Arka Ghosh | HS 4
Reachability in symmetric Petri nets with data
15h24-15h34 | Benjamin Bordais | HS 3
Well-behaving concurrent games: from local to global properties
Coffee Break

Wednesday 16h00 - 17h00, Highlights Business Meeing | TBA

"Highlights Business Meeting"


Thursday 09h00 - 10h00, Keynote Speaker | HS 3 | chair: Bernd Finkbeiner |

Sophie Pinchinat - Make attack-defense trees formal objects

We consider a highly classic model used by security expert to reason about ways to attack a system and to defend it. Introduced by Schneier in 1999, attack-defense trees mean to graphically represent how non-atomic goals (either of the attacker or of the defender) decompose into a combination of subgoals, or how they are countered, in an informal manner though.
Formal semantics for this informal model have been intensively studied the last decade, in order to enrich the set of formal method tools in risk analysis. We present this broad area of research, while focusing on our recent investigations to equip the model with a dynamic semantics that reflects the course of steps of an attack. In particular, we study natural decision problems, as well as the expressiveness of the model, that incidentally coincides with star-free languages.

Coffee Break

Thursday 10h30 - 11h42, Contributed Talks

Synthesis | HS 3 |
chair: Sven Schewe
Algorithms & Complexity | HS 4 |
chair: Meena Mahajan
Synthesis | HS 3 | chair: Sven ScheweAlgorithms & Complexity | HS 4 | chair: Meena Mahajan
10h30-10h40 | S Akshay | HS 3
Boolean Functional Synthesis: From One to All Skolem Functions
10h30-10h40 | Jonas Schmidt | HS 4
Dynamic constant-time parallel graph algorithms with sub-linear work
10h42-10h52 | Ayrat Khalimov | HS 3
Fully Generalized Reactivity (1) Synthesis
10h42-10h52 | Jennifer Todtenhoefer | HS 4
On the work of dynamic constant-time parallel algorithms for regular tree languages and context-free languages
10h54-11h04 | Satya Prakash Nayak | HS 3
Seamless Reactivity of Hybrid Control via Augmented Games
10h54-11h04 | GUNJAN KUMAR | HS 4
Approximate Model Counting: Is SAT Oracle More Powerful than NP Oracle?
11h06-11h16 | Alexander Rabinovich | HS 3
Synthesis of Infinite State Systems
11h06-11h16 | Kuldeep S. Meel | HS 4
Probabilistic Query Evaluation: The Combined FPRAS Landscape
11h18-11h28 | Prabhat Kumar Jha | HS 3
Games for Efficient Supervisor Synthesis
11h18-11h28 | Lorenzo Clemente | HS 4
Complexity of deciding equality of power series from combinatorial enumeration
11h30-11h40 | Patrick Wienhöft | HS 3
Strategy Synthesis in Markov Decision Processes Under Limited Sampling Access
11h30-11h40 | Marcin Przybylko | HS 4
Enumerating Partial Answers in Description Logics with Functional Roles
11h42-11h52 | Kuldeep Meel | HS 4
Distinct Elements in Streams: An Algorithm for the (Text) Book

Thursday 14h00 - 15h24, Contributed Talks

Formal Methods and Learning | HS 3 |
chair: Djordje Zikelic
Automata, Algebra & Languages | HS 4 |
chair: Mikolaj Bojanczyk
Formal Methods and Learning | HS 3 | chair: Djordje ZikelicAutomata, Algebra & Languages | HS 4 | chair: Mikolaj Bojanczyk
14h00-14h10 | Marco Sälzer | HS 3
About Limits In Formal Verification of Graph Neural Networks
14h00-14h10 | Rémi Morvan | HS 4
Algebras for Regular Relations
14h12-14h22 | Nina Runde | HS 3
On Learning MSO-Formulas
14h12-14h22 | Thomas Colcombet | HS 4
Cascades of condensations
14h24-14h34 | Debraj Chakraborty | HS 3
Formally-Sharp DAgger for MCTS: Lower-Latency Monte Carlo Tree Search using Data Aggregation with Formal Methods
14h24-14h34 | Antoine Amarilli | HS 4
Enumerating Regular Languages with Bounded Delay
14h36-14h46 | León Bohn | HS 3
Constructing Deterministic Parity Automata from Positive and Negative Examples
14h36-14h46 | Anton D Chernev | HS 4
A dual adjunction between Ω-automata and Wilke algebras
14h48-14h58 | Martin Lange | HS 3
Formal Reasoning about Influence in Natural Sciences Experiments
14h48-14h58 | Alexandre Terefenko | HS 4
Semantics of Attack-Defense Trees for Dynamic Countermeasures: a New Hierarchy of Star-free Languages
15h00-15h10 | Henning Urbat | HS 4
Nominal Topology for Data Languages
Coffee Break

Thursday 16h00 - 17h00, Special Session | HS 3 |

"Open Problems Tools and Experiments"


Friday 09h00 - 10h00, Keynote Speaker | HS 3 | chair: Slawek Lasota |

Meena Mahajan - Quantified Boolean Formulas and Proof Complexity

For several years, both proof complexity and practical solving focussed on propositional proof systems and detecting (un)satisfiability. In the last two decades, several proof systems for the more succinct Quantified Boolean Formulas QBFs have been proposed and studied, and several QBF solvers have been developed. This talk will give an overview of what has been achieved in QBF proof complexity, and how (if at all) it informs QBF solving.

Coffee Break

Friday 10h30 - 11h42, Contributed Talks

Probabilistic and Timed Systems | HS 3 |
chair: Michael Cadilhac
Games 3 | HS 4 |
chair: Maximilian P. Weininger
Probabilistic and Timed Systems | HS 3 | chair: Michael CadilhacGames 3 | HS 4 | chair: Maximilian P. Weininger
10h30-10h40 | Muqsit Azeem | HS 3
1–2–3–Go! Explainable Policies for Arbitrarily Large Parameterized Markov Decision Processes via Decision-Tree Generalization
10h30-10h40 | Vojtech Rehak | HS 4
Mean Payoff Optimization for Systems of Periodic Service and Maintenance
10h42-10h52 | Đorđe Žikelić | HS 3
MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives
10h42-10h52 | Aline Goeminne | HS 4
Multi-Weighted Reachability Games
10h54-11h04 | Paweł Parys | HS 3
The Probabilistic Rabin Tree Theorem
10h54-11h04 | Aditya Prakash | HS 4
Joker Games for checking History-Determinism
11h06-11h16 | Neha A Rino | HS 3
Timed Alignments
11h06-11h16 | Suman Sadhukhan | HS 4
Reachability Poorman Discrete-Bidding Games
11h18-11h28 | Govind Rajanbabu | HS 3
One timed model to unify them all! - A foundation for efficient MITL Model-checking
11h18-11h28 | Daniel Hausmann | HS 4
Solving Emerson-Lei Games via Zielonka Trees
11h30-11h40 | Florian Bruse | HS 3
Timed Recursive CTL

Friday 14h00 - 14h48, Contributed Talks

Model Theory & Logic | HS 3 |
chair: Ramanathan Thinniyam Srinivasan
Applications and Other Topics | HS 4 |
chair: Supratik Chakraborty
Model Theory & Logic | HS 3 | chair: Ramanathan Thinniyam SrinivasanApplications and Other Topics | HS 4 | chair: Supratik Chakraborty
14h00-14h10 | Michael Levet | HS 3
On the Descriptive Complexity of Groups without Abelian Normal Subgroups
14h00-14h10 | Muhammad Usama Sardar | HS 4
Comprehensive Specification and Formal Analysis of Attestation Mechanisms in Confidential Computing
14h12-14h22 | Nina Pardal | HS 3
Unified Foundations of Team Semantics via Semirings
14h12-14h22 | Fabian Vehlken | HS 4
Teaching reductions: Formal foundations
14h24-14h34 | Mikołaj Bojańczyk | HS 3
Polyregular functions on unordered trees of bounded height
14h24-14h34 | Maurice Herwig | HS 4
Problem-Specific Visual Feedback in Discrete Modelling
14h36-14h46 | Pascal Bergsträßer | HS 3
Membership Problems in Subclasses of Rational Relations
14h36-14h46 | Paul D Gallot | HS 4
The MIX2 language is not an EDT0L language