GT DAAL 2026

Given a relational specification {$\varphi(X, Y)$}, functional synthesis concerns the construction of functions (or terms) {$F(X)$} such that {$\varphi(X, F(X))$} is semantically equivalent to {$\exists Y \varphi(X, Y)$}. Such functions are also called Skolem functions, and their algorithmic synthesis has many applications, including in program synthesis, QBF-SAT certificate generation, circuit repair, reactive synthesis, planning and the like. The synthesis problem is intractable unless long-standing complexity-theoretic conjectures are falsified. Fortunately, polynomial-time synthesis algorithms can be designed if {$\varphi$} is compiled to special normal forms.

In this talk, we present some such normal forms in the propositional setting, and discuss algorithms to compile to such forms. We show that normal forms originally studied in AI and formal verification, such as Decomposable Negation Normal Form (DNNF), weak DNNF and deterministic DNNF admit polynomial-time synthesis. We show that new normal forms like Synthesis Negation Normal Form (SynNNF) and Subset And-Unrealizable Normal Form (SAUNF) can be defined, that lead to efficient functional synthesis in the Boolean setting. We discuss properties of and relations between these normal forms, and show that every universal representation that admits polynomial-time synthesis is polynomially reducible to SAUNF for Boolean functional synthesis. We present preliminary results of compiling from conjunctive normal form (CNF) to SynNNF, that show the promise of this approach in practice.

In recent years, hyperproperties and their specification languages have gained significant attention within formal methods, security, and cyber-physical systems communities. Hyperproperties relate multiple execution traces in a system and are thereby able to express information-flow properties capturing security and privacy requirements.

HyperLTL is obtained by extending LTL, the most influential specification language for linear time properties, by trace quantifiers in order to refer to multiple executions of a system.

HyperLTL model-checking is decidable but expensive. A cheaper (but incomplete) method interprets the verification of a HyperLTL formula as a two-player game between universal and existential quantifiers. This approach is particularly well-suited for producing easily verifiable certificates of satisfaction or violation.

We present the first sound and complete game-based verification algorithm for HyperLTL.

This talk is based on joint work with Martin Zimmermann.

We design an extension of the ATL* that captures framework with both imperfect information and resource settings, and we study its model-checking problem. Both direction being prompt to undecidability, we investigate a fragment in which agents are totally ordered according to their access to information, and have knowledge about the weights.

We prove that the model-checking problem of this fragment is decidable, by introducing a new class of automata extending alternating and nondeterministic parity tree automata by adding resource considerations, and lifting important results on them, such as a simulation theorem.

Timed automata form an elegant and well-studied model for real-time systems. Many efficient algorithms and tools have been developed to analyse by checking the existence of errors in their executions (translated as reachability problems). However, instead of its elegance, this model exposes some undesirable artefacts from the mathematical model. Especially the precision in time measurement is supposed to be arbitrary, which is unrealistic. To deal with this issue, many notions of robustness were introduced. In this talk, I will discuss some of them and some recent advancements in the context of timed games.

Macro Tree Transducers (or MTTs for short) are a model of tree-to-tree functions that generalizes the classic top-down tree transducers. They were introduced in 1980 as a generalization of attribute grammars, a model used in natural language processing and compilation theory to assign semantic meaning to words in a context-free language. We present the decidable characterisation of Linear Size-To-Height Macro Tree Transducers (LSHI MTTs) from Gallot, Maneth, Nakano & Peyrat 2023, and also explore how we, in collaboration with Lê Thành Dũng Nguyên and Luc Dartois, reused this characterisation to relate MTTs and some other computational models on trees, including Tree-to-tree Hennie Machines, a generalisation of Tree-Walking Transducers.

We consider the sequences of natural integers that can be computed by a deterministic transducer, with input in a arbitrary structure, output in natural integers and with memory the set of stacks of stacks of the structure. We show, by constructive proofs, that these sequences are, exactly, the counting sequences of formal languages generated by unambiguous context-free indexed grammars, with indexes in the structure. This general theorem applies, notably, to the structure of natural integers endowed with the decrement operation, showing that the polynomial recurrences count exactly the index-languages.

Active automata learning (AAL) under a Minimally Adequate Teacher (MAT) has been successfully used to infer a regular language through membership and equivalence queries. This language might not be fully characterized: we are thus interested in finding any solution in a target class of possibly many regular languages. Some problems such as regular language separation or inductive invariant synthesis in the context of regular model checking (RMC) may indeed admit more than one answer. We therefore introduce IdMAT: a new teacher formalism answering queries with respect to any language in the target class, all at once. Such a teacher—tailored towards invariant synthesis—might provide incomplete “don’t know” answers, but also inductive facts of the form “if w1 is accepted, so is w2 ”. We pair IdMAT with a novel AAL algorithm LIndA that 1. encodes all uncertainties as a unique SAT instance and does not fork, 2. leverages incremental SAT solving and UNSAT core analysis, and 3. handles counterexamples—of the simple or inductive type—in a frugal manner inspired by the Rivest-Schapire refinement technique.

Kleinberg and Mullainathan showed that language generation in the limit is always possible at the level of computability: given enough positive examples, a learner can eventually generate data indistinguishable from a target language. However, such existence results do not address feasibility. We study the sample complexity of language generation in the limit for several canonical classes of formal languages. Our results show that infeasibility already appears for context-free and regular languages, and persists even for strict subclasses such as locally threshold testable languages, as well as for incomparable classes such as non-erasing pattern languages, a well-studied class in the theory of language identification. Overall, our results establish a clear gap between the theoretical possibility of language generation in the limit and its computational feasibility.

https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.4

Abstract: We discuss the inner workings of "ltlfsynt", the winner of the LTLf track of SyntComp'25, the reactive synthesis competition. This tool is based on a direct and incremental transformation of an LTLf formula into a DFA represented using Multi-Terminal Binary Decision Diagrams (MTBDD). The MTBDD-based DFA is then interpreted as a 2-player reachability game that is solved on-the-fly during its construction.

Additionally, we discuss two extensions.

First, a fragment of LTL called "syntactic obligations" (Boolean combinations of safety and co-safety formulas) can be used for reactive synthesis using a very similar approach. This time, syntactic obligations are translated to deterministic weak ω-automata represented using MTBDDs, and the on-the-fly game solving uses a weak objective.

Second, both approaches can easily be extended to support existential or universal quantifications of some atomic propositions. Using universal quantification, our tool supports synthesis under partial observation, i.e., some of the input signals cannot be observed by the controller.

Slides

We introduce automata over a particular type of structured data, namely an alphabet which is given as a (finite or infinite) directed graph. This constrains concatenation: two strings may only be concatenated if the end vertex of the first is equal to the start vertex of the second.

We develop the beginnings of an automata theory for languages on graph alphabets. We show that they admit a Kleene theorem, relating rational and regular languages, and a Myhill-Nerode theorem, stating that languages are regular iff they have finite prefix or, equivalently, suffix quotient. We present determinization and minimization algorithms, but we also exhibit that regular languages are not stable by complementation.

There is nothing surprising about our results, except maybe for the fact that all standard constructions still work. I'll also hint at generalizations to alphabets which are presimplicial sets and to directed hypergraphs.

Joint work with Hugo Bazille, see https://arxiv.org/abs/2602.10036.