Abstract The synthesis of systems from formal specifications is a fundamental problem in symbolic AI and formal methods where the goal is to automatically construct implementations that meet desired requirements. In practice, specifications often include both hard constraints (critical requirements) and soft constraints (desirable properties). However, when specifications are unrealizable (due to conflicts between requirements) traditional synthesis methods fail to provide meaningful implementations or guidance. This problem has been addressed with maximum realizability , a framework for synthesizing systems that satisfy hard constraints while maximizing the satisfaction of soft constraints. However, the literature only solves this technique for classic discrete Linear Temporal Logic (LTL), whereas its extension to richer LTL modulo theories ( $$LTL _{\mathcal {T}} $$ L T L T ) remains unexplored. In this paper, we bridge this gap and we propose two approaches: (1) a method based on exhaustively traversing a set of abstractions and (2) an alternative method that incrementally refines abstractions during synthesis. Additionally, (3) we introduce lattice-based optimization techniques to further improve scalability by pruning uninteresting combinations of soft constraints. Our methods are evaluated on benchmarks from synthesis competitions and practical case studies, demonstrating their scalability and effectiveness.

Automated logic circuit design enhances chip performance, energy efficiency, and reliability, with applications in model-checking, reactive synthesis, and hyperproperty verification. AIGER circuits are a standard format for these domains, used in hardware model-checking, synthesis competitions such as Syntcomp, symbolic synthesis algorithms, and the verification of security properties in neural networks and safety-critical systems. Traditionally, AIGER circuits are generated from Linear Temporal Logic (LTL) specifications through complex pipelines, such as translating LTL to SMV or to automata and then to AIGER. These pipelines guarantee functional equivalence but produce large circuits with auto-generated labels that obscure the specification’s meaning. In applications like symbolic reactive synthesis, model-checking, and neural network verification, understanding latches and outputs is critical for debugging and tool improvement. In this tool paper, we introduce AIGLE, a novel tool that generates compact AIGER circuits directly from LTL[X] or Past-LTL specifications. Our approach uses linear-size translation from LTL[X] to Past-LTL, which produces highly legible circuits. Compared to tools like py-aiger, our tool reduces gate counts-—often by thousands-— improving readability and synthesis speed. Our empirical evaluation demonstrates smaller, more understandable circuits and faster synthesis, offering a scalable, engineer-friendly solution for formal methods applications.

Large language models (LLMs) are increasingly used to control embodied agents by mapping natural-language commands to high-level actions. While this paradigm enables flexible human-robot interaction, it also introduces significant safety risks, as LLM-generated commands are not guaranteed to respect physical, environmental, or mission-critical constraints. In this paper, we present an application of reactive synthesis modulo theories to the real-time guardrailing of an LLM-controlled quadruped robot, using the first-order theory of bitvectors as a symbolic abstraction of the robot's action space and environment. Our system translates natural-language commands into discrete bitvector-encoded actions, which are then filtered by a formally synthesized guardrail (also called shield) that enforces safety and liveness properties expressed in Linear Temporal Logic modulo bitvector constraints. The shield operates online and corrects unsafe commands while preserving the intent of the human operator. We instantiate our framework in a realistic locomotion setting, inspired by recent work on language-driven robot control, and demonstrate that the robot maintains safety under adversarial and dynamic environmental conditions. This work illustrates how theory-aware synthesis can serve as a practical foundation for trustworthy human--robot interaction, enabling the deployment of learning-based controllers in safety-critical settings with formal guarantees.

