ABSTRACT. Reactive synthesis is a challenging problem for two reasons: It is algorithmically hard, and writing formal specifications by hand is notoriously difficult. In this extended abstract, we report on current advances in tackling both sides of the problem with Large Reasoning Models (LRMs). On the algorithmic side, we present a neuro-symbolic approach that couples LRMs with model checkers to iteratively repair a synthesized Verilog implementation via sound symbolic feedback. Our approach solves more benchmark instances than last year's SYNTCOMP winner and extends to constructing parameterized systems. On the specification side, we introduce an autoformalization step that shifts the specification task from temporal logic to natural language and introduce a dataset of natural-language specifications for evaluation. We demonstrate performance comparable to that of starting from formal specifications, establishing natural synthesis as a viable end-to-end workflow.

ABSTRACT. Strategy synthesis typically follows an all-or-nothing paradigm, returning unrealisable whenever a specification cannot be guaranteed in an uncertain environment. In this paper, we introduce optimal LTLf synthesis, where the goal is to realise as many objectives as possible from a given specification consisting of multiple objectives, especially for the case that they are not all jointly realisable. We first consider max-guarantee synthesis, which commits to a maximal set of objectives that we can a priori guarantee to realise. We then introduce max-observation synthesis, which maximises a posteriori realised objectives that may be incomparable on different executions. Finally, we present incremental max-observation synthesis, which further improves strategies by exploiting opportunities for stronger guarantees when they arise during an execution. Experimental results show that different variations of optimal synthesis scale broadly equally well, solving a large fraction of the benchmark instances within the given timeout, demonstrating the practical feasibility of the approach.

ABSTRACT. We present a practical acceleration of recent quasipolynomial-time progress measure algorithms for parity games. For this, we combine a novel Strahler-universal tree encoding with data-parallel (SIMD) computation. Our key contribution is showing that common instances admit very small structural parameters, enabling compact representations that fit into SIMD registers. This insight allows us to redesign the core lifting (i.e. successor computation) step into a parallel form, yielding significant empirical speedups over existing implementations. This work demonstrates that bridging algorithmic structure (Strahler measures) with hardware-aware optimization (SIMD) can materially improve parity game solving.

ABSTRACT. Reactive synthesis with non-integer discounted-sum objectives is solved by Bansal et al. (AAAI 2022) via the DSLow comparator automaton, which under-approximates the running sum and reduces the problem to a Büchi game on the product of the arena and comparator. Their construction allocates the full product upfront and explores it by BFS, incurring two costs: many product states are structurally unreachable (ghost states), and BFS defers winning states behind a wide shallow frontier. We propose (1) a lazy on-the-fly construction that materializes only reachable states, and (2) a priority-guided exploration keyed on U − c (distance to comparator saturation) with interleaved backward propagation. On the standard benchmarks, our approach constructs 74– 99% fewer states and discovers the first winning state up to 22× faster, with identical winning regions. Weight-specific asymmetric comparator bounds additionally cut the theoretical state space by 40–50% at no cost.

ABSTRACT. We study the synthesis of policies for stochastic systems acting on behalf of multiple principals with heterogeneous time preferences. We model this setting using asymmetrically-discounted Markov decision processes (MDPs), where each principal possesses an individual reward function and discount factor. The objective is to synthesize policies maximizing a utilitarian notion of social welfare, defined as the aggregate discounted payoff across all principals. Heterogeneous discounting fundamentally changes the structure of optimal policies: in contrast to classical discounted MDPs, welfare-optimal policies are generally not positional, even when all principals receive identical rewards. Nevertheless, we establish that optimal policies admit a simple structure: pure finite-memory counting strategies suffice and can be synthesized in polynomial time under mild assumptions on the spacing of discount factors. We further show that restricting synthesis to stationary strategies leads to computational intractability: deciding whether there exists a stationary strategy achieving a given welfare threshold is NP-hard, even for two principals with identical rewards. Our results highlight how heterogeneous temporal preferences introduce new synthesis challenges at the intersection of formal methods, multi-agent planning, and algorithmic game theory.

