Monday
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  
We introduce the contraction sequences, which allow to define the twinwidth of a graph and more generally the socalled reduced parameters. To form some intuition, we survey which classes have bounded twinwidth and which do not. We first recast the proof of the CourcelleMakowskyRotics theorem (on MSO model checking of classes of bounded cliquewidth) that uses the FefermanVaught theorem in the language of component twinwidth a reduced parameter. We then add a Gaifmanlike locality argument to get a fixedparameter tractable algorithm on classes of bounded twinwidth, when given a witness of low twinwidth. We show that transductions of bounded twinwidth classes have bounded twinwidth. We survey other connections of twinwidth and logic, notably the characterizations that: a class has bounded twinwidth if and only if it is the transduction of a proper permutation class, a class of totally ordered graphs has bounded twinwidth if and only if it is monadically dependent.
Coffee Break
Monday 11h00  12h30, Tutorial  HS 3  
Lunch
Monday 14h30  16h00, Tutorial  HS 3  
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  
Tuesday
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  
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 socalled fullinformation protocols, where nodes piggypack 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   Games 1  HS 4  
Revisiting the growth of
polyregular functions
Revisiting the growth of polyregular functionsPolyregular functions are the class of stringtostring functions definable by pebble transducers, an extension of finitestate automata with outputs and multiple twoway reading heads (pebbles) with a stack discipline. If a polyregular function can be computed with k pebbles, then its output length is bounded by a polynomial of degree k in the input length. But Bojańczyk has shown that the converse fails. We provide two alternative easier proofs. The first establishes by elementary means that some quadratic polyregular function requires 3 pebbles. The second proof  just as short, albeit less elementary  shows a stronger statement: for every k, there exists some polyregular function with quadratic growth whose output language differs from that of any kfold composition of macro tree transducers (and which therefore cannot be computed by a kpebble transducer). Along the way, we also refute a conjectured logical characterization of polyblind functions. 
Stochastic Games with Bounded
Treewidth
Stochastic Games with Bounded TreewidthTurnbased stochastic games (aka simple stochastic games) are twoplayer zerosum games played on directed graphs with probabilistic transitions.The goal of playermax is to maximize the probability to reach a target state against the adversarial playermin.These games lie in NP ∩ coNP but the existence of polynomialtime algorithm is a major open question, all known deterministic algorithms require exponential time in the worstcase.An important open question has been whether faster algorithms can be obtained parametrized by the treewidth of the game graph.In this work our main result is a deterministic algorithm to solve turnbased stochastic games that, given a gamewith n states, treewidth at most t, and the bitcomplexity of the probabilistic transition function log D, has running time O((tn^2 log D)^(t log n)). In particular, our algorithm is quasipolynomial time for games with constant or polylogarithmic treewidth.The main result was published in SODA'23. 
FORQbased Language Inclusion
Formal Testing⋆
FORQbased Language Inclusion Formal Testing⋆We propose a novel algorithm to decide the language inclusion between (nondeterministic) Buchi automata, a PSpacecomplete problem. Our approach, like others before, leverage a notion of quasiorder to prune the search for a counterexample by discarding candidates which are subsumed by others for the quasiorder. Discarded candidates are guaranteed to not compromise the completeness of the algorithm. The novelty of our work lies in the quasiorder used to discard candidates. We introduce FORQs (family of right quasiorders) that we obtain by adapting the notion of family of right congruences put forward by Maler and Staiger in 1993. We define a FORQbased inclusion algorithm which we prove correct and instantiate it for a specific FORQ, called the structural FORQ, induced by the Buchi automaton to the right of the inclusion sign. The resulting implementation, called Forklift, scales up better than the stateoftheart on a variety of benchmarks including benchmarks from program verification and theorem proving for word combinatorics. 
Games to Decide All Behavioral
Equivalences at Once
Games to Decide All Behavioral Equivalences at OnceHow to elegantly determine the best fit of (in)equivalences for a pair of processes? We generalize the wellknown bisimulation game to find distinguishing HennessyMilner logic formulas for finitestate processes covering van Glabbeek's lineartime–branchingtime spectrum. By quantifying expressive power along six dimensions, we can quickly identify distinctions belonging to the coarsest distinguishing behavioral preorders and equivalences. The compared processes are equivalent in each coarser behavioral equivalence from the spectrum.The core of the talk is based on joint work with David N. Jansen and Uwe Nestmann, published in LMCS https://doi.org/10.46298/lmcs18(3:19)2022. A prototype implementation of our generic equivalencechecking runs on https://equiv.io/. 
The BigO Problem for MaxPlus
Automata is Decidable (PSPACEComplete)
The BigO Problem for MaxPlus Automata is Decidable (PSPACEComplete)We show that the bigO problem for maxplus automata, i.e. weighted automata over the semiring (N ∪ {∞}, max, +), is decidable and PSPACEcomplete. The bigO (or affine domination) problem asks whether, given two maxplus automata computing functions f and g, there exists a constant c such that f ≤ cg + c. This is a relaxation of the containment problem asking whether f ≤ g, which is undecidable. Our decidability result uses Simon's forest factorisation theorem, and relies on detecting specific elements, that we call witnesses, in a finite semigroup closed under two special operations: stabilisation and flattening.Joint work with Laure Daviaud. 
How to Play Optimally for
Regular Objectives?
How to Play Optimally for Regular Objectives?We study twoplayer zerosum games played on graphs and make contributions toward the following question: given an objective, how much memory is required to play optimally for that objective? We study regular objectives, where the goal of one of the two players is that eventually the sequence of colors along the play belongs to some regular language of finite words. We obtain different characterizations of the chromatic memory requirements for such objectives for both players, from which we derive complexitytheoretic statements: deciding whether there exist small memory structures sufficient to play optimally is NPcomplete for both players. Some of our characterization results apply to a more general class of objectives: topologically closed and topologically open sets.These results are based on joint work with Patricia Bouyer, Nathanaël Fijalkow, and Mickael Randour. 
Automata with Timers
Automata with TimersRecently, Frits W. Vaandrager et al. [1] studied learning (automatic construction using the wellknown L* algorithm [2]) finite state machines augmented with a timer. Timers are an often used mechanism in many contexts, such as network protocol and control software, in which a system sends a message and, if after a certain amount of time, an acknowledgement message is not received, the system sends the same message, i.e., we rely on a timer.In a machine with timers, we start a timer by setting it at a certain constant. Whenever a timer reaches zero, it produces a special "time out" symbol that triggers a transition in the finite state machine. Obtaining a learning algorithm for machines with multiple timers is not easy as multiple actions can occur at the same time (if multiple timers reach zero concurrently, for instance). In these "races", the machine decides nondeterministically in which order these actions are processed. Moreover, a transition may kill or restart a timer. It is thus not easy, from an execution trace containing races, to be certain of whether a timer is active and, if it is, at which value it was set. Moreover, as these races do not appear in the single timer case, we can not straightforwardly extend the techniques from [1].Therefore, in this joint work with Véronique Bruyère (University of Mons), Guillermo A. Pérez (University of Antwerp), and Frits W. Vaandrager (Radboud Universiteit), we lay the first steps towards a learning algorithm for finite state machines augmented with a finite number of timers by studying how one can remove these races while still observing the actions in the same order. We also prove that the reachability problem is PSPACEcomplete.[1] Frits W. Vaandrager, Roderick Bloem, Masoud Ebrahimi. Learning Mealy Machines with One Timer. Information and Computation (2023).[2] Dana Angluin. Learning Regular Sets from Queries and Counterexamples. Information and computation 75.2 (1987). 
A characterization of positional
omegaregular languages
A characterization of positional omegaregular languagesIn the context of infinite duration games over graphs, a central question is: For which objectives can the existential player always play optimally using positional (memoryless) strategies? We present a characterization of positionality for the class of omegaregular objectives. Namely, an omegaregular objective is positional if and only if it is recognized by a goodforgames parity automaton admitting a total order over its set of states such that its transitions satisfy some monotonicity properties with respect to this order. Using this characterization, we hope to answer many open questions concerning positionality in the case of omegaregular objectives, including obtaining finitetoinfinite and 1to2players arenas lifts and the closure under union of prefixindependent positional objectives.This talk is based on ongoing work with Pierre Ohlmann. 
Developments in
HigherDimensional Automata Theory
Developments in HigherDimensional Automata TheoryHigher dimensional automata (HDAs) were introduced by Pratt and van Glabbeek as a general geometric model for noninterleaving concurrency generalizing standard finite automata, but also Petri nets and event structures. In this setup, autoconcurrency is allowed and events may have a duration. Uli Fahrenberg et al have recently introduced languages of HDAs, which consist of subsumptionclosed sets of partially ordered multisets with interfaces (ipomsets), and shown a Kleene theorem and a MyhillNerode theorem for them. In this work we further develop the language theory of HDAs. We show a Pumping Lemma which allows us to expose a class of nonregular ipomset languages. We show that inclusion of regular languages is decidable (hence is emptiness), and that intersections of regular languages are again regular. On the other hand, no universal finite HDA exists, so complements of regular languages are not regular. We introduce a widthbounded version of complement and show that widthbounded complements of regular languages are again regular. 
Solving OddFair Parity
Games
Solving OddFair Parity GamesThis talk discusses the problem of efficiently solving parity games whereplayer Odd has to obey an additional strong transition fairness constraint onits vertices. We call such games Oddfair Parity games. Banerjee et. al. showed that Oddfair parity games can be solved via a fixedpoint formula thathighly resembles the one for ‘regular’ parity games. In this talk, we presenta new a Zielonkatype algorithm for solving Oddfair parity games, which notonly shares the same worstcase complexity as Zielonka’s algorithm for regularparity games but also preserves the algorithmic advantage that Zielonka’s algorithm possesses over other parity solvers with exponential time complexity, suchas Banerjee et. al.’s fixedpoint algorithm. Zielonka’s algorithm’s establishedreputation for solving parity games efficiently makes the Oddfair Zielonka’s algorithm presented in this talk the best known generic algorithm to solve Oddfairparity games. 
Parikh OneCounter
Automata
Parikh OneCounter AutomataCounting abilities in finite automata are traditionally provided by two orthogonal extensions: adding a single counter that can be tested for zeroness at any point, or adding Zvalued counters that are tested for equality only at the end of runs. In this talk, I will report on finite automata extended with both types of counters. They are called Parikh OneCounter Automata (POCA): the ``Parikh'' part referring to the evaluation of counters at the end of runs, and the ``OneCounter'' part to the single counter that can be tested during runs. Their expressiveness, in the deterministic and nondeterministic variants, is investigated; it is shown in particular that there are deterministic POCA languages that cannot be expressed without nondeterminism in the original models. The natural decision problems are also studied; strikingly, most of them are no harder than in the original models. A parametric version of nonemptiness is also considered. Based on joint work with Arka Ghosh, Guillermo A. Pérez, and Ritam Raha. 
Permissiveness for Strategy
Adaptation
Permissiveness for Strategy AdaptationGames on graphs provide an effective way of constructing systems that keep running while fulfilling their tasks at hand, under presence of physical environments. Such games however inherently assume that the environment is always antagonistic, and are solved by computing one strategy that allows the system to win against all moves of the environment. But in practice, the environment rarely acts adversarial (in fact, it might even be possible to control the environment agents), and the operating conditions rarely remain static to allow only one strategy to be sufficient. It is due to this drawback that games on graphs have found limited application in the construction of codependent systems operating in transient conditions. The key missing ingredient in the remedy of the mentioned problems is the notion of permissiveness of the agents strategies involved in the game being played.There have been attempts to incorporate permissiveness into the synthesis of strategies, but with limited success. With the goal to automatically obtain resilient and teamplaying systems to solve distributed ω regular tasks, in ourwork, we present novel ways to produce permissive strategies that enable the systems to negotiate with other systems automatically.To this end, in our work, we formalize the notions of permissive assumption on the environment [1] and permissive strategies for the system [2]. We then use novel templates to describe both for a game on a graph. With that in place we give polynomial time algorithms to compute permissive assumptions and permissive strategies for ωregular objectives. Furthermore, we give polynomial time algorithms to compose objectives, to build faulttolerant strategies, and toautomatically negotiate with other agents to complete different tasks.This is joint work with Kaushik Mallik, Satya Prakash Nayak and AnneKathrin Schmuck.References:1. Anand, A., Mallik, K., Nayak, S. P., and Schmuck, A.K. Computing adequately permissive assumptions for synthesis. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS, 2023), ETAPS2. Anand, A., Nayak, S. P., and Schmuck, A.K. Synthesizing permissive winning strategy templates for parity games. Tech. rep., 2023. To appear in 35th International Conference on Computer Aided Verification (CAV) 2023. 
Lunch
Tuesday 14h00  15h00, Keynote Speaker  HS 3  
We will explore the similarities and differences between historydeterminism and related notions, such as goodforgames, guidability, determinizabilitybypruning, winningtokengames, and residuality.
Coffee Break
Tuesday 15h30  16h54, Contributed Talks



