On Temporal ASP with Eager Unfoldable Operators

On Temporal ASP with Eager Unfoldable Operators

Thomas Eiter, Davide Soldà

Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence
Main Track. Pages 4473-4481. https://doi.org/10.24963/ijcai.2025/498

Temporal Equilibrium Logic (TEL) extends Answer Set Programming (ASP) with linear-time temporal operators (LTL), enabling reasoning about dynamic systems. However, TEL enforces strong minimization criteria that may preclude intuitive models. Liveness formulas, for instance, tend to fail to have infinite equilibrium models, as TEL minimization postpones satisfaction forever. 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.
Keywords:
Knowledge Representation and Reasoning: KRR: Knowledge representation languages
Knowledge Representation and Reasoning: KRR: Logic programming
Knowledge Representation and Reasoning: KRR: Non-monotonic reasoning