On the Complexity of Model Checking for Temporal Equilibrium Logic

Vortrag von Oscar Barreca

Veranstaltungsort: APB 3027
Beginn: 10. Dezember 2026 um 11:00
Ende: 10. Dezember 2026 um 12:00
Forschungsgruppe: Automatentheorie
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 presented at Logic Programming and Nonmonotonic Reasoning (LPNMR) 26 in Klagenfurt, Austria, on September 2026.