On the Complexity of Model Checking for Temporal Equilibrium Logic

Talk by Oscar Barreca

Location: APB 3027
Start: 10. December 2026 at 11:00 am
End: 10. December 2026 at 12:00 pm
Research group: Automata Theory
Event series: Research Seminar Logic and AI
iCal

This talk presents the results obtained while studying the computational complexity of the model checking (MC) problem for temporal equilibrium logic (TEL), a temporal extension of answer set programming (ASP) introduced by Pedro Cabalar and Gilberto Pérez Vega in 2007.

Given a Kripke structure (KS) 𝐾 and a TEL formula 𝜑, the MC problem for TEL (Telks) is the problem of deciding whether 𝐾 is a temporal equilibrium model (TEM) of 𝜑. The obtained complexity results justify a division of this problem into two variants: a universal one (Telks∀) asking whether all traces 𝑇 within 𝐾 are a TEM of 𝜑; and an existential one (Telks∃) asking whether a trace 𝑇 within 𝐾 exists which is a TEM of 𝜑.

A restriction of the Telks problem over linear KSs (Telt), corresponding to asking whether a periodically infinite LTL trace is a TEM of a given TEL formula 𝜑, is also investigated. The complexity of the Telks∀, Telks∃ and Telt problems when the set of allowed temporal operators, the temporal height (the number of nested temporal operators) and the implication height (the number of nested implication operators) of a formula is restricted is also presented.

The work this talk is based on was already presented at Logic Programming and Nonmonotonic Reasoning (LPNMR) 26 in Klagenfurt, Austria, on September 2026.