Anzeige
Erschienen in:
2011 | OriginalPaper | Buchkapitel
Loop Formulas for Splitable Temporal Logic Programs
verfasst von : Felicidad Aguado, Pedro Cabalar, Gilberto Pérez, Concepción Vidal
Erschienen in: Logic Programming and Nonmonotonic Reasoning
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
In this paper, we study a method for computing
temporal equilibrium models
, a generalisation of stable models for logic programs with temporal operators, as in Linear Temporal Logic (LTL). To this aim, we focus on a syntactic subclass of these temporal logic programs called
splitable
and whose main property is satisfying a kind of “future projected” dependence present in most dynamic scenarios in Answer Set Programming (ASP). Informally speaking, this property can be expressed as “past does not depend on the future.” We show that for this syntactic class, temporal equilibrium models can be captured by an LTL formula, that results from the combination of two well-known techniques in ASP: splitting and loop formulas. As a result, an LTL model checker can be used to obtain the temporal equilibrium models of the program.