Monitoring Arithmetic Temporal Properties on Finite Traces
Authors: Paolo Felli, Marco Montali, Fabio Patrizi, Sarah Winkler
AAAI 2023 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Feasibility is witnessed by a prototype implementation. We implemented our approach in a prototype, whose source code and web interface are available via https://monitoring.adatool.net. |
| Researcher Affiliation | Academia | 1Universit a di Bologna Bologna Italy 2Free University of Bozen-Bolzano Bolzano Italy 3Sapienza Universit a di Roma Rome Italy |
| Pseudocode | Yes | 1: procedure MONITOR(ψ, τ) 2: compute ψback and Dψback or take from cache 3: w word in ΘcurΘ consistent with τ 4: P state in Dψback such that {q0} w P 5: G CGψ(P, ) or take from cache 6: αn last assignment in τ 7: if P accepting in Dψback then 8: return (CS if αn |= FUNS(G) else PS) 9: else return (CV if αn |= FSAT(G) else PV) |
| Open Source Code | Yes | We implemented our approach in a prototype, whose source code and web interface are available via https://monitoring.adatool.net. |
| Open Datasets | No | The paper discusses theoretical concepts and a prototype implementation. It does not mention using any publicly available datasets for training, validation, or testing, nor does it provide access to a newly created dataset. |
| Dataset Splits | No | The paper does not mention any training/validation/test dataset splits or cross-validation setups. |
| Hardware Specification | No | The paper states that a prototype was implemented but does not specify any hardware details (e.g., CPU, GPU, memory) used for its implementation or any experiments. |
| Software Dependencies | No | The tool is implemented in Python, using Z3 (de Moura and Bjørner 2008) and CVC5 (Deters et al. 2014) for SMT checks and quantifier elimination. However, specific version numbers for Python, Z3, or CVC5 are not provided. |
| Experiment Setup | No | The paper focuses on the theoretical underpinnings and a prototype demonstration. It does not provide specific experimental setup details such as hyperparameter values, training configurations, or system-level settings for quantitative experiments. |