PhD in Coupled Reactive Synthesis Modulo TheoriesThe overall goal of the project is to develop scalable algorithmsfor reactive synthesis modulo theories by coupling automata-theoreticgame solving with on-demand theory reasoning.An important area of formal methods is the synthesis of controllersfor critical systems modeled using temporal logic over rich data.In the modulo theories setting, the plant is described by logicaltheories (e.G., linear arithmetic over signals) rather than purelyBoolean variables, and the goal is to compute a strategy thatsatisfies an LTL specification for all behaviors of the environment.From the practitioner’s point of view, it is crucial that problemsin the software requirement phase are uncovered as early as possible,which requires synthesis algorithms that scale to realistic plantmodels.Previous algorithms for solving reactive synthesis modulo theoriesfollow one of two paradigms. Either the theories are eagerlyeliminated through Boolean abstractions, to which standard automata-and game-based synthesis is then applied,



or a counterexample-guidedabstraction refinement loop is used, iteratively refining theabstraction until a solution or a disproof of realizability is found(e.G., CEGRES). Both paradigms decouple theory reasoning from gamesolving: eager abstraction discards precision upfront and can lead tocombinatorial explosion, while refinement repeatedly solves games onabstractions that may be irrelevant to the final strategy.This PhD proposes a third intermediate approach to synthesis modulotheories, analogous to lazy SMT solving, which we have called coupledreactive synthesis modulo theories. Instead of abstracting the formulaupfront, theory reasoning is performed during game solving: the gamealgorithm issues targeted queries to a theory solver only when itneeds to reason about successors exploration, so that theory precisionis spent only on the parts of the exploration that are relevant to thespecification.The student will investigate

📌 Phd In Coupled Reactive Synthesis Modulo Theories (Madrid)
🏢 IMDEA Software Institute
📍 Madrid