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

2022 - 20243
Restablecer filtros

Ajustes

Autor: Rodriguez, Andoni ×

Resultados de la búsqueda

Mostrando 1 - 3 de 3
  • Miniatura
    Artículo
    A SAT-based Efficient Method for the Synthesis from numerical LTL spefications
    Rodriguez, Andoni; Sánchez, César. Actas de las XXI Jornadas de Programación y Lenguajes (PROLE 2022), 2022-09-05.
    Reactive synthesis is the problem of automatically finding a system that satisfies a temporal logic specification, where the atomic propositions are split into those controlled by the system and those controlled by the environment. In this paper we address the problem of the reactive synthesis of specifications that use numerical variables. We consider an approach that transforms the arithmetic specification into a purely Boolean specification by substituting the arithmetic literals by Boolean variables, and computing an additional Boolean requirement that captures the dependencies between the new variables. The resulting specification can be passed to off-the-self Boolean synthesis tools, and is realizable if and only if the original arithmetic specification is. In this paper, we present a method to compute this equi-realizable Boolean specification based on a nested encoding of the search for such a specification using a SAT-solver (for efficiently encoding the search) and an SMT-solver (for checking the decision power of each player) iteratively.
  • 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).
  • Miniatura
    Artículo
    Unconditional Unrealizability Detection in Reactive Systems Modulo Theories
    Rodriguez, Andoni; Sánchez, César. Actas de las XXIII Jornadas de Programación y Lenguajes (PROLE 2024), 2024-06-17.
    Linear Temporal Logic modulo theories (LTLT ) extends LTL by allowing atomic propositions to be literals from the theory T . Realizability of an LTLT specification φ is proven to be decidable by a Boolean abstraction that generates an equi-realizable LTL specification from φ. This abstraction method also opens the door for a more thoughtful analysis of LTLT specifications. In this work in progress, we address how to produce informative traces of LTLT specifications by finding strategies of the players such that certain desired or undesired goals are reached. In particularly, we show how to produce unconditional unrealizability witnesses for an uncontrollable environment. We present two approaches based on unrollings of formulae: the first one characterizes the problem using SMT-with-quantifiers; the second one Booleanizes the LTLT formula and then uses QBF solving. We show the latter is faster and provides more termination guarantees. To the best of our knowledge, this is the first such specification analysis over such an expressive fragment of the logic.