Verification, Model Checking, Reachability  HS 3   Model Theory  HS 4  
Model Checking Linear Temporal
Logic over Finite Traces
Model Checking Linear Temporal Logic over Finite TracesRecent years have witnessed a growing interest in reasoning about the finitehorizon counterpart of $\ltl$, called $\ltlf$, for systems of unbounded but finite horizons. While the problems of satisfiability and synthesis from $\ltlf$ specifications have been studied extensively, the verification problem has surprisingly been overlooked. To this end, this work presents the \emph{first} study of modelchecking from $\ltlf$ specifications. We observe that there are striking differences between $\ltlf$ and $\ltl$ model checking. Most significantly, under the same nonterminating semantics of models, $\ltlf$ model checking is $\expspace$complete, making it exponentially harder than $\ltl$ model checking. This is unexpected since one of the attributes behind the success of $\ltlf$ is that problems over $\ltlf$ have so far been {\em perceived} to be at most as hard as thoseon $\ltl$, if not easier. For instance, (a). reasoning about $\ltlf$ deals with automata over finite words whereas $\ltl$ requires automata over infinitewords, (b). the complexity of reactive synthesis and satisfiability from $\ltlf$ and $\ltl$ are identical, and so on.We also show that under \emph{terminating} semantics, $\ltlf$ model checking is \pspacecomplete. Thus, demonstrating the importance of semantics in model checking for finitehorizon temporal specifications. 
Sparsity: from graphs to
relational structures
Sparsity: from graphs to relational structuresNowhere density is a seminal notion in algorithmic graph theory and combinatorics, that generalises numerous wellbehaved properties of classes of finite graphs. For monotone classes, nowhere density appears to be a key dividing line that separates tame from wild behaviour. From the perspective of model theory, Adler and Adler established that the monotone nowhere dense classes are precisely those that are monadically NIP, i.e. they do not transduce the class of all graphs, and conjectured that the same phenomenon occurs for classes of arbitrary relational structures and their corresponding Gaifman graphs. In this talk, I discuss recent results of Braunfeld, Dawar, Eleftheriadis, and Papadopoulos (2023) that settle the question of AdlerAdler, and survey few results from graph sparsity theory that generalise to the relational setting. 
Computing Reachable
Simulations
Computing Reachable SimulationsWe study the problem of computing reachable blocks of the simulation equivalence and design algorithms for this problem by interleaving reachability and simulation computation while possibly avoiding the computation of all the reachable states or the whole simulation preorder.The interest in computing simulation blocks stems from the fact that simulation provides a better state space reduction than other equivalence notions such as bisimilarity, yet retaining enough precision for model checking.On the other hand, the problem turns out to be significantly harder than the one for the bisimulation case.We put forward a sound algorithm manipulating state partitions and relations between their blocks, suited for processing infinitestate systems. This is a joint work with Pierre Ganty and Francesco Ranzato. 
Proving combinatorial properties
of graphs using model theory
Proving combinatorial properties of graphs using model theoryA pinnacle of sparsity theory, initiated by Nešetřil and Ossona de Mendez, is the result of Grohe, Kreutzer, and Siebertz which identifies subgrafclosed classes of graphs with FPT model checking as exactly nowhere dense classes. One of the key steps in the proof is characterizing nowhere dense classes of graphs in terms of a game called the Splitter game. There is an ongoing effort aimed at generalizing sparsity theory to classes of graphs that are not necessarily sparse. One of the most recent steps toward this goal is an analogous characterization of monadically stable classes of graphs (which contain FOinterpretations of nowhere dense graphs) in terms of a game called the Flipper game [Gajarský et al., arXiv:2301.13735]. The interesting thing is that the paper presents two different proofs of the characterization – one is a direct combinatorial proof, while the other one relies on tools from ("infinite") model theory.There is also a notion of a canonical strategy in the Flipper game [Gajarský et al., arXiv:2303.01473]. This time, the only presented proof uses tools from model theory and it is not obvious how to reprove the result in a combinatorial way. In my talk I'll present a simplified version of this result. Namely, I'll sketch a model theoretic proof that in nowhere dense classes of graphs there are at most a constant number of progressing moves for Splitter in the Splitter game. Although this is a purely combinatorial theorem, the only proof we know (so the one I'll sketch) relies on the compactness theorem for firstorder logic. 
Checking Presence Reachability
Properties on Parameterized SharedMemory Systems
Checking Presence Reachability Properties on Parameterized SharedMemory SystemsWe consider the verification of distributed systems composed of an arbitrary number of asynchronous processes. Processes are identical finitestate machines communicating by reading from and writing to a shared memory. Beyond the standard model with finitely many registers, we tackle roundbased sharedmemory systems with fresh registers at each round. In the latter model, both the number of processes and the number of registers are unbounded, making verification particularly challenging. The properties studied are generic presence reachability objectives that subsume classical questions such as safety or synchronization by expressing the presence or absence of processes in some states. In the more general roundbased setting, we establish that the parameterized verification of presence reachability properties is PSPACEcomplete. Moreover, for the roundless model with finitely many registers, we prove that the complexity drops down to NPcomplete and we provide several natural restrictions that make the problem solvable in polynomial time. 
Universal quantification in
automatic structures: an ExpSpacehard nut to crack
Universal quantification in automatic structures: an ExpSpacehard nut to crackAutomatic structures are structures whose universe and relations can be represented as regular languages. It follows from the standard closure properties of regular languages that the firstorder theory of an automatic structure is decidable. While existential quantifiers can be eliminated in linear time by application of a homomorphism, universal quantifiers are commonly eliminated via the identity ∀x. Φ ≡ ¬(∃x. ¬Φ). If Φ is represented in the standard way as an NFA, a priori this approach results in a doubly exponential blowup. However, the recent literature has shown that there are classes of automatic structures for which universal quantifiers can be eliminated without this blowup when treated as firstclass citizens and not resorting to double complementation. While existing lower bounds for some classes of automatic structures show that a singly exponential blowup is unavoidable when eliminating a universal quantifier, it is not known whether there may be better approaches that avoid the naïve doubly exponential blowup. We answer this question negatively.In my presentation, starting with a short introduction to the field of automatic structures, I will outline the construction of a family of NFA representing automatic relations for which the minimal NFA recognising the language after a universal projection step is doubly exponential, and deciding whether this language is empty is ExpSpacecomplete.Keywords: automatic structures, universal projection, tiling problems, state complexityAuthors: Christoph Haase, R.P. 
Broadcast networks with local
registers
Broadcast networks with local registersWe consider the parameterized verification of a model representing an arbitrarily large network of agents which communicate by broadcasting and receiving messages. The broadcast topology is reconfigurable, hence a message sent may be received by an arbitrary subset of agents. Agents have local registers which contain identifiers. They may broadcast, receive, store and compare these values using their registers. We consider the coverability problem, where one asks whether a given state of the system may be reached by at least one agent. We show that this problem is decidable using a refined abstraction of runs; however, it is as hard as coverability in lossy channel systems, which is HyperAckermannian. We contrast this with the undecidability of the closelyrelated target reachability problem on one hand, and with the NPcompleteness of the problem when each agent has only one register on the other.This is joint work with Lucie Guillou and Nicolas Waldburger. 
Logical Equivalences,
Homomorphism Indistinguishability, and Forbidden Minors
Logical Equivalences, Homomorphism Indistinguishability, and Forbidden MinorsTwo graphs $G$ and $H$ are \emph{homomorphism indistinguishable} over a class of graphs $\mathcal{F}$ if for all graphs $F \in \mathcal{F}$ the number of homomorphisms from $F$ to $G$ is equal to the number of homomorphisms from $F$ to $H$.Many natural equivalence relations comparing graphs such as (quantum) isomorphism, spectral, and logical equivalences can be characterised as homomorphism indistinguishability relations over certain graph classes.In this talk, the interplay of the properties of a graph class and its homomorphism indistinguishability relation are studied.As an application, \emph{selfcomplementarity}, a property of logics on graphs satisfied by many wellstudied logics, is identified. It is proven that the equivalence over a selfcomplementary logic admitting a characterisation as homomorphism indistinguishability relation can be characterised by homomorphism indistinguishability over a minorclosed graph class.Thereby, first evidences are provided for a possible connection between minors and homomorphism indistinguishability as conjectured by Roberson~(2022). 
Checking Refinement of
Asynchronous Programs against ContextFree Specifications
Checking Refinement of Asynchronous Programs against ContextFree SpecificationsIn the languagetheoretic approach to refinement verification, we check that the language of traces of an implementation all belong to the language of a specification. We consider the refinement verification problem for asynchronous programs against specifications given by a Dyck language. We show that this problem is EXPSPACEcomplete  the same complexity as that of language emptiness and for refinement verification against a regular specification. Our algorithm uses several novel technical ingredients. First, we show that checking if the coverability language of a succinctly described vector addition system with states (VASS) is contained in a Dyck language is EXPSPACEcomplete. Second, in the more technical part of the proof, we define an ordering on words and show a downward closure construction that allows replacing the (contextfree) language of each task in an asynchronous program by a regular language. Unlike downward closure operations usually considered in infinitestate verification, our ordering is not a wellquasiordering, and we have to construct the regular language ab initio. Once the tasks can be replaced, we show a reduction to an appropriate VASS and use our first ingredient. In addition to the inherent theoretical interest, refinement verification with Dyck specifications captures common practical resource usage patterns based on reference counting, for which few algorithmic techniques were known.Based on joint work with Moses Ganardi, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche for ICALP 2023. 
ZeroOne Laws in Semiring
Semantics
ZeroOne Laws in Semiring SemanticsSemiring semantics evaluates logical statements by values in a commutative semiring, which can model information such as costs or access restrictions. Random semiring interpretations, induced by a probability distribution on the semiring, generalise random structures, which raises the question to what extent the classical 01 laws of firstorder logic apply to semiring semantics.In this talk, we will see that a 01 law holds for for many semirings, that is, every firstorder sentence asymptotically almost surely evaluates to a unique semiring value on random semiring interpretations. For finite and infinite lattice semirings, we further show that only three semiring values are possible: 0, 1, and the smallest nonzero value. The proof is a combination of the classical extension axioms and an algebraic representation of firstorder sentences tailored to semiring semantics.Joint work with Erich Grädel, Hayyan Helal, and Richard Wilke. 
ContextBounded Verification of
ContextFree Specifications
ContextBounded Verification of ContextFree SpecificationsA fundamental problem in refinement verification is to check that the language of behaviors of an implemen tation is included in the language of the specification. We consider the refinement verification problem where the implementation is a multithreaded shared memory system modeled as a multistack pushdown automaton and the specification is an inputdeterministic multistack pushdown language. Our main result shows that the contextbounded refinement problem, where we ask that all behaviors generated in runs of bounded number of context switches belong to a specification given by a Dyck language, is decidable and coNPcomplete. The more general case of inputdeterministic languages follows, with the same complexity.Contextbounding is essential since emptiness for multipushdown automata is already undecidable, and so is the refinement verification problem for the subclass of regular specifications. Inputdeterministic languages capture many nonregular specifications of practical interest and our result opens the way for algorithmic analysis of these properties. The contextbounded refinement problem is coNPhard already with deterministic regular specifications; our result demonstrates that the problem is not harder despite the stronger class of specifications. Our proof introduces several general techniques for formal languages and counter programs and shows that the search for counterexamples can be reduced in nondeterministic polynomial time to the satisfiability problem for existential Presburger arithmetic.These techniques are essential to ensure the coNP upper bound: existing techniques for regular specifications are not powerful enough for decidability, while simple reductions lead to problems that are either undecidable or have high complexities. As a special case, our decidability result gives an algorithmic verification technique to reason about reference counting and reentrant locking in multithreaded programs.This is joint work with Pascal Baumann, Moses Ganardi, Rupak Majumdar and Georg Zetzsche. 
Lower bounds for Choiceless
Polynomial Time via Symmetric XORcircuits
Lower bounds for Choiceless Polynomial Time via Symmetric XORcircuitsChoiceless Polynomial Time (CPT) is one of the few remaining candidate logics for capturing PTIME. We make progress towards separating CPT from polynomial time by firstly establishing a connection between the expressive power of CPT and the existence of certain symmetric circuit families, and secondly, proving lower bounds against these circuits. We focus on the isomorphism problem of unordered CaiFürerImmermangraphs (the CFIquery) as a potential candidate for separating CPT from P. Results by Dawar, Richerby and Rossman, and subsequently by Pakusa, Schalthöfer and Selman show that the CFIquery is CPTdefinable on linearly ordered and preordered base graphs with small colour classes. We define a class of CPTalgorithms, that we call "CFIsymmetric algorithms", which generalises all the known ones, and show that such algorithms can only define the CFIquery on a given class of base graphs if there exists a family of symmetric XORcircuits with certain properties. These properties include that the circuits have the same symmetries as the base graphs, are of polynomial size, and satisfy certain fanin restrictions. Then we prove that such circuits with slightly strengthened requirements (i.e. stronger symmetry and fanin and fanout restrictions) do not exist for the ndimensional hypercubes as base graphs. This almost separates the CFIsymmetric algorithms from polynomial time  up to the gap that remains between the circuits whose existence we can currently disprove and the circuits whose existence is necessary for the definability of the CFIquery by a CFIsymmetric algorithm. 
New Results of Membership
Problems for Trace Languages
New Results of Membership Problems for Trace LanguagesIn dynamic analysis of programs, one observes an execution (sequence of events) and checks whether the execution satisfies or violates some property. When the programs are concurrent, such a simple check is often not robust to nondeterministic thread scheduling. In this case, the more appropriate question is the predictive version: given an execution, is there a semantically equivalent execution that satisfies or violates the property of interest. In concurrency theory, when equivalence is characterised by Mazurkiewicz traces, the corresponding question is called membership problem for trace language (MPTL). In 1989, A. Bertoni, G. Mauri, and N. Sabadini showed that MPTL can be solved in time O(n^\alpha) when the property is described using a regular language; n is the size of the execution (or string) and \alpha describes the width of the concurrency relation. We show that, in fact, this problem cannot be solved in better time by showing matching (conditional) lower bound of \Omega(n^\alpha) under the Strong Exponential Time Hypothesis. This result applies to even starfree regular languages. Motivated by practical applicability of runtime monitoring in a predictive setting, we propose a class of languages, called pattern languages, for which MPTL can be solved in constant space and linear time, in other words, using a DFA. Pattern languages essentially encode the existence of a subsequence: for every Pattern language L, there is finite string u such that every member string w in L has u as a subsequence. Pattern languages is a subclass of starfree regular languages and is closed under union, intersection, concatenation, and Kleene star. 
Simulating LogspaceRecursion
with Logarithmic Quantifier Depth
Simulating LogspaceRecursion with Logarithmic Quantifier DepthThe fixedpoint logic LREC= was developed by Grohe et al. (CSL 2012) in the quest for a logic to capture all problems decidable in logarithmic space.It extends FO+C, firstorder logic with counting, by an operator that formalises a limited form of recursion.We show that for every LREC=definable property on relational structures,there is a constant k such that the kvariable fragment of firstorder logic with counting quantifiers expresses the property via formulae of logarithmic quantifier depth.This yields that any pair of graphs separable by the property can be distinguished with the kdimensional WeisfeilerLeman algorithm in a logarithmic number of iterations.In particular, it implies that the algorithm identifies every interval graph and every chordal clawfree graph in logarithmically many iterations.Joint work with Steffen van Bergerem, Martin Grohe, and Sandra Kiefer 
Evaluating Restricted
FirstOrder Counting Properties on Nowhere Dense Classes and
Beyond
Evaluating Restricted FirstOrder Counting Properties on Nowhere Dense Classes and BeyondIt is known that firstorder logic with some counting extensions canbe efficiently evaluated on graph classes with bounded expansion, wheredepth$r$ minors have constant density. More precisely, the formulasare $\exists x_1 ... x_k \#y \phi(x_1,\ldots,x_k, y)>N$,where $\phi$ is an FOformula.If $\phi$ is quantifierfree, we canextend this result to \emph{nowhere dense} graph classes with analmost linear FPT run time. Lifting thisresult further to slightly more general graph classes, namely almost nowheredense classes, where the size of depth$r$ clique minors is subpolynomial,is impossible unless $\rm FPT=W[1]$. On the other hand, in almostnowhere dense classes we can approximate such counting formulas with asmall additive error.In particular, it follows that partial covering problems, such as partialdominating set, have fixed parameter algorithms on nowhere densegraph classes with almost linear running time. 
Wednesday
Wednesday 09h00  10h00, Keynote Speaker  HS 3  
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 goodforMDP automata, and for synthesis and games, it could be
goodforgames 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   Logic  HS 4  
Stopping Criteria for Value
Iteration on Stochastic~Games with Quantitative Objectives
Stopping Criteria for Value Iteration on Stochastic~Games with Quantitative ObjectivesThis extended abstract is based on joint work with Jan Kretinsky, accepted at LICS'23. An extended version is available at https://arxiv.org/abs/2304.09930.This is the favourite result of both authors of this submission.We plan a joint presentation, also to emphasize the game aspect of the content.A classic solution technique for Markov decision processes (MDP) and stochastic games (SG) is value iteration (VI).Due to its good practical performance, this approximative approach is typically preferred over exact techniques, even though no practical bounds on the imprecision of the result could be given until recently.As a consequence, even the most used model checkers could return arbitrarily wrong results.Over the past decade, different works derived stopping criteria, indicating when the precision reaches the desired level, for various settings, in particular MDP with reachability, total reward, and mean payoff, and SG with reachability.In this paper, we provide the first stopping criteria for VI on SG with total reward and mean payoff, yielding the first anytime algorithms in these settings.To this end, we provide the solution in two flavours:First through a reduction to the MDP case and second directly on SG.The former is simpler and automatically utilizes any advances on MDP.The latter allows for more local computations, heading towards better practical efficiency.Our solution unifies the previously mentioned approaches for MDP and SG and their underlying ideas.To achieve this, we isolate objectivespecific subroutines as well as identify objectiveindependent concepts.These structural concepts, while surprisingly simple, form the very essence of the unified solution. 
Counting Homomorphisms from
Hypergraphs of Bounded Generalised Hypertree Width: A Logical
Characterisation
Counting Homomorphisms from Hypergraphs of Bounded Generalised Hypertree Width: A Logical CharacterisationWe introduce the 2sorted counting logic GC^k that expresses properties of hypergraphs.This logic has available k "blue" variables to address edges, an unbounded number of "red" variables to address vertices of a hypergraph, and atomic formulas E(e,v) to express that vertex v is contained in edge e.We show that two hypergraphs H, H' satisfy the same sentences of the logic GC^k if, and only if, they are homomorphism indistinguishable over the class of hypergraphs of generalised hypertree width at most k.Here, H, H' are called homomorphism indistinguishable over a class C if for every hypergraph G in C the number of homomorphisms from G to H equals the number of homomorphisms from G to H'.This result can be viewed as a generalisation (from graphs to hypergraphs) of a result by Dvorak (2010) stating that any two (undirected, simple, finite) graphs H, H' are indistinguishable by the (k+1)variable counting logic C^{k+1} if, and only if, they are homomorphism indistinguishable on the class of graphs of tree width at most k.This is joint work with Nicole Schweikardt. 
Rabin Games and Colourful
Trees
Rabin Games and Colourful TreesWe provide an algorithm to solve Rabin and Streett games over $n$ vertices, $m$ edges, and $k$ colours, that runs in $\Tilde{O}\left(mn^3(k!)^{1+o(1)} \right)$ time and $O(nk\log k \log n)$ space, where $\Tilde{O}$ hides polylogarithmic factors.Our algorithm is an improvement by a super quadratic dependence on $k!$ from the currently best known run time of $O\left(mn^2(k!)^{2+o(1)}\right)$, obtained by converting a Rabin game into a parity game, while simultaneously improving its exponential space requirement.Our main technical ingredient is a characterization of progress measures for Rabin games using colourful trees and a combinatorial construction of succinctlyrepresented, universal colourful trees. Colourful universal trees are generalisations of universal trees used by Jurdzinski and Lazic (2017) to solve parity games, as well as of Rabin progress measures of Klarlund and Kozen (1991). Our algorithm for Rabin games performs lifting on progress measures defined on succinct, colourful, universal trees. 
Plan Logic
Plan LogicStrategy logics has two major flaws: the decision problems associated have a high complexity (model checking is non elementary and satisfiability is undecidable) and the strategy quantified might not be feasible. However, these drawbacks appear to be related as the fragment One Goal has a 2EXPTIME complexity and feasible strategies suffice to verify a formula. In this work, we propose an approach to define a logic suited to reason about feasible strategies by changing the domain of quantification. We replace strategies with plans (sequences of actions) and define a behavioral compositional semantics to ensure feasibility. This allows for the definition of an equivalent gametheoretic semantics and then, 2EXPTIME decision procedures. 
Weighted Timed Games:
decidability, stochastic strategies, and robustness
Weighted Timed Games: decidability, stochastic strategies, and robustnessWeighted timed games are twoplayer zerosum games played in a timed automaton equipped with integer weights. We consider optimal reachability objectives, in which one of the players, whom we call Min, wants to reach a target location while minimising the cumulated weight. While knowing if Min has a (deterministic) strategy to guarantee a value lower than a given threshold is known to be undecidable (with two or more clocks), several conditions, one ofthem being the divergence or oneclock WTGs with only nonnegative weights,have been given to recover decidability.We will briefly present our contributions in this domain. We first extend the decidable fragments by showing that for all oneclock WTGs (with arbitrary weights), the value function can be computed in exponential time (if weights are encoded in unary).Next, in such weighted timed games (like in untimed weighted games in thepresence of negative weights), Min may need finite memory to play (close to)optimally. This is thus tempting to try to emulate this finite memory withother strategic capabilities. In particular, we allow the players to usestochastic decisions, both in the choice of transitions and timing delays. Wegive, for the first time, a definition of the expected value in weighted timedgames, overcoming several theoretical challenges. We then show that, indivergent weighted timed games, the stochastic value is indeed equal to theclassical (deterministic) value, thus proving that Min can guarantee the samevalue while only using stochastic choices and no memory.Finally, even stochastic strategies may not be implementable since they can use infinite precision of clocks in the choice of the delay or in the knowledge about the configurations. Robustness is a known feature to encode the imprecision of delays in strategies: robustness allows Max player (the opponent of Min) to lightly perturb the delay chosen by Min. In the literature, two robust semantics exist: conservative semantic checks a guard after the perturbation, and excessive semantic checks a guard before. As for deterministic strategies, it was known that if Min has a (robust)strategy to guarantee a value lower than a given threshold is known to beundecidable. By adapting the process of value iteration introduced by Alur, wecompute the (robust) value in acyclic WTG under conservative and excessivesemantics.This is joint work with Benjamin Monmege and PierreAlain Reynier. 
Positive FirstOrder Logic on
Words and Graphs
Positive FirstOrder Logic on Words and GraphsThis work is about the logic FO +, a fragment of firstorder logic on finite words, where monadic predicates can only appear positively. We show that there is an FOdefinable language that is monotone in monadic predicates but not definable in FO +. This provides a simple proof that Lyndon’s preservation theorem fails on finite structures. We lift this example language to finite graphs, thereby providing a new result of independent interest for FOdefinable graph classes: negation might be needed even when the class is closed under addition of edges. We finally show that given a regular language, it is undecidable whether is is definable in FO+. 
Solving Timed Parity Games with
Surprise
Solving Timed Parity Games with SurpriseWe are interested in tools for synthesizing strategies in timed games with parity objective.From a theoretical point of view, we define and interpret these games as in the paper The Element of Surprise by Luca de Alpharo et al. (CONCUR~2003). This paper highlights several subtleties of timed games. They can be summarized as follows: representing a timed parity game by an interleaving of waiting steps (continuous transition) and actions (discrete transition) does not capture the strategies that require to be the fastest (as in a cowboy duel). Such strategies are called surprise strategies and do not have equivalent nosurprise strategies. Thus, taking surprise into account changes the game, i.e., the winner may be different depending on whether we consider surprise strategies. The paper studies reachability and safety objectives, but can also be used to adapt Zielonka's procedure to solve timed parity games.To our knowledge, the results of this paper have not been implemented in concrete tools. The paper does not give an explicit construction or other implementation methods, and UppAal, a wellknown timed game solver, considers a different semantics and focuses on reachability objectives.We therefore propose an explicit construction corresponding to the work of de Alpharo et al. and present its use in Zielonka's procedure for solving timed parity games.We believe that a tool for experimenting with new semisymbolic algorithms on timed games would benefit the community. TChecker is a project built in this sense and is in active development for at least eight years. However, it is a model checker: it does not yet support games. Therefore, together with Gilles Geeraerts, JeanFrançois Raskin, and Antoine Bedaton, we are working on integrating game support into TChecker and implementing our timed Zielonka's algorithm there as a proof of concept.Note: This work is being done in the context of my PhD. 
Semenov Arithmetic, Affine VASS,
and String Constraints
Semenov Arithmetic, Affine VASS, and String ConstraintsWe study extensions of Semenov arithmetic, the firstorder theory of the structure $\langle \mathbb{N},+,2^x\rangle$. It is wellknown that this theory becomes undecidable when extended with regular predicates over number strings, such as the Büchi $V_2$predicate. We therefore restrict ourselves to the existential theory of Semenov arithmetic and show that this theory is decidable in 2EXPSPACE when extended with arbitrary regular predicates over number strings. Our approach relies on a reduction to the emptiness problem for a restricted class of affine vector addition systems with states, which we show decidable in EXPSPACE. As an application of our result, we settle an open problem from the literature and show decidability of a class of string constraints involving length constraints. 
Finitememory strategies in
infinite concurrent twoplayer games
Finitememory strategies in infinite concurrent twoplayer gamesWe study infinite twoplayer win/lose games (A,B,W) where A and B are the action sets for the two players and W the winning set. At each round Player 1 and 2 concurrently choose one action in A and B respectively, generating an infinite sequence. Player 1 wins iff said sequence lies in W. Contrarily to the classical framework of games on graphs, this framework does not allow any observation on the current state of the game other than what the Player can compute onthefly from the stream of actions played.We study three different topological classes of winning sets (sets in the Hausdorff difference hierarchy, sets described using a combination of open sets and Büchi conditions, sets described using a combination of open sets and Parity conditions), and show that, under a well partial order condition on the winning sets induced by the histories, if Player 1 has a(n almostsurely) winning strategy, then she has a finitememory one. These classes include variations of typically wellstudied games such as Büchi/Parity games on finite graphs or energy games.Coauthors: Patricia Bouyer and Stéphane Le Roux. 
An AutomataTheoretic
Characterisation of Weighted FirstOrder Logic
An AutomataTheoretic Characterisation of Weighted FirstOrder LogicSince the 1970s with the work of McNaughton, Papert and Schützenberger, a regular language is known to be definable in the firstorder logic if and only if its syntactic monoid is aperiodic. This algebraic characterisation of a fundamental logical fragment has been extended in the quantitative case by Droste and Gastin, dealing with polynomially ambiguous weighted automata and a restricted fragment of weighted firstorder logic. In the quantitative setting, the full weighted firstorder logic (without the restriction that Droste and Gastin use, about the quantifier alternation) is more powerful than weighted automata, and extensions of the automata with twoway navigation, and pebbles or nested capabilities have been introduced to deal with it. In this work, we characterise the fragment of these extended weighted automata that recognise exactly the full weighted firstorder logic, under the condition that automata are polynomially ambiguous.This is joint work with Benjamin Monmege. 
ppLTLTT: Temporal testing for
purepast linear temporal logic formulas
ppLTLTT: Temporal testing for purepast linear temporal logic formulasWe introduce ppLTLTT, a commandline tool for translating purepast lineartemporal logic formulas into automata monitoring their truth values at everypoint in time. We show how ppLTLTT can be used to easily extend existing LTLbased tools, such as LTLtoautomata translators and reactive synthesis tools,to support a richer input language. Namely, with ppLTLTT, tools that acceptLTL input are also made to handle purepast LTL as atomic formulae. Whilethe addition of past operators does not increase the expressive power of LTL, itopens up the possibility of writing more intuitive and succinct specifications. Weillustrate this intended use of ppLTLTT for Slugs, Strix and Spot’s commandline tool LTL2TGBA by describing three corresponding wrapper tools pSlugs,pStrix and pLTL2TGBA, that all leverage ppLTLTT. All three wrapper tools aredesigned to seamlessly fit this paradigm, by staying as close to the respectivesyntax of each underlying tool as possible. 
Lunch
Wednesday 14h00  15h24, Contributed Talks



Automata and Transducers  HS 3   VASS, Skolem and Petri Net Problems  HS 4  
Monads, comonads, and
transducers
Monads, comonads, and transducersRegular languages are one of the most fundamental concepts in the area of formal language theory. In the recent decades, there has been an ongoing effort to extend the definition of regularity to structures more complex than finite words. Examples include infinite words, as well as finite and infinite trees. A recently developed line of research (see references at the end of the paper) is to find a common framework that would encapsulate (at least a significant portion of) these various generalizations. The approach proposed in the cited publications is to define regularity in terms of monads and their algebras – the framework proposes a definition of regularity for languages that are subsets of MΣ, where M is a monad, and Σ is a finite alphabet.In this presentation, I would like to discuss a possible extension of this framework for studying transducers. For this purpose, I am going to consider functors that simultaneously exhibit both the structure of a monad and of a comonad. It turns out that for such functors one can define a class of recognizable functions of type MΣ → MΓ, which (depending on the chosen M) can encompass deterministic Mealy machines (both lefttoright and righttoleft), lettertoletter rational functions, and some classes of transductions for structures other than words.In the talk, I plan to discuss what properties of M are required, to ensure that the class of its transductions is closed under compositions, and to discuss potential directions for future work.REFERENCES:Bojańczyk, Mikołaj. "Recognizable languages over monads." Developments in Language Theory: 19th International Conference, DLT 2015, Liverpool, UK, July 2730, 2015, Proceedings.. Cham: Springer International Publishing, 2015.Bojańczyk, Mikołaj. "Languages recognized by finite semigroups, and their generalizations to objects such as trees and graphs, with an emphasis on definability in monadic secondorder logic." arXiv eprints (2020): arXiv2008.Bojańczyk, Mikołaj, Bartek Klin, and Julian Salamanca. "Monadic monadic second order logic." arXiv preprint arXiv:2201.09969 (2022). 
Coverability in VASS Revisited:
Improving Rackoff’s Bounds to Obtain Conditional Optimaility
Coverability in VASS Revisited: Improving Rackoff’s Bounds to Obtain Conditional OptimailitySeminal results establish that the coverability problem for Vector Addition Systems with States (VASS) is in EXPSPACE (Rackoff, '78) and is EXPSPACEhard already under unary encodings (Lipton, '76).More precisely, Rosier and Yen later utilise Rackoff's bounding technique to show that if coverability holds then there is a run of length at most n^(2^(O(d*log(d))), where d is the dimension and n is the size of the given unary VASS.Earlier, Lipton showed that there exist instances of coverability in ddimensional unary VASS that are only witnessed by runs of doubleexponential length that is at least n^(2^(Omega(d))).In this presentation, I will outline how to carefully strengthen Rackoff's approach to improve the upper bound to show that if coverability holds then there exists a run of length at most n^(2^(O(d))).Moreover, we therefore obtain an optimal 2^(O(d))*log(n)space algorithm for coverability.This closes a fortyoneyearold gap that was stated as an open problem by Mayr and Meyer.Furthermore, we obtain a deterministic n^(2^(O(d)))time algorithm for coverability in unary dVASS.We show that this is optimal under the Exponential Time Hypothesis, in particular by leveraging the time required to detect a clique in a graph.I also plan to present the approach and techniques used in our reduction from finding cliques in graphs to coverability in unary VASS.Ultimately, this yields a conditional matching lower bound that coverability in unary dVASS requires n^(2^(Omega(d)))time.This presentation concerns ongoing joint work with Marvin Künnemann, Filip Mazowiecki, Lia Schütze, and Karol Węgrzycki. Please see the attached extended abstract for greater overview of our recent work. 
Implicit automata in typed
λcalculi (I, II and III)
Implicit automata in typed λcalculi (I, II and III)In the past few years, Cécilia Pradic and I have been pursuing a research programme aimed at uncovering connections of the form: "the languages/functions recognized by some flavor A of automata are exactly those definable in some typed λcalculus P, using a certain input/output convention". λcalculi are minimalistic functional programming languages, and type systems have been used to achieve interesting restrictions on their expressive power in a field called implicit computational complexity – hence the title. The I/O conventions that we use are based on Church encodings, whose connections with automata theory have been leveraged in higherorder model checking (HOMC).Our main inspiration is a result of Hillebrand and Kanellakis (1996): A = regular languages, P = simply typed λcalculus. We have managed to characterize starfree languages, regular tree functions (in a similar fashion to Gallot, Lemay & Salvati 2020) and comparisonfree polyregular functions (a class whose introduction was motivated by our work on λcalculi!) using type systems based on linear logic (a programming language counterpart of various "copyless" or "single use" restrictions in automata theory). These developments, and the semantic/categorytheoretic tools that they involve, are recapitulated in the longer abstract https://csweb.swan.ac.uk/~cpradic/smpabstract.pdfMore recently, I have devised a transducer model, based on the collapsible pushdown automata used in HOMC, that captures the treetotree functions computable by simply typed λterms, thus answering a question going back at least to the 1980s. This work can also be seen as a revival of Engelfriet and Vogler's investigations into "high level tree transducers", also in the 1980s. 
Robust Positivity Problems for
loworder Linear Recurrence Sequences
Robust Positivity Problems for loworder Linear Recurrence SequencesLinear Recurrence Sequences (LRS) are a fundamental mathematical primitive for a plethora of applications such as model checking, probabilistic systems, computational biology, and economics. Positivity (are all terms of the given LRS at least 0?) and Ultimate Positivity (are all but finitely many terms of the given LRS at least 0?) are important open numbertheoretic decision problems. Recently, the robust versions of these problems, that ask whether the LRS is (Ultimately) Positive despite small perturbations to its initialisation, have gained attention as a means to model the imprecision that arises in practical settings. In this paper, we consider Robust Positivity and Ultimate Positivity problems where the neighbourhood of the initialisation, specified in a natural and general format, is also part of the input. We contribute by proving sharp decidability results: decision procedures at orders our techniques can't handle would entail significant numbertheoretic breakthroughs. 
Unboundedness problems for
machines with reversalbounded counters
Unboundedness problems for machines with reversalbounded countersAuthors: Pascal Baumann, Flavio D’Alessandro, Moses Ganardi, Oscar Ibarra, Ian McQuillan, Lia Schütze, and Georg ZetzscheWe consider a general class of decision problems concerning formal languages, called “(onedimensional) unboundedness predicates”, for automata that feature reversalbounded counters (RBCA). We show that each problem in this class reduces—nondeterministically in polynomial time—to the same problem for just finite automata. We also show an analogous reduction for automata that have access to both a pushdown stack and reversalbounded counters (PRBCA).This allows us to answer several open questions: For example, we show that it is coNPcomplete to decide whether a given (P)RBCA language L is bounded, meaning whether there exist words w_1, ... , w_n with L ⊆ w_1^* ··· w_n^*. For PRBCA, even decidability was open. Our methods also show that there is no language of a (P)RBCA of intermediate growth. This means, the number of words of each length grows either polynomially or exponentially. Part of our proof is likely of independent interest: We show that one can translate an RBCA into a machine with Zcounters in logarithmic space, while preserving the accepted language. 
Reachability in Continuous
Pushdown VASS
Reachability in Continuous Pushdown VASSPushdown Vector Addition Systems with States (PVASS) consist of finitely many control states, a pushdown stack, and a set of counters that can be incremented and decremented, but not tested for zero. Whether the reachability problem is decidable for PVASS is a longstanding open problem.We consider continuous PVASS, which are PVASS with a continuous semantics.This means, the counter values are nonnegative rational numbers and whenever a vector is added to the current counter values, this vector is first scaled with an arbitrarily chosen fraction between zero and one.We show that reachability in continuous PVASS is NEXPTIMEcomplete.Our result is unusually robust: Reachability can be decided in NEXPTIME even if all numbers are specified in binary. On the other hand, NEXPTIMEhardness already holds for coverability, in fixed dimension, for bounded stack, and even if all numbers are specified in unary.This is joint work with Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche. 
Refinement problems for
recognizable relations
Refinement problems for recognizable relationsGiven a relation on the states of a finite deterministic automaton, is it possible to define a congruence of finite index, refining this relation and verifying a given property ?This general problem came up while searching for an algebraic solution to the register minimization problem for streaming string transducers realizing rational functions between words. It is also linked to the problem of separation of regular languages.In this talk, I will present different equivalent forms of the refinement problem and show its connection with other well known problems. I will also present an interesting tool, which is part of an ongoing work on the subject, that can describe the possible solutions of this problem. 
Geometry of Reachability Sets of
Vector Addition Systems
Geometry of Reachability Sets of Vector Addition SystemsCoauthors: Mikhail Raskin and Javier EsparzaVector Addition Systems (VAS), aka Petri nets, are a popular model of concurrency. The reachability set of a VAS is the set of configurations reachable from the initial configuration. Leroux has studied the geometric properties of VAS reachability sets, and used them to derive decision procedures for important analysis problems. In this talk we continue the geometric study of reachability sets. We show that every reachability set admits a finite decomposition into disjoint almosthybridlinear sets enjoying nice geometric properties. Further, we prove that the decomposition of the reachability set of a given VAS is effectively computable. As a corollary, we derive a simple algorithm for deciding semilinearity of VAS reachability sets, the first one since Hauschildt's 1990 algorithm. As a second corollary, we prove that the complement of a reachability set always contains an infinite linear set. 
DimensionMinimality and
Primality of Counter Nets
DimensionMinimality and Primality of Counter NetsA $k$Counter Net ($k$CN) is a finitestate automaton equipped with $k$ integer counters that are not allowed to become negative, but do not have explicit zero tests. This languagerecognition model can be thought of as labelled vector addition systems with states, some of which are accepting.Certain decision problems for $k$CNs become easier, or indeed decidable, when the dimension $k$ is small.Yet, little is known about the effect that the dimension $k$ has on the class of languages recognised by $k$CNs. Specifically, it would be useful if we could simplify algorithmic reasoning by reducing the dimension of a given CN.To this end, we introduce the notion of dimensionprimality for $k$CN, whereby a $k$CN is prime if it recognises a language that that cannot be decomposed into a finite intersection of languages recognised by $d$CNs, for some $d<k$. We show that primality is undecidable.We also study two related notions: dimensionminimality (where we seek a single languageequivalent $d$CN of lower dimension) and language regularity.Additionally, we explore the tradeoffs in expressiveness between dimension and nondeterminism for CN.This presentation is based on submitted work with Shaull Almagor, Guy Avni and Henry SinclairBanks. 
History Deterministic Vector
Addition Systems
History Deterministic Vector Addition SystemsIn this talk, we consider Historydeterminism, a restricted form of nondeterminism, for Vector Addition Systems with States (VASS) when used as acceptors to recognise languages of finite words, both with coverability and reachability acceptance.Historydeterminism requires that the nondeterministic choices can be resolved onthefly; based on the past andwithout jeopardising acceptance of any possible continuation of the input word.Our results show that the historydeterministic (HD) VASS sit strictly between deterministic and nondeterministic VASS.We compare the relative expressiveness of HD systems, and closureproperties of the induced language classes, with coverability and reachability semantics, with or without $\epsilon$ labelled transitions.With two or more counters HDVASS are essentially able to approximate 2counter Minsky machines, leading to several undecidability results. It is undecidable whether an VASS is historydeterministic, or if a language equivalent historydeterministic VASS exists.Checking language inclusion between historydeterministic $2$VASS is also undecidable.This talk is based on joint work with Patrick Totzke and David Purser. 
One deterministiccounter
automata
One deterministiccounter automataWe introduce one deterministiccounter automata (ODCA), which are onecounterautomata where all runs labelled by a given word have the same counter effect,a property we call counterdeterminacy. ODCAs are an extension of visiblyonecounter automata  onecounter automata (OCA), where the input alphabetdetermines the actions on the counter. They are a natural way to introducenondeterminism/weights to OCAs while maintaining the decidability of crucialproblems that are undecidable on general OCAs. For example, the equivalenceproblem is decidable for deterministic OCAs, whereas it is undecidable fornondeterministic OCAs. We consider both nondeterministic and weighted ODCAs.Our work shows that the equivalence problem is decidable in polynomial timefor weighted ODCAs over a field and polynomial space for nondeterministicODCAs. As a corollary, we get that the regularity problem, i.e., the problem ofchecking whether an input weighted ODCA is equivalent to some weightedautomaton, is also in polynomial time. Furthermore, we show that the coveringand coverable equivalence problems for uninitialised weighted ODCAs aredecidable in polynomial time. We also introduce a few reachability problemsthat are of independent interest and show that they are in P. Thesereachability problems later help in solving the equivalence problem.https://arxiv.org/abs/2301.13456 
Skolem and Positivity
Completeness of Ergodic Markov Chains
Skolem and Positivity Completeness of Ergodic Markov ChainsWe consider the following decision problems: given a finite, rational Markov chain, source and target states, and a rational threshold, does there exist an n such that the probability of reaching the target from the source in n steps is equal to the threshold (resp. crosses the threshold)? These problems are known to be equivalent to the Skolem (resp. Positivity) problems for Linear Recurrence Sequences (LRS). These are numbertheoretic problems whose decidability has been open for decades. We present a short, selfcontained, and elementary reduction from LRS to Markov Chains that improves the state of the art as follows: (a) We reduce to ergodic Markov Chains, a class that is widely used in Model Checking. (b) We reduce LRS to Markov Chains of significantly lower order than before. We thus get sharper hardness results for a more ubiquitous class of Markov Chains. Immediate applications include problems in modeling biological systems, and regular automatabased counting problems. 
Closeness of Finite State
Transducers
Closeness of Finite State TransducersFor a metric over words, we define the distance between two transducers with identical domain as the supremum of the distances of their respective outputs over all inputs. We argue that this is a useful generalisation for comparing transducers that goes beyond the equivalence problem. Two transducers are said to be \emph{close} (\textit{resp.} $k$close) with respect to a metric if their distance is bounded (\textit{resp.} at most $k$). Computing distance between transducers is equivalent to deciding closeness and $k$closeness, over integervalued metrics. We show that closeness and $k$closeness are decidable for rational transducers w.r.t.~common edit distances. Hence the distances with respect to them are also computable. The proof relies on a generalisation of theorems of LyndonSch\"utzenberger from combinatorics of words. Stated concisely, the theorem reads that a sumfree (generated by an regular expression free of unions) set of pairs is conjugate if and only if there is a word witnessing the conjugacy of all the pairs.An interesting corollary of our results is that it can decided if the outputs of two sequential or rational transducers are conjugates for all inputs. 
Reachability in symmetric Petri
nets with data
Reachability in symmetric Petri nets with dataIn Petri nets with data, tokens carry values that can be tested during the execution of transitions. In the case of equality data we can check if two tokens carry the same data value, in the case of ordered data we can check if the data value in a token is greater/less than the data value in some other token. The decidability status of the reachability problem in Petri nets with equality data is still open, while the same problem for Petri nets with ordered data is known to be undecidable.We prove the decidability of the reachability problem, both for equality and ordered data, in the subclass of symmetric Petri nets, where each transition has its inverse. Towards this aim, we lift the classical theory of Groebner bases to ideals of polynomials over an orbitfinite set of variables.This is a work in progress, conducted jointly with Piotr Hofman and Sławomir Lasota. 
Wellbehaving concurrent games:
from local to global properties
Wellbehaving concurrent games: from local to global propertiesIn general, finite concurrent twoplayer games behave poorly, especially when compared totheir turnbased counterparts. For instance, in deterministic turnbased games — with a Borelobjective — either of the players has a winning strategy, which fails in concurrent reachability games even with a single nontrivial concurrent interactions of the players. Furthermore,considering stochastic games, in finite turnbased parity games, positional optimal strategiesalways exist for both players, whereas optimal strategies need not exist in concurrent games,even for a reachability objective. With more involved objectives, it actually gets even worse: forinstance, playing subgame optimally may require infinite memory in concurrent parity games.We present a twostep approach to characterize a structural condition on the interactionsappearing in a concurrent game that ensures that such games behave well — for a specificdesirable property — while still being more general than turnbased games. The two stepsare as follows, given a desirable property φ that we want to hold in concurrent games — forinstance, the existence of optimal strategies in reachability games. First, characterize the safelocal interactions that behave well individually — that is such that the property φ is ensured inall games where they are the only nontrivial local interaction. Second, in games where all localinteractions are safe, study if the property φ also holds. If so, we have proved the following,w.r.t. the property φ:• Unsafe local interactions do not behave well, even individually;• Safe local interactions behave well, even collectively.We have used this approach in several papers [1, 2, 3], which are joint works with PatriciaBouyer and Stéphane Le Roux. 
Coffee Break
Wednesday 16h00  17h00, Highlights Business Meeing  TBA
"Highlights Business Meeting"
Thursday
Thursday 09h00  10h00, Keynote Speaker  HS 3  
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, attackdefense trees mean to
graphically represent how nonatomic 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 starfree languages.
Coffee Break
Thursday 10h30  11h42, Contributed Talks



Synthesis  HS 3   Algorithms & Complexity  HS 4  
Boolean Functional Synthesis:
From One to All Skolem Functions
Boolean Functional Synthesis: From One to All Skolem FunctionsGiven a specification as a Boolean relation between inputs and outputs, Boolean functional synthesis generates a function, called a Skolem function, for each output in terms of the inputs such that the specification is satisfied. There is a large body of recent work which uses different techniques to solve this problem, i.e., synthesize one Skolem function from a given relational specification. But in general, there may be many possibilities for Skolem functions satisfying the same specification, and further, the criteria to pick one or the other may vary from specification to specification.In this work, we develop a new technique to represent the space of all Skolem functions in a criteriaagnostic form that makes it possible to subsequently extract Skolem functions for different criteria. Our approach is based on a novel counterexample guided strategy for existentially quantifying a subset of variables from a specification in negation normal form. We implement this technique and compare our performance with that of other knowledge compilation approaches for Boolean functional synthesis, and show promising results. Surprisingly, there are several benchmarks for which we can synthesize such a "useful" representation of the entire space of Skolem functions, while other tools fail to synthesize even a single Skolem function. 
Dynamic constanttime parallel
graph algorithms with sublinear work
Dynamic constanttime parallel graph algorithms with sublinear workThe talk proposes dynamic parallel algorithms for connectivity and bipartiteness of undirected graphs that require constanttime and n^{1/2} times polylog(n) work on the (arbitrary) CRCW PRAM model. The work of these algorithms almost matches the work of the O(log n) time algorithm for Connectivity by Kopelowitz et al. (2018) on the EREW PRAM model and the time of the sequential algorithm for bipartiteness by Eppstein et al. (1997). In particular, it is shown that the sparsification technique, which has been used in both mentioned papers, can in principle also be used for constant time algorithms in the CRCW PRAM model, despite the logarithmic depth of sparsification trees. This talk presents yet unpublished joined work with Thomas Schwentick. 
Fully Generalized Reactivity (1)
Synthesis
Fully Generalized Reactivity (1) SynthesisRecently Ehlers&Schewe proposed a canonical minimal representation foromegaregular languages [1]. The representation consists of a canonical chainof coBüchi languages (COCOA): A1 ⊃ A2 ⊃ ... ⊃ An, where each Ai is expressibleby a goodforgames coBüchi automaton, canonical and minimal by the work ofAbu Radi and Kupferman [2]. This work presents a first application of the newrepresentation, to the problem of reactive synthesis. In reactive synthesis wewant to automatically construct a transducer from a specification in e.g.linear temporal logic. The flow of our construction is: translate a given LTLinto a parity automaton and into COCOA using [1,2], then we construct amucalculus fixpoint formula which is evaluated on a game graph of thesynthesis problem. The resulting procedure generalizes the widely knownGeneralized Reactivity (1) synthesis approach to full LTL while inheriting itsefficiency advantages on the original specification class.This is a joint work with Rüdiger Ehlers (main contributor). [1]: Natural Colors of Infinite Words, by Rüdiger Ehlers and Sven Schewe[2]: Minimization and Canonization of GFG TransitionBased Automata, by Bader {Abu Radi} and Orna Kupferman 
On the work of dynamic
constanttime parallel algorithms for regular tree languages and
contextfree languages
On the work of dynamic constanttime parallel algorithms for regular tree languages and contextfree languagesPrevious work on Dynamic Complexity has established that there exist dynamic constanttime parallel algorithms for regular tree languages and contextfree languages under label or symbol changes. However, these algorithms were not developed with the goal to minimise work (or equivantly, the number of processors). In fact, their inspection yields the work bounds O(n^2) and O(n^7) per change operation, respectively.In this talk, dynamic algorithms for regular tree languages are proposed that generalise the previous algorithms in that they allow unbounded node rank and leaf insertions, while improving the work bound from O(n^2) to O(n^ϵ), for arbitrary ϵ > 0.For contextfree languages algorithms with better work bounds (compared with O(n^7)) for restricted classes are proposed: for every ϵ > 0 there are such algorithms for deterministic contextfree languages with work bound O(n^(3+ϵ)) and for visibly pushdown languages with work bound O(n^(2+ϵ)).This talk is based on joint work with Jonas Schmidt and Thomas Schwentick. 
Seamless Reactivity of Hybrid
Control via Augmented Games
Seamless Reactivity of Hybrid Control via Augmented GamesThe problem of synthesizing controllers with respect to temporal logic specifications has received considerable attention in the last decade, especially in the context of cyberphysical systems (CPS) design. Such problems occur for example in the control of autonomous robots deployed in warehouses, for underwater inspection or in rescue and evacuation scenarios. In order to solve such problems, techniques from the formal methods and the control community are combined. In particular, twoplayer games over finite graphs are used on the higher layer to reason about the temporal logic specification, while classical feedback controller synthesis is used in the lower layer to actuate the underlying dynamical system. Unfortunately, in existing approaches, the integration of highlevel game solving algorithms with feedbackcontroller synthesis has to substantially compromise the unique features of both methodologies in order to achieve compatibility. In order to close this gap, this talk shows a novel approach to the higherlayer game solving problem targeted towards controller synthesis for CPS. The key contribution of our work is twofold. First, instead of synthesizing single strategies, we compute \emph{strategy templates} which allow for a certified translation into lowlevel feedback controller synthesis problems. Second, we allow for \emph{progress group augmentations} of the games we solve which allow us to capture rich liveness properties implemented by the lower control layer that reduce the conservativeness of the higher layer synthesis game. We showcase our work using an example from robot motion planning.This is joint work with Lucas Neves Egidio, Matteo Della Rossa, AnneKathrin Schmuck, and Raphaël Jungers. 
Approximate Model Counting: Is
SAT Oracle More Powerful than NP Oracle?
Approximate Model Counting: Is SAT Oracle More Powerful than NP Oracle?Given a Boolean formula $\phi$ over $n$ variables, the problem of model counting is to compute the number of solutions of $\phi$. Model counting is a fundamental problem in computer science with wideranging applications in domains such as quantified information leakage, probabilistic reasoning, network reliability, neural network verification, and more. Owing to the \#Phardness of the problems, Stockmeyer initiated the study of the complexity of approximate counting. Stockmeyer showed that $\log n$ calls to NP oracle are necessary and sufficient to achieve $(\epsilon,\delta)$ guarantees. The hashingbased framework proposed by Stockmeyer has been very influential in designing practical counters over the past decade, wherein the SAT solver substitutes the NP oracle calls in practice. It is well known that NP oracle does not fully capture the behavior of SAT solvers, as SAT solvers are also designed to provide satisfying assignments when a formula is satisfiable, without additional overhead. Accordingly, the notion of SAT oracle has been proposed to capture the behavior of SAT solver wherein given a Boolean formula, an SAT oracle returns a satisfying assignment if the formula is satisfiable or returns unsatisfiable otherwise. Since the practical stateoftheart approximate counting techniques use SAT solvers, a natural question is whether an SAT oracle is more powerful than an NP oracle in the context of approximate model counting. The primary contribution of this work is to study the relative power of the NP oracle and SAT oracle in the context of approximate model counting. The previous techniques proposed in the context of an NP oracle are weak to provide strong bounds in the context of SAT oracle since, in contrast to an NP oracle that provides only one bit of information, an SAT oracle can provide $n$ bits of information. We, therefore, develop a new methodology to achieve the main result: an SAT oracle is no more powerful than an NP oracle in the context of approximate model counting. 
Synthesis of Infinite State
Systems
Synthesis of Infinite State SystemsThe classical Church synthesis problem, solved by Buchi and Landweber treats the synthesis of finite state systems. The synthesis of infinite state systems, on the other hand, has only been investigated few times since then, with no complete or systematic solution.We present a systematic study of the synthesis of infinite state systems. The main step involves the synthesis of MSOdefinable parity games, which is, finding MSOdefinable uniform memoryless winning strategies for these games. 
Probabilistic Query Evaluation:
The Combined FPRAS Landscape
Probabilistic Query Evaluation: The Combined FPRAS LandscapeConsider the problem of computing the probability of a query over a tupleindependent probabilistic database, known as the probabilistic query evaluation (PQE) problem. The problem is wellknown to be #Phard in data complexity for conjunctive queries in general, as well as for several subclasses of conjunctive queries (Dalvi and Suciu 2004). Existing approximation approaches for dealing with hard queries have centred on computing the lineage of the query over the database, which can be intractable for all but the smallest of queries due to the exponential dependence of the lineage size on the query length.In this talk, I will show how to construct a fully polynomialtime randomized approximation scheme (FPRAS) for the PQE problem for any class of selfjoinfree conjunctive queries of bounded hypertree width, that runs in time polynomial in *both* the query length and database size. An interesting consequence of this result is the existence of classes of queries that are #Phard in data complexity to evaluate exactly, yet easy to approximate both in terms of query length and database size. The result builds on a recent breakthrough in approximating the number of fixedsize trees accepted by a nondeterministic finite tree automaton (Arenas, Croquevielle, Jayaram and Riveros 2021).Joint work with Kuldeep S. Meel. Based on a paper accepted to PODS 2023. 
Games for Efficient Supervisor
Synthesis
Games for Efficient Supervisor SynthesisIn recent years, there was an increasing interest in the connections between supervisory control theory and reactive synthesis.As the two fields use similar techniques there is great hope that technologies from one field could be used in the other.In this spirit, we provide an alternative reduction from the supervisor synthesis problem to solving B\"uchi games via games with a nonblocking objective. Our reduction is more compact and uniform than previous reductions.As a consequence, it gives an asymptotically better upper bound on the time complexity of the supervisory control synthesis problem. Our reduction also breaks a widely held belief about the impossibility of reduction of supervisory control synthesis problem to a game with linear winning condition. 
Complexity of deciding equality
of power series from combinatorial enumeration
Complexity of deciding equality of power series from combinatorial enumerationA power series is constructible differentially finite (CDF) if it satisfies a system of polynomial differential equations [Bergeron & Reutenauer 1990, Bergeron & Sattler 1995]. CDF series generalise algebraic power se ries and find a natural application as exponential generating functions in combinatorial enumeration (e.g., combinatorial species by Andre Joyal). For instance, the exponential generating functions of Bell numbers B(n), of rooted Cayley trees (sequence nn−1), of seriesparallel graphs, and of languages of unordered trees defined by Parikh tree automata are CDF. Bergeron & Reutenauer observed that the equality problem for univari ate CDF series is decidable, without providing a complexity bound. We show that zeroness of univariate CDF series can be solved in elementary (2EXPTIME) complexity. The proof relies on a technical lemma from [Novikov & Yakovenko 1999] showing that chains of polynomial ideals generated by iterated Lie derivatives have at most doubly exponential length. We then extend this result in two directions. First, we show that the 2EXPTIME complexity is retained for multivariate CDF. Second, we show that the problem is in PTIME for CDF satisfying a system of linear differential equations with constant coefficients. Along the way, we show that multivariate CDF is a very robust class with many pleasant closure properties. 
Strategy Synthesis in Markov
Decision Processes Under Limited Sampling Access
Strategy Synthesis in Markov Decision Processes Under Limited Sampling AccessA central task in control theory, artificial intelligence, andformal methods is to synthesize rewardmaximizing strategies for agentsthat operate in partially unknown environments. In environments modelled by graybox Markov decision processes (MDPs), the impact of theagents’ actions are known in terms of successor states but not the stochasticsinvolved.In this talk I will present a new strategy synthesis algorithm forgraybox MDPs, via reinforcement learning that utilizes interval MDPs asinternal model. To compete with limited sampling access in reinforcementlearning, the algorithm incorporates two novel concepts, focusingon rapid and successful learning rather than on optimality:lower confidence bound exploration reinforces variantsof already learned practical strategies and action scoping reduces thelearning action space to promising actions. In particular, I will focus on how these methods can be applied inthe context of formal verification of queries asking for theexistence of a strategy under certain constraints.I will illustrate benefits of ouralgorithms by means of a prototypical implementation applied on examplesfrom the AI and formal methods communities and discuss possible extensions.This is joint work with Christel Baier, Clemens Dubslaff, and Stefan J. Kiebel.The full paper has been accepted for publication at the NASA Formal Methods conference 2023.An extended preprint is avaiable. 
Enumerating Partial Answers in
Description Logics with Functional Roles
Enumerating Partial Answers in Description Logics with Functional RolesIn ontologymediated querying, a query is combined with an ontology to enrich querying with domain knowledge and to facilitate access to incomplete and heterogeneous data.Most of the existing studies have concentrated on the basic problem of singletesting which means to decide, given an ontologymediated query (OMQ) Q=(O,q), a database D, and a candidate answer c, whether c is indeed an answer to Q on D. From the viewpoint of many practical applications, however, the assumption that a candidate answer is provided is hardly realistic and it seems much more relevant to efficiently enumerate all answers to Q on D.In this talk, I will discuss sufficient and necessary conditions to achieve enumeration algorithms that have a linear time preprocessing phase (in the size of the database) and constant delay between answers, with no answer repetition. I will focus on OMQs Q=(O,q) where the query q is a conjunctive query and the ontology O is expressed in description logic ELIHF. This logic allows for complex concept definitions and functionality assertions.The talk is based on joint work with Carsten Lutz, presented during the ThirtySeventh AAAI Conference on Artificial Intelligence (AAAI'23). 
Distinct Elements in Streams:
An Algorithm for the (Text) Book
Distinct Elements in Streams: An Algorithm for the (Text) BookGiven a data stream of m elements, the Distinct Elements problem is to estimate the number of distinct elements in the stream. Distinct Elements has been a subject of theoretical and empirical investigations over the past four decades resulting in spaceoptimal algorithms for it. However, all the current stateoftheart algorithms are often difficult to analyze or impractical. I will present a simple, intuitive, samplingbased spaceefficient algorithm whose description and the proof are accessible to undergraduates with a knowledge of basic probability theory. In addition to the simplicity, the approach has significant theoretical and practical implications: our approach allowed us to resolve the open problem of (Discrete) Klee's Measure Problem in the streaming setting and build a stateoftheart DNF counter in practice. Relevant publication: https://arxiv.org/abs/2301.10191 
Lunch
Thursday 14h00  15h24, Contributed Talks



Formal Methods and Learning  HS 3   Automata, Algebra & Languages  HS 4  
About Limits In Formal
Verification of Graph Neural Networks
About Limits In Formal Verification of Graph Neural NetworksDeep learning methods, especially their most prominent representative (deep) neural networks, have proved to be very successful in a broad range of applications, delivering impressive results. Unsurprisingly, deep learning methods are also used in safetycritical applications like early disease detection or driving assistants, which naturally leads to the need for safety certificates. Currently very popular are so called Graph Neural Networks (GNN), a neural network model for computing functions over graphs. While there is ongoing work on (formal) verification of GNN there is no work so far giving reliable decidability or complexity bounds of corresponding problems Thus, there are currently no fundamental results that frame and guide the development of GNN verification algorithms. We present our contributions to this topic, establishing first (un)decidability results regarding the verification problem of common safety properties of so called Message Passing Neural Networks (MPNN), one of the most popular GNN variants. Additionally, we discuss strong conjectures, leading to lower and upper complexity bounds for the same problems, and we rank the implications of our results for the development of corresponding sound and complete verification algorithms. 
Algebras for Regular
Relations
Algebras for Regular RelationsWe introduce the notion of synchronous algebra, which is a type of algebras tailored to recognize regular relations: any relation admits a syntactic synchronous algebra, and this relation is regular (i.e. accepted by a synchronous automaton) if and only if this algebra is finite.We show that these algebras naturally arises using two different constructions:1. using Bojańczyk's theory of recognizability via monads over typed sets,2. by encoding synchronous words as finite words over an extended alphabet: synchronous algebras arise as the class of monoids that are quotiented by the syntactic monoid of "wellformed words", namely the language of all words corresponding to some encoding.Lastly, we show why this notion of algebra is inherently more suitable to studying properties of regular relations compared to monoids or semigroups. 
On Learning MSOFormulas
On Learning MSOFormulasAbstractConsider the following supervised classification problem: given a backgroundstructure with a set of instances X and a training set S ⊆ X × {+, −}, we aimto find a hypothesis h : X → {+, −} from some hypothesis class H, that mapsevery instance to a class. Such a hypothesis is consistent with the training example when h(x) = c for (x, c) ∈ S. We consider a setup where the backgroundstructure is a relational structure A and an instance v̄ ∈ A^d is a dtuple ofelements from the universe. We aim to learn a monadic secondorder formulaφ(x̄) with x̄ = d free instance variables, that is consistent with the trainingset. This means, that for every positive example in the training set (v̄, +) ∈ Swe have A = φ(v̄) and for (v̄, −) ∈ S we have A ⊭ φ(v̄). We call the problemMSOLearn and for d = 1 we speak of unaryMSOLearn.We analyze the problem in the context of parameterized complexity and show that it is fixedparameter tractable for d=1 on structures of bounded treewidth and graphs of bounded cliquewidth. Furthermore, we give bounds for d>1 in the PAC learning framework. 
Cascades of condensations
Cascades of condensationsThis is joint worked with Adsul Bharat, thanks to the Highlights Extended Stay Support Scheme 2023.We show that all regular languages can be described by applying a sequence of simple socalled ``condensation maps.''A condensation map consists, given an input word, in selecting maximal factors that belong to a condensation language, and evaluate all of them in parallel. A condensation language is a language for which it is guaranteed that in the above definition maximal factors cannot overlap: it is assumed to be infix closed and to have the property that if $ua$ and $av$ are in the language, then $uav$ also is. The simple condensation maps correspond to very simple cases.This result captures classical proof techniques in the study of regular languages and exhibit similarities with the KrohnRhodes' theorem and the theorem of factorisation forest of Simon. 
FormallySharp DAgger for MCTS:
LowerLatency Monte Carlo Tree Search using Data Aggregation with Formal
Methods
FormallySharp DAgger for MCTS: LowerLatency Monte Carlo Tree Search using Data Aggregation with Formal MethodsWe discuss how to efficiently combine formal methods, Monte Carlo Tree Search (MCTS), and deep learning in order to produce highquality receding horizon strategies in large Markov Decision processes (MDPs). In particular, we use modelchecking techniques to guide the MCTS algorithm in order to generate offline samples of highquality decisions on a representative set of states of the MDP. Those samples can then be used to train a neural network that imitates the strategy used to generate them. This neural network can either be used as a guide on a lowerlatency MCTS online search, or alternatively be used as a fullfledged strategy when minimal latency is required. We use statistical model checking to detect when additional samples are needed and to focus those additional samples on configurations where the learnt neural network strategy differs from the (computationallyexpensive) offline strategy. We illustrate the use of our method on MDPs that model the Frozen Lake and PacMan environments  two popular benchmarks to evaluate reinforcementlearning algorithms.The talk is based on the sametitled paper accepted at AAMAS,2023. This is a joint work with Damien BusattoGaston, JeanFrançois Raskin and Guillermo A. Pérez. 
Enumerating Regular Languages
with Bounded Delay
Enumerating Regular Languages with Bounded DelayWe study the task, for a given language L, of enumerating the (generally infinite) sequence of its words,without repetitions, while bounding the delay between two consecutive words. To allow for delay boundsthat do not depend on the current word length, we assume a model where we produce each word by editingthe preceding word with a small edit script, rather than writing out the word from scratch. In particular,this witnesses that the language is orderable, i.e., we can write its words as an infinite sequence such that theLevenshtein edit distance between any two consecutive words is bounded by a value that depends only on thelanguage. For instance, (a + b)∗ is orderable (with a variant of the Gray code), but a∗ + b∗ is not.We characterize which regular languages are enumerable in this sense, and show that this can be decided inPTIME in an input deterministic finite automaton (DFA) for the language. In fact, we show that, given aDFA A, we can compute in PTIME automata A1 , . . . , At such that L(A) is partitioned as L(A1 ) ⊔ . . . ⊔ L(At )and every L(Ai ) is orderable in this sense. Further, we show that the value of t obtained is optimal, i.e., wecannot partition L(A) into less than t orderable languages.In the case where L(A) is orderable (i.e., t = 1), we show that the ordering can be produced by a boundeddelayalgorithm: specifically, the algorithm runs in a suitable pointer machine model, and produces a sequence ofboundedlength edit scripts to visit the words of L(A) without repetitions, with bounded delay – exponentialin A – between each script. In fact, we show that we can achieve this while only allowing the edit operationspush and pop at the beginning and end of the word, which implies that the word can in fact be maintained ina doubleended queue.By contrast, when fixing the distance bound d between consecutive words and the number of classes of thepartition, it is NPhard in the input DFA A to decide if L(A) is orderable in this sense, already for finitelanguages.Last, we study the model where pushpop edits are only allowed at the end of the word, corresponding to acase where the word is maintained on a stack. We show that these operations are strictly weaker and that theslender languages are precisely those that can be partitioned into finitely many languages that are orderablein this sense. For the slender languages, we can again characterize the minimal number of languages in thepartition, and achieve boundeddelay enumeration.This is joint work with Mikaël Monet, and was presented at STACS’23. 
Constructing Deterministic
Parity Automata from Positive and Negative Examples
Constructing Deterministic Parity Automata from Positive and Negative ExamplesWe present a polynomial time algorithm that constructs a deterministic parity automaton DPA from a given set of positive and negative ultimately periodic example words. We show that this algorithm is complete for the class of ωregular languages, that is, it can learn a DPA for each regular ωlanguage. For this purpose, we propose a canonical form of DPA, which we call precise DPA (of a language), and show that it can be constructed from the syntactic family of right congruences for that language (introduced by Maler and Staiger in 1997. The precise DPA can be of exponential size compared to a minimal DPA for a language, but it can also be a minimal DPA, depending on the structure of the language. The upper bound that we obtain on the number of examples required for our algorithm to find a DPA for L is therefore exponential in the size of a minimal DPA, in general. But we identify two parameters of regular ωlanguages such that fixing these parameters makes the bound polynomial.This is joint work with Christof Löding. 
A dual adjunction between
Ωautomata and Wilke algebras
A dual adjunction between Ωautomata and Wilke algebrasΩautomata are a type of automata for ωregular languages. Instead of infinite words, they read pairs of finite words, called lassos, that represent ultimately periodic words. Due to the fact that ωregular languages are determined by their ultimately periodic fragments, Ωautomata can be associated with ωregular languages. In terms of structure, they resemble pairs of DFAs, and as a result they can be modelled as coalgebras.We study the categorical relationship between Ωautomata and Wilke algebras, which recognise ωregular languages. We present a chain of adjunctions starting from the category of Ωautomata without initial states and ending with the dual of the category of quotients of the free Wilke algebra. As key ingredients, we determine how the Ωautomata properties circularity and coherence change under transition reversal and propose novel transformations between Ωautomata and Wilke algebras.Consequently, we obtain a dual adjunction between Ωautomata (with an initial state) for a language and quotients of the free Wilke algebra for that language. We note that every quotient Wilke algebra is mapped to an observable Ωautomaton, and every reachable Ωautomaton gets mapped to the syntactic Wilke algebra.This is joint work with Helle Hvid Hansen (University of Groningen) and Clemens Kupke (University of Strathclyde). 
Formal Reasoning about Influence
in Natural Sciences Experiments
Formal Reasoning about Influence in Natural Sciences ExperimentsWe present a simple calculus for deriving statements about the local behaviour of partial, continuous functions over the reals, within a collection of such functions associated with the elements of a finite partial order. The motivation for this work is drawn from an attempt to foster digitalisation in secondaryeduction classrooms, in particular in experimental lessons in natural science classes. This provides a way to formally model experiments and to automatically derive the truth of hypotheses made about certain phenomena in such experiments.The proof calculus turns out to be sound in general, complete for a large class of formal experiment models, and is decidble in polynomial time.This is joint work with Florian Bruse, Sören Möller and Shahla Rasulzade from the University of Kassel. 
Semantics of AttackDefense
Trees for Dynamic Countermeasures: a New Hierarchy of Starfree
Languages
Semantics of AttackDefense Trees for Dynamic Countermeasures: a New Hierarchy of Starfree LanguagesThe presentation aims at presenting a mathematical setting for attackdefense trees, a classic graphical model to specify attacks and nested countermeasures,that we equip with trace language semantics allowing to have an original dynamic interpretation of countermeasures. Interestingly, the expressiveness of attackdefense trees coincides with starfree languages, and the nested countermeasures impact the expressiveness of attackdefense trees. With an adequate notion of counterdepth, we exhibit a strict hierarchy of the starfree languages that does not coincides either with the dotdepth hierarchy, or with the firstorder logic alternation quantifier hierarchy on the very first levels. Additionally, driven by the use of attackdefense trees in practice, we address the decision problems of trace membership and of nonemptiness, and study their computational complexities parameterized by the counterdepth. The presentation is based on a joint work with Sophie Pinchinat and Thomas Brihaye. 
Nominal Topology for Data
Languages
Nominal Topology for Data LanguagesWe propose a novel topological perspective on data languages recognizable by orbitﬁnite nominal monoids. For this purpose, we introduce proorbitﬁnite nominal topological spaces, a form of nominal topological spaces generalizing classical profinite spaces. Assuming globally bounded support sizes of the underlying nominal sets, which correspond to bounds on the number of registers of automata, proorbitﬁnite nominal topological spaces coincide with nominal Stone spaces and are shown to be dually equivalent to a suitable subcategory of nominal boolean algebras. Recognizable data languages are characterized as topologically clopen sets of proorbitﬁnite words. In addition, we explore the expressive power of proorbitﬁnite equations and provide a nominal version of Reiterman’s pseudovariety theorem. This talk is based on joint work with Fabian Birkmann and Stefan Milius, presented at ICALP 2023. 
Coffee Break
Thursday 16h00  17h00, Special Session  HS 3 
"Open Problems Tools and Experiments"
Friday
Friday 09h00  10h00, Keynote Speaker  HS 3  
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   Games 3  HS 4  
1–2–3–Go! Explainable Policies
for Arbitrarily Large Parameterized Markov Decision Processes via
DecisionTree Generalization
1–2–3–Go! Explainable Policies for Arbitrarily Large Parameterized Markov Decision Processes via DecisionTree GeneralizationDespite the advances in probabilistic model checking, the scalability of the verification methods as well as the explainability of the results remains limited. In particular, when instantiating parametrized Markov decision processes (MDPs) even with moderate values, the state space often becomes extremely large; similarly, the policy, if any is produced, can be too large an object to be understood, or even implemented. To tackle these issues, we propose a simple learningbased approach to construct often nearoptimal policies and their interpretable representations as decision trees, even for huge MDPs. The main idea is to generalize optimal strategies from smaller to larger instantiations, using decisiontree learning.This is a joint work with Alexandros Evangelidis, Jan Křetı́nský, Mohammadsadegh Mohagheghi, Stefanie Mohr, and Maximilian Weininger. 
Mean Payoff Optimization for
Systems of Periodic Service and Maintenance
Mean Payoff Optimization for Systems of Periodic Service and MaintenanceConsider oriented graph nodes requiring periodic visits by a service agent. The agent moves among the nodes and receives a payoff for each completed service task, depending on the time elapsed since the previous visit to a node. We consider the problem of finding a suitable schedule for the agent to maximize its longrun average payoff per time unit. We show that the problem of constructing an epsilonoptimal schedule is PSPACEhard for every fixed nonnegative epsilon, and that there exists an optimal periodic schedule of exponential length. We propose randomized finitememory (RFM) schedules as a compact description of the agent's strategies and design an efficient algorithm for constructing RFM schedules. Furthermore, we construct deterministic periodic schedules by sampling from RFM schedules.This is a joint work with David Klaška, Antonín Kučera, and Vít Musil and it has been accepted as a full paper for the main track of the IJCAI 2023 conference. 
MDPs as Distribution
Transformers: Affine Invariant Synthesis for Safety Objectives
MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety ObjectivesMarkov decision processes can be viewed as transformers of probability distributions. While this view is useful from a practical standpointto reason about trajectories of distributions, basic reachability and safetyproblems are known to be computationally intractable (i.e., Skolemhard)to solve in such models. Further, we show that even for simple examples ofMDPs, strategies for safety objectives over distributions can require infinitememory and randomization.In light of this, we present a novel overapproximation approach to synthesizestrategies in an MDP, such that a safety objective over the distributionsis met. More precisely, we develop a new framework for templatebasedsynthesis of certificates as affine distributional and inductive invariants forsafety objectives in MDPs. We provide two algorithms within this framework.One can only synthesize memoryless strategies, but has relative completenessguarantees, while the other can synthesize general strategies. The runtimecomplexity of both algorithms is in PSPACE. We implement these algorithmsand show that they can solve several nontrivial examples.This is joint work with S. Akshay, Krishnendu Chatterjee and Tobias Meggendorfer that will be presented at CAV 2023. 
MultiWeighted Reachability
Games
MultiWeighted Reachability GamesWe study twoplayer multiweighted reachability games played on a finite directed graph, where an agent, called P1, has several quantitative reachability objectives that he wants to optimize against an antagonistic environment, called P2. In this setting, we ask what cost profiles P1 can ensure regardless of the opponent's behavior. Since this set of ensured values may not be a singleton, cost profiles are compared thanks to: (i) a lexicographic order that ranks the objectives a priori, ensuring the unicity of an upper value or (ii) a componentwise order. In the latter case, P1 chooses his ``preferred'' ensured value a fortiori, once he knows the Pareto frontier. We synthesize (i) lexicooptimal strategies and (ii) Paretooptimal strategies. The strategies are obtained thanks to a fixpoint algorithm which also computes the upper value in polynomial time and the Pareto frontier in exponential time. Finally, we study the complexity of a related decision problem: the constrained existence problem. This problem is proved in P with the lexicographic order and PSpacecomplete with the componentwise order. This is a joint work with Thomas Brihaye. 
The Probabilistic Rabin Tree
Theorem
The Probabilistic Rabin Tree TheoremThe Rabin tree theorem yields an algorithm to solve the satisfiability problem for monadic secondorder logic over infinite trees. Here we solve the probabilistic variant of this problem. Namely, we show how to compute the probability that a randomly chosen tree satisfies a given formula. We additionally show that this probability is an algebraic number. This closes a line of research where similar results were shown for formalisms weaker than the full monadic secondorder logic.Joint work with Damian Niwiński and Michał Skrzypczak, submitted (under review). 
Joker Games for checking
HistoryDeterminism
Joker Games for checking HistoryDeterminismHistorydeterminism is a property of models where the nondeterministic choices in the model are resolved `onthefly’ based on the input read so far. Historydeterministic parity automata are known to be more succinct than their deterministic counterpart (Kuperberg, Skrzypczak 2015), and exhibit compositionality with games akin to deterministic automata (Henzinger, Piterman 2006), hence they’re also called goodforgames.The exact complexity of checking historydeterminism for higher parity indices remains open despite significant efforts, and is only known to be polynomial time for the lower indices of Büchi and coBüchi. The underlying technique for the recent polynomial time algorithms for these use twotoken games: Finding the winner in the twotoken game turns out to be equivalent to checking historydeterminism when the parity automaton is a Büchi or coBüchi automaton (Bagnol, Kuperberg 2018; Boker, Kuperberg, Lehtinen, Skrzypczak 2020). It is conjectured that twotoken games characterise historydeterminism for all parity automata as well, and this is known as the twotoken or the G2 conjecture. We show that for Büchi automata, checking historydeterminism is equivalent to solving the joker game. These were originally used by Kuperberg and Skrzypczak (2015) to give a polynomialtime algorithm for checking historydeterminism of a coBüchi automaton, but it is not known if joker games characterise historydeterminism for coBüchi automata.The arena of joker games is smaller than that of twotoken games by a linear factor, and thus solving joker games is faster by a quadratic factor than solving twotoken games for Büchi automata. Moreover, our result implies that twotoken games characterise historydeterminism for Büchi automata, and thus is an alternative proof of the twotoken conjecture for the Büchi case. This leads us to propose the joker conjecture: Checking historydeterminism on a parity automaton is equivalent to finding the winner in the joker game. This is a stronger version of the twotoken conjecture. We also hope that our ongoing work on joker games could lead to insights that help us progress in discovering efficient algorithms for checking historydeterminism, as well as towards the G2 conjecture.(Joint ongoing work with Udi Boker, Marcin Jurdziński and Karoliina Lehtinen) 
Timed Alignments
Timed AlignmentsThe subject of this presentation is to study conformance checking for timed models, that is, process models that consider both the sequence of events in a process as well as the timestamps at which each event is recorded. Timeaware process mining is a growing subfield of research, and as tools that seek to discover timing related properties in processes develop, so does the need for verification techniques that can tackle time constraints and provide insightful quality measures for timeaware process models. In particular, one of the most useful conformance artefacts is the alignment, that is, finding the minimal changes necessary to correct a new observation to conform to a process model. In this presentation, we set the problem of timed alignment and solve three cases each corresponding to a different metric over time processes. For the first, we have an algorithm whose time complexity is linear both in the size of the observed trace and the process model, and for the second, we provide an encoding in simplex. For the second and third, we further restrict our attention to process models with linear causal processes which allows us to provide a quadratic time algorithm, and a linear time algorithm, respectively. 
Reachability Poorman
DiscreteBidding Games
Reachability Poorman DiscreteBidding GamesWe consider "bidding games", a class of twoplayer zerosum "graph games". The game proceeds as follows. Both players have bounded budgets. A token is placed on a vertex of a graph, in each turn the players simultaneously submit bids, and the higher bidder moves the token (ties are broken according to a predefined mechanism). Player 1 wins the game iff the token visits a designated target vertex. We consider, for the first time, "poorman discretebidding" in which the granularity of the bids is restricted and the higher bid is paid to the bank. In contrast, in "Richman continuousbidding" bids can be arbitrarily small and are paid to the other player. While the latter mechanism is technically more accessible, the former is more appealing from a practical standpoint. Our study focuses on "threshold budgets", which is the necessary and sufficient initial budget required for Player 1 to ensure winning against a given Player 2 budget. We show existence of thresholds when Player 1 wins bidding ties. In DAGs, we show that threshold budgets can be approximated with error bounds by thresholds under continuousbidding and that they exhibit a periodic behavior. We identify closedform solutions in special cases. We implement and experiment with an algorithm to find threshold budgets.This is a joint work with Guy Avni, Tobias Meggendorfer, Josef Tkadlec, and Djordje Zikelic. 
One timed model to unify them
all!  A foundation for efficient MITL Modelchecking
One timed model to unify them all!  A foundation for efficient MITL ModelcheckingTimed automata are a wellestablished model for realtime systems. Over the years, various timed temporal logics (such as MTL, MITL) have been proposed with the goal of modelchecking realtime systems. A widely used formalism to model timed speciﬁcations is Eventclock automata (ECA). Even though ECA is a subclass of timed automata, the translation from ECA to Timed automata is expensive. Consequently, a framework that can capture the features of both Timed automata and Eventclock automata would provide a way to directly modelcheck timed temporal specifications over timed systems. In this work, we propose a new model, called Generalized Timed Automata (GTA), that unifies the features of various models such as timed automata, eventclock automata (with and without diagonal constraints), and automata with timers. Our main contribution is a new simulationbased zone algorithm for checking reachability in this unified model. While such algorithms are known to exist for timed automata, and have recently been shown for eventclock automata without diagonal constraints, this is the first result that can handle eventclock automata with diagonal constraints and automata with timers. We also provide a prototype implementation of our model and algorithm in TChecker, an opensource platform for timed automata analysis, and show promising results on several existing and new benchmarks. This is the first effective implementation not just for our unified model, but even just for automata with timers or for eventclock automata (with predicting clocks) without going through a costly translation via timed automata. Joint work with S Akshay, Paul Gastin, Aniruddha Joshi and B Srivathsan. 
Solving EmersonLei Games via
Zielonka Trees
Solving EmersonLei Games via Zielonka TreesWe show how EmersonLei games can be solved symbolically by providing a fixpointbased characterization of the winning region, which results from analysis of the Zielonka tree of the winning condition. The proposed algorithm generalizes the solutions of known winning conditions such as parity, Streett, Rabin, and GR[1] objectives, and in the case of these conditions reproduces previously known algorithms and complexity results; the algorithm solves unrestricted EmersonLei games with n nodes, m edges and d colors in time O((n^(d/2)) d! m). 
Timed Recursive CTL
Timed Recursive CTLWe study the complexity of the modelchecking problem of Timed Recursive CTL, TRecCTL. This logic is obtained as the merger of two extensions of CTL, Timed CTL and Temporal Logic with Recursion. The former extends CTL by operators to talk about timed aspects of systems defined by timed automata. The latter adds a recursion operator to CTL, greatly increasing the expressive power of the resulting logic.We obtain that the modelchecking problem for TRecCTL is 2EXPTIME complete. Moreover, the modelchecking problem for the socalled tailrecursive fragment of TRecCTL, obtained by limiting the way recursion is used, is EXPSPACE complete. Notably, the former problem is already 2EXPTIME hard in its expression complexity, and the latter is already EXPSPACE complete in its data complexity. Moreover, the hardness result already holds for timed automata with one clock only. For Timed CTL, the amount of clocks present is important. 
Lunch
Friday 14h00  14h48, Contributed Talks



Model Theory & Logic  HS 3   Applications and Other Topics  HS 4  
On the Descriptive Complexity of
Groups without Abelian Normal Subgroups
On the Descriptive Complexity of Groups without Abelian Normal SubgroupsIn this talk, I will discuss the descriptive complexity theory of finite groups by examining the power of the second EhrenfeuchtFraïss\'e bijective pebble game in Hella's (Ann. Pure Appl. Log., 1989) hierarchy. This is a SpoilerDuplicator game in which Spoiler can place up to two pebbles each round. While it trivially solves graph isomorphism, it may be nontrivial for finite groups, and other ternary relational structures. Our main result is that, in the pebble game characterization, only $O(1)$ pebbles and $O(1)$ rounds suffice to identify all groups without Abelian normal subgroups (a class of groups for which isomorphism testing is known to be in \textsf{P}; Babai, Codenotti, \& Qiao, ICALP 2012). By Hella's results (ibid.), this is equivalent to saying that these groups are identified by formulas in firstorder logic with generalized $2$ary quantifiers, using only $O(1)$ variables and $O(1)$ quantifier depth.This is joint work with Joshua A. Grochow. 
Comprehensive Specification and
Formal Analysis of Attestation Mechanisms in Confidential
Computing
Comprehensive Specification and Formal Analysis of Attestation Mechanisms in Confidential ComputingThe proposed talk is intended for themes “Verification” and “Applications”. The talk aims to introduce an emerging and exciting domain of confidential computing with our recent work on specification and verification of one of the most critical mechanisms, namely remote attestation, and ignite discussions on promising directions of future research and collaborations. Confidential Computing (CC) using hardwarebased Trusted Execution Environments (TEEs) has emerged as a promising solution for protecting sensitive data in all forms. One of the fundamental characteristics of such TEEs is remote attestation [4] which provides mechanisms for securely measuring and reporting the state of the remote platform and computing environment to a user. We present a novel approach combining TEEagnostic attestation architecture and formal analysis enabling comprehensive and rigor ous security analysis of attestation mechanisms in CC. We demonstrate the application of our approach for three prominent industrial representatives, namely Arm Confidential Compute Architecture (CCA) [1, 2] in architecture lead solutions, Intel Trust Domain Extensions (TDX) [5] in vendor solutions, and Secure CON tainer Environment (SCONE) [3] in frameworks. For each of these solutions, we provide a comprehensive specification of all phases of the attestation mechanism in confidential computing, namely provisioning, initialization, and attestation protocol. Our approach reveals design and security issues in Intel TDX and SCONE attestation. 
Unified Foundations of Team
Semantics via Semirings
Unified Foundations of Team Semantics via SemiringsSemiring semantics for firstorder logic provides a way to trace how facts represented by a model are used to deduce satisfaction of a formula.Team semantics is a framework for studying logics of dependence and independence in diverse contexts such as databases, quantum mechanics, and statistics by extending firstorder logic with atoms that describe dependencies between variables. Combining these two, we propose a unifying approach for analysing the concepts of dependence and independence via a novel semiring team semantics, which subsumes all the previously considered variants for firstorder team semantics.In particular, we study the preservation of satisfaction of dependencies and formulae between different semirings. In addition we create links to reasoning tasks such as provenance, counting, and repairs.This is joint work with Timon Barlag, Miika Hannula, Juha Kontinen, and Jonni Virtema. 
Teaching reductions: Formal
foundations
Teaching reductions: Formal foundationsDesigning computational reductions is a challenging task for students. Inthis paper we explore formal foundations for offering support for thislearning task by teaching support systems. Our approach is to (a)identify typical building blocks of reductions, (b) develop a simpledescriptional language for specifying reductions that allows forcombining building blocks in a simple, modular manner, (c) study theexpressive power of such a language to ensure that it is reasonablybroad, and to (d) design suitable algorithms for employing this languagein teaching support systems, including the design of feedback mechanisms.This is joint work with Julien Grange, Nils Vortmeier and Thomas Zeume. 
Polyregular functions on
unordered trees of bounded height
Polyregular functions on unordered trees of bounded heightJoint work with Bartek Klin (Oxford)We consider firstorder interpretations that input and output trees of bounded height. The corresponding functions have polynomial output size, since a firstorder interpretation can use a $k$tuple of input nodes to represent a single output node. We prove that the equivalence problem for such functions is decidable, i.e.~given two such interpretations, one can decide whether for every input tree, the two output trees are isomorphic. This result is incomparable to the open problem about deciding equivalence for polyregular stringtostring functions.We also give a calculus, based on prime functions and combinators, which derives all firstorder interpretations for unordered trees of bounded height. The calculus is based on a type system, where the type constructors are products, coproducts and multisets. Thanks to the results about treetotree interpretations, the equivalence problem is decidable for this calculus.As an application of our results, we show that the equivalence problem is decidable for firstorder interpretations between classes of graphs that have bounded tree depth. In all cases studied in this paper, firstorder logic and mso have the same expressive power, and hence all results apply also to mso interpretations. 
ProblemSpecific Visual Feedback
in Discrete Modelling
ProblemSpecific Visual Feedback in Discrete ModellingDiscrete modelling as the basis of problem solving is an essential skill for computer scientists, but the correct use of formal languages like propositional logic for such purposes remains a big challenge for undergraduate students.We present a tool, called DiMo, aimed at supporting the acquisition of such formal modelling competencies using propositional logic. The DiMo tool provides a language which allows propositional formulas  parameterised by integers  to be specified and checked for satisfiability, validity and equivalence, and thus, allows parametrised realworld problems to be modelled in propositional logic.We specifically focus on DiMo's generic capabilities to form problemspecific feedback that allows users to visualise the result of their modelling attempts in terms of the modelled problemat hand, thus helping students to initiate corresponding learning cycles.The results presented in this talk are based on joint work with Norbert Hundeshagen, John Hundhausen, Stefan Kablowski and Martin Lange. 
Membership Problems in
Subclasses of Rational Relations
Membership Problems in Subclasses of Rational RelationsWe revisit the membership problem for subclasses of rational relations over finite and infinite words: Given a relation R in a class C_2, does R belong to a smaller class C_1? The subclasses of rational relations that we consider are formed by the deterministic rational relations, synchronous (also called automatic or regular) relations, and recognizable relations. We provide improved complexity and new decidability results. (i) Testing whether a synchronous relation over infinite words is recognizable is NLcomplete (PSPACEcomplete) if the relation is given by a (non)deterministic omegaautomaton. (ii) Testing whether a deterministic rational binary relation is recognizable is decidable in polynomial time. For relations of higher arity, we present a randomized exponential time algorithm. (iii) We provide the first algorithm to decide whether a deterministic rational relation is synchronous. For binary relations the algorithm even runs in polynomial time. 
The MIX2 language is not an
EDT0L language
The MIX2 language is not an EDT0L languageThe MIX languages have attracted the attention of at least two communities: mathematical linguistics and computational group theory. The first one considers these languages as being completely unstructured and they should not be in the class of languages which are used to define natural languages. The second community is interested in classifying groups in terms of the formal properties of their word languages. In this work we prove that the MIX2 language is not generated by EDT0L systems. We first prove that it is not generated by a nonbranching Multiple ContextFree Grammar, which is known to be equivalent to EDT0L systems of finite index. We prove this by providing a family of counterexamples words. Finally we bridge the gap with general EDT0L systems using a theorem from Latteux. 