Polyregular functions are the class of string-to-string functions definable by pebble transducers, an extension of finite-state automata with outputs and multiple two-way 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 k-fold composition of macro tree transducers (and which therefore cannot be computed by a k-pebble transducer). Along the way, we also refute a conjectured logical characterization of polyblind functions.

We propose a novel algorithm to decide the language inclusion between (nondeterministic) Buchi automata, a PSpace-complete 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 FORQ-based 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 state-of-the-art on a variety of benchmarks including benchmarks from program verification and theorem proving for word combinatorics.

We show that the big-O problem for max-plus automata, i.e. weighted automata over the semiring (N ∪ {-∞}, max, +), is decidable and PSPACE-complete. The big-O (or affine domination) problem asks whether, given two max-plus 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.

Recently, Frits W. Vaandrager et al. [1] studied learning (automatic construction using the well-known 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 non-deterministically 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 PSPACE-complete.[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).

Higher dimensional automata (HDAs) were introduced by Pratt and van Glabbeek as a general geometric model for non-interleaving 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 subsumption-closed sets of partially ordered multisets with interfaces (ipomsets), and shown a Kleene theorem and a Myhill-Nerode 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 non-regular 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 width-bounded version of complement and show that width-bounded complements of regular languages are again regular.

Counting 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 Z-valued 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 One-Counter Automata (POCA): the ``Parikh'' part referring to the evaluation of counters at the end of runs, and the ``One-Counter'' 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.

Recent years have witnessed a growing interest in reasoning about the finite-horizon 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 model-checking from $\ltlf$ specifications. We observe that there are striking differences between $\ltlf$ and $\ltl$ model checking. Most significantly, under the same non-terminating 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 \pspace-complete. Thus, demonstrating the importance of semantics in model checking for finite-horizon temporal specifications.

We 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 infinite-state systems. This is a joint work with Pierre Ganty and Francesco Ranzato.

We consider the verification of distributed systems composed of an arbitrary number of asynchronous processes. Processes are identical finite-state machines communicating by reading from and writing to a shared memory. Beyond the standard model with finitely many registers, we tackle round-based shared-memory 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 round-based setting, we establish that the parameterized verification of presence reachability properties is PSPACE-complete. Moreover, for the roundless model with finitely many registers, we prove that the complexity drops down to NP-complete and we provide several natural restrictions that make the problem solvable in polynomial time.

We 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 Hyper-Ackermannian. We contrast this with the undecidability of the closely-related target reachability problem on one hand, and with the NP-completeness of the problem when each agent has only one register on the other.This is joint work with Lucie Guillou and Nicolas Waldburger.

In the language-theoretic 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 EXPSPACE-complete -- 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 EXPSPACE-complete. 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 (context-free) language of each task in an asynchronous program by a regular language. Unlike downward closure operations usually considered in infinite-state verification, our ordering is not a well-quasi-ordering, 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.

A 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 input-deterministic multistack pushdown language. Our main result shows that the context-bounded 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 coNP-complete. The more general case of input-deterministic languages follows, with the same complexity.Context-bounding is essential since emptiness for multipushdown automata is already undecidable, and so is the refinement verification problem for the subclass of regular specifications. Input-deterministic languages capture many non-regular specifications of practical interest and our result opens the way for algorithmic analysis of these properties. The context-bounded refinement problem is coNP-hard 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 non-deterministic 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 re-entrant locking in multithreaded programs.This is joint work with Pascal Baumann, Moses Ganardi, Rupak Majumdar and Georg Zetzsche.

In 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 star-free 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 star-free regular languages and is closed under union, intersection, concatenation, and Kleene star.

This 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 objective-specific subroutines as well as identify objective-independent concepts.These structural concepts, while surprisingly simple, form the very essence of the unified solution.

We 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 poly-logarithmic 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 succinctly-represented, 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.

Weighted timed games are two-player zero-sum 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 one-clock WTGs with only non-negative 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 one-clock 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 Pierre-Alain Reynier.

We 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 no-surprise 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 well-known 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, Jean-Franç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.

We study infinite two-player 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 on-the-fly 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 almost-surely) winning strategy, then she has a finite-memory one. These classes include variations of typically well-studied games such as Büchi/Parity games on finite graphs or energy games.Co-authors: Patricia Bouyer and Stéphane Le Roux.

