On the complexity of temporal equilibrium logic

DOI10.1109/LICS.2015.65MaRDI QIDQ4635843zbMATH OpenOpenAlexWikidataFDO

Authors

Publication date 23 April 2018

Published in 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1503.00043

Mathematics Subject Classification ID

Temporal logic (03B44) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60)

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.

Recommendations

• On the expressiveness of temporal equilibrium logic
• Automata-Based Computation of Temporal Equilibrium Models
• A normal form for linear temporal equilibrium logic
• Temporal Equilibrium Logic: A First Approach
• An infinitary encoding of temporal equilibrium logic

Cited in

(15)

• Metabolic pathways as temporal logic programs
• On the expressiveness of temporal equilibrium logic
• Loop formulas for splitable temporal logic programs
• Stable Models for Temporal Theories
• Temporal equilibrium logic: a survey
• Temporal equilibrium logic with past operators
• An infinitary encoding of temporal equilibrium logic
• Temporal logic programs with variables
• Asymptotic behaviour in temporal logic
• A normal form for linear temporal equilibrium logic
• Temporal ASP: from logical foundations to practical use with \texttt{telingo}
• The complexity of temporal logic over the reals
• Gödel-Dummett linear temporal logic
• The stable model semantics of Datalog with metric temporal operators
• Linear-time temporal answer set programming

This page was built for publication: On the complexity of temporal equilibrium logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635843)