In recent years, Machine Learning (ML) models have achieved remarkable success in various domains. However, these models also tend to demonstrate unsafe behaviors, precluding their deployment in safety-critical systems. To cope with this issue, ample research focuses on developing methods that guarantee the safe behaviour of a given ML model. A prominent example is shielding which incorporates an ex- ternal component (a “shield”) that blocks unwanted behavior. Despite significant progress, shielding suffers from a main setback: it is currently geared towards properties encoded solely in propositional logics (e.g., LTL) and is unsuitable for richer logics. This, in turn, limits the widespread applicability of shielding in many real-world systems. In this work, we address this gap, and extend shielding to LTL modulo theories, by building upon recent advances in reactive synthesis modulo theories. This allowed us to develop a novel approach for generating shields conforming to complex safety specifications in these more expressive, logics. We evaluated our shields and demonstrate their ability to handle rich data with temporal dynamics. To the best of our knowledge, this is the first approach for synthesizing shields for such expressivity.

Abstract Reactive synthesis is the process of automatically generating a correct system from a given temporal specification. In this paper, we address the problem of reactive synthesis for LTL modulo theories ( $$\textrm{LTL}^{\mathcal {T}}$$ LTL T ), which extends LTL with literals from a first-order theory and allows relating the values of data across time . This logic allows describing complex dynamics both for the system and for the environment—such as a numeric variable increasing monotonically over time. The logic also allows defining relations (and not only assignment) between variables, enabling permissive shielding. We propose a sound algorithm called Counter-Example Guided Reactive Synthesis modulo theories (CEGRES), whose core is the novel concept of reactive tautology , which are valid temporal formulas that preserve the semantics of the specification but make the algorithm conclusive. Although realizability for full $$\textrm{LTL}^{\mathcal {T}} $$ LTL T is undecidable in general, we prove that CEGRES is terminating for some important theories and for arbitrary theories when specifications do not fetch data across time. We include an empirical evaluation that shows that CEGRES can solve many reactive synthesis problems of practical interest.

Safe Reinforcement Learning focuses on developing optimal policies while ensuring safety. A popular method to address such task is shielding, in which a correct-by-construction safety component is synthetised from logical specifications. Recently, shield synthesis has been extended to infinite-state domains, such as continuous environments. This makes shielding more applicable to realistic scenarios. However, often shields might be unrealizable because the specification is inconsistent. In order to address this gap, we present a method to obtain simple unconditional and conditional explanations that witness unrealizability, which goes by temporal formula unrolling: bounded strategy search. In this paper, we show different variants of the technique as well as its applicability

Reactive synthesis is the process of generate correct con- trollers from temporal logic specifications. Typically, synthesis is restricted to Boolean specifications in LTL. Recently, a Boolean abstraction technique allows to translate LTLT specifications that contain literals in theories into equi-realizable LTL specifications, but no full synthesis procedure exists yet. In synthesis modulo theories, the system receives valuations of environment variables (from a first-order theory T ) and outputs valuations of system variables from T . In this paper, we address how to syntheize a full controller using a combination of the static Boolean controller obtained from the Booleanized LTL specification together with on-the-fly queries to a solver that produces models of satisfiable existential T formulae. This is the first synthesis method for LTL modulo theories. Additionally, our method can produce adaptive responses which increases explainability and can improve runtime properties like performance. Our approach is applicable to both LTL modulo theories and LTLf modulo theories.

Abstract In this paper, we address the problem of the (reactive) realizability of specifications of theories richer than Booleans, including arithmetic theories. Our approach transforms theory specifications into purely Boolean specifications by (1) substituting theory literals by Boolean variables, and (2) computing an additional Boolean requirement that captures the dependencies between the new variables imposed by the literals. The resulting specification can be passed to existing Boolean off-the-shelf realizability tools, and is realizable if and only if the original specification is realizable. The first contribution is a brute-force version of our method, which requires a number of SMT queries that is doubly exponential in the number of input literals. Then, we present a faster method that exploits a nested encoding of the search for the extra requirement and uses SAT solving for faster traversing the search space and uses SMT queries internally. Another contribution is a prototype in Z3-Python. Finally, we report an empirical evaluation using specifications inspired in real industrial cases. To the best of our knowledge, this is the first method that succeeds in non-Boolean LTL realizability.