A SAT-based Efficient Method for the Synthesis from numerical LTL spefications





Publicado en

Actas de las XXI Jornadas de Programación y Lenguajes (PROLE 2022)


CC BY 4.0


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.


Acerca de Rodriguez, Andoni

Palabras clave

Boolean Abstraction, Formal Methods, Formal Specification, Formal Verification, Reactive Systems, Realizability, SAT Solving, SMT Solving, Synthesis
Página completa del ítem
Notificar un error en este artículo
Mostrar cita
Mostrar cita en BibTeX
Descargar cita en BibTeX