Shield Synthesis for LTL Modulo Theories
Authors: Andoni Rodríguez, Guy Amir, Davide Corsi, César Sánchez, Guy Katz
AAAI 2025 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We evaluated our shields and demonstrate their ability to handle rich data with temporal dynamics. To the best of our knowledge, this is the first approach for synthesizing shields for such expressivity. [...] We compared our work with theirs: for the 13 different specifications from (Wu et al. 2019), we generated our shield and measured time for computing: (i) the Boolean step (clm. B), and (ii) producing the final output (clm. T ). We compared our results at Tab. 1. For the first task, our approach, on average, requires less than 0.21µs, while they take more than twice as long on average (with over 0.47µs). Our approach was also more efficient in the second task, taking on average about 0.157ms, whereas they take required 0.557ms on average. [...] Tab. 1 shows that our approach can manage both rich data and temporal dynamics. |
| Researcher Affiliation | Academia | 1 IMDEA Software Institute, Spain 2 Universidad Polit ecnica de Madrid, Spain 3 Cornell University, USA 4 University of California, Irvine, USA 5 The Hebrew University of Jerusalem, Israel EMAIL, EMAIL, EMAIL, EMAIL, EMAIL |
| Pseudocode | No | The paper describes methods with numbered steps and uses block diagrams (Figure 1) to illustrate architectures, but it does not contain any explicitly labeled 'Pseudocode' or 'Algorithm' blocks. |
| Open Source Code | No | See the extended version of this paper (Rodriguez et al. 2024) for a for additional details. [...] Rodriguez, A.; Amir, G.; Corsi, D.; Sanchez, C.; and Katz, G. 2024. Shield Synthesis for LTL Modulo Theories . Technical Report. https://arxiv.org/abs/2406.04184. The paper provides a link to an arXiv technical report for an extended version but does not provide a direct link to source code or explicitly state that the code for the described methodology is being released. |
| Open Datasets | No | The paper does not mention using any specific publicly available datasets for its evaluation or experiments. It discusses applying the methods to |
| Dataset Splits | No | The paper does not mention using any specific datasets or providing details about how data was split into training, validation, or test sets. The evaluation focuses on performance metrics (time measurements) against theoretical components rather than data-driven empirical results. |
| Hardware Specification | No | The paper discusses measurement times (e.g., 0.21µs, 0.157ms) for different tasks in Table 1 but does not specify any hardware components (e.g., CPU, GPU models, memory, or cloud resources) used to obtain these measurements. |
| Software Dependencies | No | The paper mentions several tools and solvers, such as 'Z3 with optimization (Bjørner, Phan, and Fleckenstein 2015)' and 'Strix (Meyer, Sickert, and Luttenberger 2018)', but it does not specify the version numbers of these or any other software dependencies used in their implementation. |
| Experiment Setup | No | The paper presents theoretical developments and an empirical evaluation focusing on performance time for different synthesis steps. However, it does not provide specific experimental setup details such as hyperparameters, model architectures, training configurations, or other system-level settings relevant for reproduction. |