ABSTRACT. This talk is based on two joint works with Pete Austin, Nicolas Mazzocchi, and Patrick Totzke published in FOSSACS 2024 and CONCUR 2025. Temporal graphs are graphs where the edge relation changes over time. This model has been used to analyse dynamic networks and distributed systems in dynamic topologies. We consider temporal graphs where the edge availability relation is given by an existential Presburger formula with a free variable such that an edge e is available at time t if and only if the formula evaluated with the free variable assigned value t is true. This allows succinct encoding of temporal graphs, while also capturing (ultimately) periodic temporal graphs. In this talk, we will consider the complexity of solving games played on (succinct) temporal graphs. In particular, our results show that reachability and parity games on temporal graphs are PSPACE-complete. In fact, the PSPACE-hardness also holds on 1-player temporal graphs. We also consider games with explorability objective, where one player tries to visit all the vertices of a graph. Explorability is a well studied topic in temporal graphs. We show that the game version of the explorability problem is PSPACE-complete even when the temporal graph is presented as a sequence of static graphs.

ABSTRACT. Given rationals α and β, the sure-almost-sure problem for an objective φ in a Markov decision process (MDP) asks if one can simultaneously ensure that all outcomes of the MDP have φ-value at least α (i.e., sure α satisfaction), and with probability 1 the outcome has φ-value at least β (i.e., almost-sure β satisfaction). The sure-limit-sure problem asks if for all ε > 0, one can simultaneously ensure that all outcomes have φ-value at least α, and with probability at least 1 − ε the outcome has φ-value at least β. Moreover, if simultaneous satisfaction of objectives is possible, then one would also like to construct a strategy (for sure-almost-sure) or a family of strategies (for sure-limit-sure) that achieves this. In this paper, we solve the sure-almost-sure and sure-limit-sure problems for window mean-payoff objectives. The window mean-payoff objective strengthens the standard mean-payoff objective by requiring that the average payoff of a finite window that slides over an infinite run be greater than a given threshold. We study two variants of window mean payoff; for both variants we show that sure-almost-sure problem and the sure-limit-sure problem are no harder than sure satisfaction and almost-sure satisfaction when considered separately for these objectives.

ABSTRACT. Identifying implicitly defined variables in a propositional formula and extracting their explicit definitions is useful for Boolean functional synthesis and related problems. This typically involves one SAT call per variable and constructing an interpolant from the resulting resolution proof. We propose extracting an entire set of n definitions from a single resolution refutation. A modification of a standard interpolation system computes interpolants under partial assignments, one per target variable. A single pass of the refutation then produces a multi-output circuit of size O(nm) for a proof of length m. Preliminary experiments on Boolean functional synthesis benchmarks show that the joint refutation is produced at least as fast as the per-variable sequence of proofs, but the multi-output circuits are typically larger. Closing this circuit-size gap is the main open question.

ABSTRACT. Boolean Functional Synthesis (BFnS) is the problem of synthesizing a Boolean function from a Boolean specification that describes a relation between input and output variables. Due to the many applications of BFnS, such as in circuit design, QBF solving, and reactive synthesis, efforts are continuously made to explore and better study BFnS. In this work we deepen our understanding of BFnS by analyzing underlying graph structures of BFnS instances. This is motivated by a chain of works on SAT instances, where analysis of graph features, such as graph modularity, is used to explore the performance of SAT solvers on industrial SAT instances. We first show that unlike instances that are random, industrial BFnS instances admit high modularity, even more than is common in SAT. Observing that, we construct a novel BFnS random instance generator with controlled modularity, which we use to study the effect of modularity on performance of state-of-the-art BFnS solvers. Finally we white-box these solvers to determine how the structure of generated instances changes iteratively through the solving process. Our findings indicate that instances modularity has a direct effect on the various solvers performance and their behavior.

