Computational Aspects of Progression for Temporal Equilibrium Logic

Computational Aspects of Progression for Temporal Equilibrium Logic

Thomas Eiter, Davide Soldà

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence
Main Track. Pages 3342-3350. https://doi.org/10.24963/ijcai.2024/370

Temporal logic plays a crucial role in specifying and reasoning about dynamic systems, where temporal constraints and properties to be monitored are essential. Traditional approaches like LTL-monitoring assume monotonicity, which limits their applicability to scenarios involving non-monotonic temporal properties. 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.
Keywords:
Knowledge Representation and Reasoning: KRR: Computational complexity of reasoning
Knowledge Representation and Reasoning: KRR: Logic programming
Knowledge Representation and Reasoning: KRR: Non-monotonic reasoning
Agent-based and Multi-agent Systems: MAS: Formal verification, validation and synthesis