On the complexity of Temporal Equilibrium Logic

TL;DR

This paper analyzes the computational complexity of checking the existence of models in Temporal Equilibrium Logic, revealing tight bounds and exploring subclasses, with implications for understanding LTL satisfiability.

Contribution

It provides the first matching lower bound for TEL model existence complexity and analyzes subclasses, offering new insights into LTL satisfiability over finite and infinite words.

Findings

Established EXPSPACE lower bound for TEL model existence

Identified tractable and intractable subclasses of TEL

Highlighted differences in LTL satisfiability over finite and infinite models

Abstract

Temporal Equilibrium Logic (TEL) is a promising framework that extends the knowledge representation and reasoning capabilities of Answer Set Programming with temporal operators in the style of LTL. To our knowledge it is the first nonmonotonic logic that accommodates fully the syntax of a standard temporal logic (specifically LTL) without requiring further constructions. This paper provides a systematic complexity analysis for the (consistency) problem of checking the existence of a temporal equilibrium model of a TEL formula. It was previously shown that this problem in the general case lies somewhere between PSPACE and EXPSPACE. Here we establish a lower bound matching the known EXPSPACE upper bound. Additionally we analyse the complexity for various natural subclasses of TEL formulas, identifying both tractable and intractable fragments. Finally the paper offers some new insights on the logic LTL by addressing satisfiability for minimal LTL models. The complexity results obtained highlight a substantial difference between interpreting LTL over finite or infinite words.