On the Complexity of Model Checking for Temporal Equilibrium Logic

Research output: Contribution to book/Conference proceedings/Anthology/Report › Conference contribution › Contributed › peer-review

Contributors

Abstract

Given an interpretation and a formula written in a logic , the problem of model checking (MC) for is the problem of determining whether is a model of . In this work, the computational complexity of MC for temporal equilibrium logic (TEL), a temporal extension of ASP, is investigated. The complexity of the universal and the existential variant of MC for TEL over Kripke structures, and of MC over linear traces, is determined. The complexity of these problems when the set of temporal operators, the temporal height or the implication height of the input formula is restricted is also determined.

Details

Original languageEnglish
Title of host publicationLogic Programming and Nonmonotonic Reasoning
PublisherSpringer Nature Switzerland
Pages67-82
Number of pages16
ISBN (electronic)978-3-032-38320-4
ISBN (print)978-3-032-38319-8
Publication statusPublished - 11 Oct 2026
Peer-reviewedYes

Publication series

SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume16952
ISSN0302-9743

External IDs

ORCID /0009-0005-9257-8217/work/230753027