The logical foundations of Answer Set Programming (ASP; [21]) rest upon the logic of Here-and-There (HT; [18]), or more precisely its equilibrium models [22] that correspond to stable models semantics [15]. For defining extensions to ASP from firm logical principles, it has thus become good practice to first elaborate upon them in the setting of HT in order to afterwards consider the respective language fragments that are well suited in the context of logic programming. This avenue was also followed in [11], which gave rise to the temporal extension of HT called Temporal Here-and-There and its non-monotonic counterpart Temporal Equilibrium Logic (for short THT and TEL [1]). More precisely, TEL builds upon an extension of the logic of HT with Linear Temporal Logic (LTL; [23]). This results in an expressive non-monotonic modal logic, which extends traditional temporal logic programming approaches [7] to the general syntax of LTL and possesses a computational complexity beyond LTL [4]. As in LTL, a model in TEL is an infinite sequence of states, called a trace. However, this rules out computation by ASP technology (and necessitates model checking) and is unnatural for applications like planning, where plans amount to finite prefixes of one or more traces (cf. [2, 12]). Unlike this, we recently proposed in [10] an alternative combination of the logics of HT and LTL whose semantics rests upon finite traces. On the one hand, this amounts to a restriction of THT and TEL to finite traces. On the other hand, this is similar to the restriction of LTL to LTLf advocated by [12]; see also [2]. Our new approach, dubbed TELf , has the following advantages. First, it is readily implementable via ASP technology. Second, it can be reduced to a normal form which is close to logic programs and much simpler than the one obtained for TEL. Finally, its temporal models are finite and offer a one-to-one correspondence to plans. Interestingly, TELf also sheds light on concepts and methodology used in incremental ASP solving when understanding incremental parameters as time points. Another distinctive feature of TELf is the inclusion of future as well as past temporal operators. We associate this with the following benefits. When using the causal reading of program rules, it is generally more natural to draw upon the past in rule bodies and to refer to the future in rule heads. A similar argument was put forward by [13] in his proposal of “declarative past and imperative future.” This format also yields a simpler normal form and lends itself to a systematic modeling methodology which favors
the definition of states in terms of the past rather than mixing in future operators. For instance, in reasoning about actions, the idea is to derive action effects for the current state and check their preconditions in the previous one, rather than to represent this as a transition from the current to the next state. This methodology aligns state constraints, effect axioms, etc. to capture the present state. As well, past operators are much easier handled computationally than their future counterparts when it comes to incremental reasoning, since they refer to already computed knowledge.
TELf is implemented in the telingo system [
Similar to the extension of LTLf to its (linear) dynamic logic counterpart LDLf [
In fact, we show that THT (and its equilibrium counterpart TEL) can be embedded into our new logic DHT (and DEL, respectively) — just as LTL can be put in LDL. Moreover, we prove that the satisfiability problem in DEL is EXPSPACE-complete; it thus coincides with that of TEL but goes beyond that of LDL and LTL, both being PSPACE-complete. In fact, the membership part of this result is obtained by means of an automata-based method for computing DEL models. Finally, we show that the monotonic base logic of DEL, namely DHT, allows us to decide strong equivalence in DEL; this reinforces the adequacy of the relation between both logics.
In the context of the version of DEL for finite traces, DELf , we developed a translation of any (converse-free) arbitrary DELf theory into a propositional theory (under the semantics of HT) and in turn into a logic program. This translation has turned out to be non-trivial: it is based on unfolding path expressions, something potentially equivalent to the execution of a sequential program. Termination is guaranteed by some preprocessing steps for normalizing path expressions.
These recent results open several interesting topics for future study. As an open
topic, it would be interesting to adapt existing model checking techniques (based on
automata construction) for temporal logics to solve the problem of existence of temporal
stable models. This was done for infinite traces in [
Title Suppressed Due to Excessive Length
ASP specifications as those handled by telingo. The current grounding of telingo
is inherited from incremental solving in clingo and does not exploit the semantics of
temporal expressions that are available now in the input language. Finally, we
envisage to extend the telingo system with features of DEL in order to obtain a powerful
system for representing and reasoning about dynamic domains, not only providing an
effective implementation of TEL and DEL but, furthermore, a platform for action and
control languages, like A; B; C [