Computational Aspects of Progression for Temporal Equilibrium Logic
Authors: Thomas Eiter, Davide Soldà
IJCAI 2024 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | We delve into complexity aspects of monitoring temporal specifications using non-monotonic Temporal Equilibrium Logic (TEL), a temporal extension of Answer Set Programming defined over Temporal Here and There Logic (THT) with a minimality criterion enforcing stable models. Notably, we study the complexity gap between monitoring properties in THT and TEL semantics, and the complexity of monitoring approximations based on progression, which is widely used in verification and in AI. In that, we pay particular attention to the fragment of temporal logic programs. While [Soldà et al., 2023] presented the approach and an algorithm for TASP progression, computational aspects such as complexity and tractability, which in an online setting is desired, were not addressed. We fill this gap with the following contributions: We characterize the complexity of monitoring under TEL3 and THT3 semantics, showing that they are like TEL and THT EXPSPACE-complete and PSPACE-complete, respectively. |
| Researcher Affiliation | Academia | Thomas Eiter and Davide Soldà Institute for Logic and Computation, TU Wien, Favoritenstraße 9 11, 1040 Vienna, Austria, eiter@kr.tuwien.ac.at, davide.solda@tuwien.ac.at |
| Pseudocode | No | The paper provides definitions for progression functions (e.g., Definition 5, Definition 8, Definition 9) and describes their operations, but it does not present them in a structured pseudocode block or algorithm format. |
| Open Source Code | No | The paper mentions existing solvers and tools (e.g., 'telingo', 'oclingo', 'ticker', 'STe LP', 'Me Teo R') but does not state that the authors' own implementation of the proposed progression methods is open-source or provide a link to their code. |
| Open Datasets | No | The paper is theoretical and does not describe experiments using specific datasets. Therefore, no information about public dataset availability is provided. |
| Dataset Splits | No | The paper is theoretical and does not describe experiments using specific datasets. Therefore, no information about training/validation/test splits is provided. |
| Hardware Specification | No | The paper is theoretical and does not describe running experiments that would require specific hardware. Therefore, no hardware specifications are mentioned. |
| Software Dependencies | No | The paper is theoretical and focuses on logical frameworks and complexity analysis. While it mentions various existing tools and solvers (e.g., 'telingo', 'clingo'), it does not specify software dependencies with version numbers required to replicate any experiments of its own. |
| Experiment Setup | No | The paper is theoretical and does not describe conducting experiments with specific setups or hyperparameters. |