ABSTRACT. Quantum circuit synthesis is the task of decomposing a given quantum operator into a sequence of elementary quantum gates. Since the finite target gate set cannot exactly implement any given operator, approximation is often necessary. Model counting, or #SAT, has recently been demonstrated as a promising new approach for tackling core problems in quantum circuit analysis. In this work, we show for the first time that the universal quantum circuit synthesis problem can be reduced to maximum model counting. We formulate a #SAT encoding for exact and approximate depth-optimal quantum circuit synthesis into the Clifford+T gate set. We evaluate our method with an open-source implementation that uses the maximum model counter d4Max as a backend. For this purpose, we extended d4Max with support for complex and negative weights to represent amplitudes. Experimental results show that existing classical tools have potential for the quantum circuit synthesis problem. https://arxiv.org/pdf/2508.00416

ABSTRACT. We propose a decoupled approach to synthesizing a word, letter by letter, that is in the conjunction of a given pair of regular objectives. A key application is multi-objective robotic path planning, where each letter corresponds to a robot action and the goal is to find a plan that satisfies both objectives. The traditional monolithic solution would construct the product automaton, and obtains a ``generator'' that outputs an accepting word. Instead, we synthesize two independent generators and compose them at runtime via an auction-based mechanism: at each time step, the generators bid for who chooses the next symbol. Advantages of this approach include design in parallel or by different vendors, and reusability, namely when an objective changes only the relevant generator is updated and the other is reused. We design, for the first time, a framework in which each generator is designed on a separate automaton, which enables specifying objectives as logical formulas. For cases in which a feasible solution is not found, we develop a successive refinement algorithm that searches for a pair of assumptions that regain feasibility. Weaker assumptions lead to increased modularity. Our algorithm is based on a novel automata-learning algorithm that can be of independent interest. We design proof-of-concept experiments where we implement our algorithm, and demonstrate the effectiveness.

ABSTRACT. History-deterministic automata are those in which nondeterministic choices can be correctly resolved stepwise: there is a strategy to select a continuation of a run given the next input letter so that if the overall input word admits some accepting run, then the constructed run is also accepting. Motivated by checking qualitative properties in probabilistic verification, we consider the setting where the resolver strategy can randomise and only needs to succeed with lower-bounded probability. We study the expressiveness of such stochastically-resolvable automata as well as consider the decision questions of whether a given automaton has this property. In particular, we show that it is undecidable to check if a given NFA is λ-stochastically resolvable. This problem is decidable for finitely-ambiguous automata. We also present complexity upper and lower bounds for several well-studied classes of automata for which this problem remains decidable.

ABSTRACT. Inductive program synthesis algorithms search a space of programs to find one that meets some specification. Enumerating according to the syntax of a programming language leads to a large search space, and hence slow synthesis, due in large part to semantic duplication. A synthesiser may have to evaluate—and reject—multiple semantically identical but syntactically different programs, wasting resources. To avoid this duplication, we present NSynC, a synthesis-by-semantics approach. By enumerating the semantics of the target language directly, we guarantee that each candidate program is semantically unique and that each evaluation of a candidate is meaningful. Specifically, we search the space of normal forms for the simply-typed lambda calculus with sums using a top-down, type-directed synthesis algorithm. Our preliminary results show a geomean speedup of 8.93x on a synthetic benchmark suite over the unrestricted algorithm.

ABSTRACT. Traditional type systems prevent basic errors but lack the expressiveness to handle logical errors or prove complex program properties. Refinement types address this by augmenting base types with decidable first-order logic constraints. However, writing them manually is difficult, which ultimately hinders their widespread adoption. Existing symbolic and data-driven inference approaches often struggle to scale to multi-function programs or rely heavily on manual annotations. In this work, we present a neurosymbolic approach for automated refinement type synthesis. Our methodology converts the refinement typing rules into a graphical representation and learns semantic representations via a Graph Neural Network (GNN). An autoregressive decoder model then synthesizes predicates, using Reinforcement Learning (RL) to navigate the search space while a type checker verifies candidates. However, a core challenge in this setting is the sparse-reward problem, where type checker feedback provides insufficient guidance for the RL agent. To address this, we introduce two main contributions. First, novel Behavioral Rewards utilizing subspecifications and semantic program slicing to provide partial rewards. Second, a data-driven, CEGAR-Guided Learning loop that refines reward signals based on incremental correctness. Together, these techniques generate denser rewards and accelerate convergence. Our implementation and initial evaluation demonstrates that the framework can synthesize semantically correct specifications for complex programs and properties.