Past-present temporal programs over finite traces

TL;DR

This paper explores a subclass of temporal logic programs called past-present programs, extending their semantics with completion and loop formulas to connect temporal stable models with LTLf expressions, enhancing modeling of dynamic systems.

Contribution

It introduces the past-present subclass of temporal programs and extends completion and loop formulas to characterize their models via LTLf, improving understanding of temporal logic programming.

Findings

Extended completion and loop formulas for past-present programs.

Captured temporal stable models using LTLf expressions.

Ensured past independence in dynamic domain modeling.

Abstract

Extensions of Answer Set Programming with language constructs from temporal logics, such as temporal equilibrium logic over finite traces (TELf), provide an expressive computational framework for modeling dynamic applications. In this paper, we study the so-called past-present syntactic subclass, which consists of a set of logic programming rules whose body references to the past and head to the present. Such restriction ensures that the past remains independent of the future, which is the case in most dynamic domains. We extend the definitions of completion and loop formulas to the case of past-present formulas, which allows capturing the temporal stable models of a set of past-present temporal programs by means of an LTLf expression.