Regular 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 left-to-right and right-to-left), letter-to-letter 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 27-30, 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 second-order logic." arXiv e-prints (2020): arXiv-2008.Bojańczyk, Mikołaj, Bartek Klin, and Julian Salamanca. "Monadic monadic second order logic." arXiv preprint arXiv:2201.09969 (2022).

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 higher-order 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 star-free languages, regular tree functions (in a similar fashion to Gallot, Lemay & Salvati 2020) and comparison-free 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/category-theoretic tools that they involve, are recapitulated in the longer abstract https://cs-web.swan.ac.uk/~cpradic/smp-abstract.pdfMore recently, I have devised a transducer model, based on the collapsible pushdown automata used in HOMC, that captures the tree-to-tree 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.

Authors: 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 “(one-dimensional) unboundedness predicates”, for automata that feature reversal-bounded counters (RBCA). We show that each problem in this class reduces—non-deterministically 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 reversal-bounded counters (PRBCA).This allows us to answer several open questions: For example, we show that it is coNP-complete 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 Z-counters in logarithmic space, while preserving the accepted language.

Given 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.

A $k$-Counter Net ($k$-CN) is a finite-state automaton equipped with $k$ integer counters that are not allowed to become negative, but do not have explicit zero tests. This language-recognition 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 dimension-primality 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: dimension-minimality (where we seek a single language-equivalent $d$-CN of lower dimension) and language regularity.Additionally, we explore the trade-offs in expressiveness between dimension and non-determinism for CN.This presentation is based on submitted work with Shaull Almagor, Guy Avni and Henry Sinclair-Banks.

We introduce one deterministic-counter automata (ODCA), which are one-counterautomata where all runs labelled by a given word have the same counter effect,a property we call counter-determinacy. ODCAs are an extension of visiblyone-counter automata - one-counter automata (OCA), where the input alphabetdetermines the actions on the counter. They are a natural way to introducenon-determinism/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 fornon-deterministic OCAs. We consider both non-deterministic and weighted ODCAs.Our work shows that the equivalence problem is decidable in polynomial timefor weighted ODCAs over a field and polynomial space for non-deterministicODCAs. 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

For 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 integer-valued 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 Lyndon-Sch\"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.

In general, finite concurrent two-player games behave poorly, especially when compared totheir turn-based counterparts. For instance, in deterministic turn-based games — with a Borelobjective — either of the players has a winning strategy, which fails in concurrent reachabil-ity games even with a single non-trivial concurrent interactions of the players. Furthermore,considering stochastic games, in finite turn-based 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 two-step 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 turn-based 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 non-trivial 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.

Given 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 criteria-agnostic form that makes it possible to subsequently extract Skolem functions for different criteria. Our approach is based on a novel counter-example 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.

Recently Ehlers&Schewe proposed a canonical minimal representation foromega-regular languages [1]. The representation consists of a canonical chainof co-Büchi languages (COCOA): A1 ⊃ A2 ⊃ ... ⊃ An, where each Ai is expressibleby a good-for-games co-Bü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 amu-calculus 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 Transition-Based Automata, by Bader {Abu Radi} and Orna Kupferman

The problem of synthesizing controllers with respect to temporal logic specifications has received considerable attention in the last decade, especially in the context of cyber-physical systems (CPS) design. Such problems occur for example in the control of autonomous robots deployed in warehouses, for under-water 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, two-player 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 high-level game solving algorithms with feedback-controller 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 higher-layer game solving problem targeted towards controller synthesis for CPS. The key contribution of our work is two-fold. First, instead of synthesizing single strategies, we compute \emph{strategy templates} which allow for a certified translation into low-level 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, Anne-Kathrin Schmuck, and Raphaël Jungers.

The 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 MSO-definable parity games, which is, finding MSO-definable uniform memoryless winning strategies for these games.

In 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 non-blocking 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.

