Autor:
Rodriguez, Andoni

Foto de perfil

E-mails conocidos

andoni.rodriguez@imdea.org

Fecha de nacimiento

Proyectos de investigación

Unidades organizativas

Puesto de trabajo

Apellidos

Rodriguez

Nombre de pila

Andoni

Nombre

Nombres alternativos

Afiliaciones conocidas

IMDEA Software Institute, Spain

Páginas web conocidas

Página completa del ítem
Notificar un error en este autor

Filtros

20231
Restablecer filtros

Ajustes

Tema: (Rich) Reactive Realizability × Tema: Boolean Abstraction × Autor: Sánchez, César ×

Resultados de la búsqueda

Mostrando 1 - 1 de 1
  • Miniatura
    Artículo
    On-the-fly reactive synthesis modulo theories
    Rodriguez, Andoni; Sánchez, César. Actas de las XXII Jornadas sobre Programación y Lenguajes (PROLE 2023), 2023-09-12.
    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).