On Temporal ASP with Eager Unfoldable Operators
Authors: Thomas Eiter, Davide Soldà
IJCAI 2025 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | We address this limitation by introducing eager temporal operators (eager Until, eager Release, etc.), and present non-disjunctive temporal programs (NDTP) as a framework for modeling dependencies, inertia, and non-determinism. The fragment of tight temporal programs (TTP), which can be recognized efficiently based on automata techniques for loop detections, guarantees polynomial encodability into LTL. Practical examples, such as request-grant protocols and user permissions in distributed systems, illustrate the applicability of our approach. Theorem 1. Deciding TEL-satisfiabilty of a formula ϕ in which eager operators occur is EXPSPACE-complete. Theorem 4. Deciding whether an NDTP program π is TEL-satisfiable is in EXPTIME. |
| Researcher Affiliation | Academia | Thomas Eiter , Davide Sold a Institute of Logic and Computation Vienna University of Technology (TU Wien), Vienna, Austria EMAIL |
| Pseudocode | No | The paper describes theoretical concepts, definitions, and theorems related to Temporal Equilibrium Logic and new temporal operators. It does not include any specific section or figure explicitly labeled as 'Pseudocode' or 'Algorithm'. |
| Open Source Code | No | Future work will be devoted to implementation and application of the results for monitoring, as well studying possible restrictions and extensions of the program classes introduced. |
| Open Datasets | No | The paper introduces a theoretical framework and illustrates concepts with practical examples (e.g., 'Example 1 (Liveness property)', 'Example 2 (Safety property)'). It does not mention the use or provision of any specific publicly available datasets. |
| Dataset Splits | No | The paper is theoretical and does not involve experiments on specific datasets, therefore, no dataset split information is provided. |
| Hardware Specification | No | The paper is theoretical and focuses on logical frameworks and complexity analysis. It does not describe any experiments requiring specific hardware, thus no hardware specifications are provided. |
| Software Dependencies | No | The paper mentions 'LTL-based model checkers such as SPIN [Holzmann, 1997], nuXmv [Cavada et al., 2014], and BLACK [Geatti et al., 2021]' as potential tools to leverage their results. However, it does not specify any software dependencies with version numbers for the development or execution of the work described in the paper itself. |
| Experiment Setup | No | The paper is theoretical, presenting new logical operators, program fragments, and complexity results. It does not describe any empirical experiments, and therefore, no specific experimental setup details or hyperparameters are provided. |