A central task in control theory, artificial intelligence, andformal methods is to synthesize reward-maximizing strategies for agentsthat operate in partially unknown environments. In environments modelled by gray-box 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 forgray-box 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 pre-print is avaiable.

Deep 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 safety-critical 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.

AbstractConsider 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 ex-ample 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 d-tuple ofelements from the universe. We aim to learn a monadic second-order 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 problemMSO-Learn and for d = 1 we speak of unary-MSO-Learn.We analyze the problem in the context of parameterized complexity and show that it is fixed-parameter tractable for d=1 on structures of bounded tree-width and graphs of bounded clique-width. Furthermore, we give bounds for d>1 in the PAC learning framework.

We discuss how to efficiently combine formal methods, Monte Carlo Tree Search (MCTS), and deep learning in order to produce high-quality receding horizon strategies in large Markov Decision processes (MDPs). In particular, we use model-checking techniques to guide the MCTS algorithm in order to generate offline samples of high-quality 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 lower-latency MCTS online search, or alternatively be used as a full-fledged 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 (computationally-expensive) offline strategy. We illustrate the use of our method on MDPs that model the Frozen Lake and Pac-Man environments --- two popular benchmarks to evaluate reinforcement-learning algorithms.The talk is based on the same-titled paper accepted at AAMAS,2023. This is a joint work with Damien Busatto-Gaston, Jean-François Raskin and Guillermo A. Pérez.

We 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.

We 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 secondary-eduction 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.

Despite 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 learning-based approach to construct often near-optimal 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 decision-tree learning.This is a joint work with Alexandros Evangelidis, Jan Křetı́nský, Mohammadsadegh Mohagheghi, Stefanie Mohr, and Maximilian Weininger.

Markov 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., Skolem-hard)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 template-basedsynthesis 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 non-trivial examples.This is joint work with S. Akshay, Krishnendu Chatterjee and Tobias Meggendorfer that will be presented at CAV 2023.

The Rabin tree theorem yields an algorithm to solve the satisfiability problem for monadic second-order 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 second-order logic.Joint work with Damian Niwiński and Michał Skrzypczak, submitted (under review).

The 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. Time-aware 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 time-aware 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.

Timed automata are a well-established model for real-time systems. Over the years, various timed temporal logics (such as MTL, MITL) have been proposed with the goal of model-checking real-time systems. A widely used formalism to model timed specifications is Event-clock 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 Event-clock automata would provide a way to directly model-check 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, event-clock automata (with and without diagonal constraints), and automata with timers. Our main contribution is a new simulation-based 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 event-clock automata without diagonal constraints, this is the first result that can handle event-clock automata with diagonal constraints and automata with timers. We also provide a prototype implementation of our model and algorithm in TChecker, an open-source 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 event-clock 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.

We study the complexity of the model-checking 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 model-checking problem for TRecCTL is 2EXPTIME complete. Moreover, the model-checking problem for the so-called tail-recursive 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.

In this talk, I will discuss the descriptive complexity theory of finite groups by examining the power of the second Ehrenfeucht--Fraïss\'e bijective pebble game in Hella's (Ann. Pure Appl. Log., 1989) hierarchy. This is a Spoiler-Duplicator 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 first-order logic with generalized $2$-ary quantifiers, using only $O(1)$ variables and $O(1)$ quantifier depth.This is joint work with Joshua A. Grochow.

Semiring semantics for first-order 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 first-order 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 first-order 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.

Joint work with Bartek Klin (Oxford)We consider first-order interpretations that input and output trees of bounded height. The corresponding functions have polynomial output size, since a first-order 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 string-to-string functions.We also give a calculus, based on prime functions and combinators, which derives all first-order interpretations for unordered trees of bounded height. The calculus is based on a type system, where the type constructors are products, co-products and multisets. Thanks to the results about tree-to-tree interpretations, the equivalence problem is decidable for this calculus.As an application of our results, we show that the equivalence problem is decidable for first-order interpretations between classes of graphs that have bounded tree depth. In all cases studied in this paper, first-order logic and mso have the same expressive power, and hence all results apply also to mso interpretations.

We 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 NL-complete (PSPACE-complete) if the relation is given by a (non)deterministic omega-automaton. (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.