Revisiting the specification decomposition for synthesis based on LTL solvers. - Josu Oca; Montserrat Hermo; Alexander Bolotov (CoRR, 2023)

A Sound and Complete Algorithm to Identify Independent Variables in a Reactive System Specification. - Josu Oca; Montserrat Hermo; Alexander Bolotov (DATE, 2024)

Towards an efficient implementation of a tableau method for reactive safety specifications. - Ander Alonso; Montserrat Hermo; Josu Oca (J. Log. Algebraic Methods Program., 2025)