Indexed in
License and use
Citations
Grant support
This work was funded in part by PRODIGY Project (TED2021-132464BI00)-funded by MCIN/AEI/10.13039/501100011033/and the European Union NextGenerationEU/PRTR-by the DECO Project (PID2022-138072OB-I00)-funded by MCIN/AEI/10.13039/501100011033 and by the ESF, as well as by a research grant from Nomadic Labs and the Tezos Foundation.
Analysis of institutional authors
Rodriguez, AndoniCorresponding AuthorPredictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis
Publicated to:Lecture Notes In Computer Science. 15055 28-50 - 2025-01-01 15055(), DOI: 10.1007/978-3-031-78750-8_2
Authors: Rodriguez, Andoni; Gorostiaga, Felipe; Sanchez, Cesar
Affiliations
Abstract
Reactive synthesis is the process of generating correct controllers from temporal logic specifications. Classical LTL reactive synthesis handles (propositional) LTL as a specification language. Boolean abstractions allow reducing LTLT specifications (i.e., LTL with propositions replaced by literals from a theory T), into equi-realizable LTL specifications. In this paper we extend these results into a full static synthesis procedure. The synthesized system receives from the environment valuations of variables from a rich theory T and outputs valuations of system variables from T. We use the abstraction method to synthesize a reactive Boolean controller from the LTL specification, and we combine it with functional synthesis to obtain a static controller for the original LTLT specification. We also show that our method allows adaptive responses in the sense that the controller can optimize its outputs in order to e.g., always provide the smallest safe values. This is the first full static synthesis method for LTLT, which is a deterministic program (hence predictable and efficient).
Keywords
Quality index
Bibliometric impact. Analysis of the contribution and dissemination channel
The work has been published in the journal Lecture Notes In Computer Science due to its progression and the good impact it has achieved in recent years, according to the agency WoS (JCR), it has become a reference in its field. In the year of publication of the work, 2025, it was in position 70/78, thus managing to position itself as a Q1 (Primer Cuartil), in the category Computer Science, Artificial Intelligence. Notably, the journal is positioned above the 90th percentile.
Leadership analysis of institutional authors
This work has been carried out with international collaboration, specifically with researchers from: Argentina.
There is a significant leadership presence as some of the institution’s authors appear as the first or last signer, detailed as follows: First Author (RODRÍGUEZ HERRERO, ANDONI) .
the author responsible for correspondence tasks has been RODRÍGUEZ HERRERO, ANDONI.