On-the-fly reactive synthesis modulo theories





Publicado en

Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023)

Licencia Creative Commons


The Boolean abstraction technique translates (i.e., Booleanizes) an LTL modulo theories specification into an equi-realizable LTL specification. This solves the realizability modulo theories problem. However, synthesis modulo theories is a different problem: the system has to receive valuations in a first-order theory T and output valuations in T . In this work in progress, we address how to meet this need without a pure synthesis method, but solving ”synthesis” on-the-fly by synthetising a Boolean controller from the Booleanized LTL specification and shipping it with a method that provides models in satisfiable instances of existential formulae (e.g., an SMT solver).


Acerca de Rodriguez, Andoni

Palabras clave

LTL Modulo Theories, (Rich) Reactive Synthesis, (Rich) Reactive Realizability, Boolean Abstraction, SMT Solvers, Model Finding, Quantifier Elimination, On-the-fly Symbolic Computation
Página completa del ítem
Notificar un error en este artículo
Mostrar cita
Mostrar cita en BibTeX
Descargar cita en BibTeX