{rfName}
Pr

Indexat a

Llicència i ús

Citacions

Altmetrics

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.

Anàlisi d'autories institucional

Rodriguez, AndoniAutor (correspondència)

Compartir

29 d’abril de 2025
Publicacions
>
Reunió
No

Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis

Publicat a:Lecture Notes In Computer Science. 15055 28-50 - 2025-01-01 15055(), DOI: 10.1007/978-3-031-78750-8_2

Autors: Rodriguez, Andoni; Gorostiaga, Felipe; Sanchez, Cesar

Afiliacions

CIFASIS, Rosario, Argentina - Autor o coautor
IMDEA Software Inst, Madrid, Spain - Autor o coautor
Univ Politecn Madrid, Madrid, Spain - Autor o coautor

Resum

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).

Paraules clau

Administração pública e de empresas, ciências contábeis e turismoAdministração, ciências contábeis e turismoArquitetura e urbanismoArquitetura, urbanismo e designArtesAstronomia / físicaBiodiversidadeBiotecnologíaCiência da computaçãoCiências agrárias iCiências ambientaisCiências biológicas iCiências biológicas iiCiências biológicas iiiCiências sociais aplicadas iComputer science (all)Computer science (miscellaneous)Computer science, artificial intelligenceComputer science, theory & methodsComunicação e informaçãoComunicació i informacióDireitoEducaçãoEducação físicaEngenharias iEngenharias iiEngenharias iiiEngenharias ivEnsinoFarmaciaGeneral computer scienceGeneral o multidisciplinarGeociênciasGeografíaInterdisciplinarLinguística e literaturaMatemática / probabilidade e estatísticaMateriaisMedicina iMedicina iiMedicina iiiMedicina veterinariaOdontologíaPlanejamento urbano e regional / demografiaPsicologíaQuímicaSaúde coletivaTheoretical computer science

Indicis de qualitat

Impacte bibliomètric. Anàlisi de la contribució i canal de difusió

El treball ha estat publicat a la revista Lecture Notes In Computer Science a causa de la seva progressió i el bon impacte que ha aconseguit en els últims anys, segons l'agència WoS (JCR), s'ha convertit en una referència en el seu camp. A l'any de publicació del treball, 2025, es trobava a la posició 13/61, aconseguint així situar-se com a revista Q1 (Primer Cuartil), en la categoria Computer Science, Theory & Methods. Destacable, igualment, el fet que la revista està posicionada per sobre del Percentil 90.

Anàlisi del lideratge dels autors institucionals

Aquest treball s'ha realitzat amb col·laboració internacional, concretament amb investigadors de: Argentina.

Hi ha un lideratge significatiu, ja que alguns dels autors pertanyents a la institució apareixen com a primer o últim signant, es pot apreciar en el detall: Primer Autor (RODRÍGUEZ HERRERO, ANDONI) .

l'autor responsable d'establir les tasques de correspondència ha estat RODRÍGUEZ HERRERO, ANDONI.