=Paper=
{{Paper
|id=Vol-3934/paper6
|storemode=property
|title=A Declarative Framework for Temporal Reasoning in Green-Aware Applications
|pdfUrl=https://ceur-ws.org/Vol-3934/paper6.pdf
|volume=Vol-3934
|authors=Giuseppe De Giacomo,Valeria Fionda,Nicola Gigante,Antonio Ielo,Francesco Ricca,Alessandra Russo
|dblpUrl=https://dblp.org/rec/conf/greenai/GiacomoFGIRR24
}}
==A Declarative Framework for Temporal Reasoning in Green-Aware Applications==
<pdf width="1500px">https://ceur-ws.org/Vol-3934/paper6.pdf</pdf>
<pre>
                         A Declarative Framework for Temporal Reasoning in
                         Green-Aware Applications
                         Giuseppe De Giacomo1 , Valeria Fionda2 , Nicola Gigante3 , Antonio Ielo2 , Francesco Ricca2
                         and Alessandra Russo4
                         1
                           University of Oxford, UK
                         2
                           University of Calabria, IT
                         3
                           Free University of Bozen-Bolzano, IT
                         4
                           Imperial College London, UK


                                      Abstract
                                      This paper presents a novel framework that integrates Linear Temporal Logic over Finite Traces (LTLf ) with the
                                      expressive capabilities of Answer Set Programming (ASP). Combining these two powerful formalisms enables
                                      efficient reasoning in complex, temporally dynamic, and knowledge-rich environments, making it well-suited for
                                      green-aware applications that demand sustainable resource management and reduced environmental impact. The
                                      proposed framework supports the querying of evolving ASP knowledge bases, allowing both brave and cautious
                                      inferences aligned with temporal constraints. We detail the foundational principles of the framework and explore
                                      its potential applications in environmentally conscious scenarios.

                                      Keywords
                                      Linear Temporal Logic, Answer Set Programming, Green-Aware reasoning




                         1. Introduction
                         In recent years, the growing emphasis on sustainability and environmental consciousness has stimulated
                         interest in developing green-aware applications [1]. These systems require advanced reasoning capabil-
                         ities to manage resources efficiently while satisfying temporal and logical constraints. Linear Temporal
                         Logic (LTL) [2] has been a cornerstone in Computer Science for reasoning about sequences of events
                         and has found application in many domains [3, 4, 5]. The variant LTL over finite traces (LTLf ) [6, 7, 8]
                         has proven particularly effective in scenarios where operations are naturally representable by finite
                         sequences of actions [9, 10]. However, due to its propositional nature, LTLf is cumbersome when dealing
                         with complex, knowledge-intensive domains. For instance, modeling dynamic systems such as networks
                         of sensors or smart buildings often involves reasoning about properties like graph connectivity or
                         node-to-node reachability, or even more complex properties such as guaranteeing a cover or domination
                         of a subnetwork, which are challenging to express solely within LTLf .

                         Example 1. In an urban traffic network, roads (edges) may be closed for maintenance, environmental
                         reasons, or congestion control. However, at each point in time, it must be ensured that traffic flow remains
                         functional while reducing emissions by dynamically shutting down certain routes, that is ensuring that all
                         locations (nodes) remain connected despite closing certain roads. This involve reasoning about relationships
                         between nodes and edges over time. Encoding such relationships directly in LTLf requires extensive formulae
                         that become unmanageable, inefficient, and unintuitive, especially as the network complexity increases.

                            To address these limitations, we propose a new framework, called LTLASP   f , that extends LTLf by
                         integrating it with Answer Set Programming (ASP) [11, 12]. ASP is a declarative programming paradigm
                         well-suited in combinatorial optimization and knowledge representation and reasoning. Our framework
                          1st Workshop on Green-Aware Artificial Intelligence, 23rd International Conference of the Italian Association for Artificial
                          Intelligence (AIxIA 2024), November 25–28, 2024, Bolzano, Italy
                          $ giuseppe.degiacomo@cs.ox.ac.uk (G. D. Giacomo); valeria.fionda@unical.it (V. Fionda); Nicola.Gigante@unibz.it
                          (N. Gigante); antonio.ielo@unical.it (A. Ielo); francesco.ricca@unical.it (F. Ricca); a.russo@imperial.ac.uk (A. Russo)
                           0000-0001-9680-7658 (G. D. Giacomo); 0000-0002-7018-1324 (V. Fionda); 0000-0002-2254-4821 (N. Gigante);
                          0009-0006-9644-7975 (A. Ielo); 0000-0001-8218-3178 (F. Ricca); 0000-0002-3318-8711 (A. Russo)
                                      © 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
                  ceur-ws.org
Workshop      ISSN 1613-0073
Proceedings
provides a way to meld ASP’s rich, expressive language with LTLf temporal reasoning features, easing
the development of sophisticated green-aware applications. Indeed, ASP enables reasoning about
individual states induced by the temporal specification in a high-level, declarative, expressive and
concise way.

Example 2. Using LTLASP  f , the traffic network problem can be encoded more naturally and efficiently.
While LTLf handles the temporal aspects of the problem (e.g., ensuring specific routes are open or closed at
different times), ASP can handle graph properties such as connectivity and connectedness between nodes as
the system evolves. This avoids the need for propositional encodings in LTLf alone, making the encoding
significantly more concise and manageable, even as the network complexity increases.

    This paper defines the LTLASP
                                f    framework and instantiates it in several green-aware application
scenarios. The rest of the paper is organized as follows. Section 2 reviews related literature. Section 3
provides a detailed overview of Linear Temporal Logic over Finite Traces and Answer Set Programming.
In Section 4, we formally define the syntax and semantics of the LTLASP f  framework, explaining how
it integrates the temporal reasoning capabilities of LTLf with the declarative power of ASP. Section 5
illustrates the application of LTLASP
                                   f    in some green-aware domains. Finally, Section 6 concludes the
paper.


2. Related Work
Linear Temporal Logic (LTL) has been extensively used for reasoning about event sequences in various
domains, such as planning, verification, and process management [2, 3, 4]. Its finite variant, LTLf , is
particularly suitable for scenarios bounded by a finite time horizon, which is crucial in many practical
applications [6, 7]. While LTLf is a powerful formalism, its propositional nature limits the ability
to capture complex temporal properties in knowledge- and data-intensive domains. To overcome
these limitations, extensions such as LTLMT f   (LTLf Modulo Theories) [13] have been developed, which
integrate additional theories like linear integer arithmetic and uninterpreted functions to increase
expressiveness [14, 15, 16], as well as atomic constraints over concrete domains [17]. Similarly, first-order
extensions of LTLf enhance its knowledge representation capabilities by allowing richer interactions
with domain-specific data [18, 19].
   The integration of logic programming with temporal reasoning has been explored to address lim-
itations in modeling dynamic systems. Notably, Eiter et al. [20] proposed combining a declarative
planning language with Answer Set Programming (ASP), enhancing expressiveness and problem-solving
capabilities in dynamic domains. Although successful, these approaches do not fully leverage ASP as a
theory within temporal logic.
   From the Answer Set Programming perspective, the strand of research on Temporal Answer Set
Programming (TASP) [21] extends standard ASP with LTL-like temporal constructs. Our approach is
not an extension of ASP with temporal constructs, but rather the embedding of ASP into LTLf reasoning,
facilitating complex queries over execution traces.
   Another strand of related research is stream reasoning, which deals with continuous query answering
over data streams [22], which often relies on logic programming as its foundation. ASP-based stream
reasoning systems typically focus on window-based approaches, processing segments of data streams to
perform temporal reasoning. Our approach reasons over finite traces, making it ideal for green-aware
applications requiring full temporal context [23].
   There have been in the literature also some proposals for ASP Modulo Theories [24] that extends
ASP by integrating external theories, akin to how SAT is extended by Satisfiability Modulo Theories
(SMT) [25, 26]. This extension allows ASP to interface with additional reasoning modules. Our departure
point is entirely different since we aim to use ASP as a theory within LTLf , enabling advanced reasoning
capabilities tailored specifically for knowledge-rich, temporal environments. Thus, our proposal relates
more to first-order extensions of LTLf and LTLMT  f   than TASP.
   Green-aware reasoning has gained significant attention recently as sustainability has become a
critical concern. Some proposals that leverage logic-based approaches have been used to model and
manage energy consumption, optimize resource allocation, and reduce environmental impacts in various
applications. A recent proposal [27] introduced a formal framework using temporal logic and simulation
tools to model and verify the energy management of buildings. In [28] the authors present a fuzzy
temporal logic-based approach to optimize energy-efficient routing in wireless sensor networks (WSNs)
integrating fuzzy logic with temporal reasoning to enhance sustainability in network operations. These
approaches demonstrate the potential of logic-based formalisms in promoting sustainability. However,
existing systems often focus on specific application domains and lack the generality and expressive
power needed to address broader green-aware scenarios, a gap that our proposed LTLASP   f  framework
aims to fill.


3. Preliminaries
This section recaps basic notions of Linear Temporal Logic over Finite Traces (LTLf ) and Answer Set
Programming (ASP) that will be used in the rest of the paper.

3.1. Linear Temporal Logic over Finite Traces
Linear Temporal Logic (LTL) is a propositional modal logic, that allows one to reason about the temporal
properties of traces. A trace is an infinite sequence of sets of propositional symbols. LTL handles time in
an abstract manner, focusing on the relative order of events within a trace rather than on the duration of
those events. Despite its abstract treatment of time, LTL has been widely and successfully applied in
various computer science fields, including planning [29, 3, 30], robotics and control theory [31, 32], and
business process management [33, 9]. Linear Temporal Logic over Finite Traces (LTLf ) [6] keeps the
same syntax as LTL but is interpreted over finite traces.
  Let 𝒜 be a finite set of propositional symbols. An LTLf formula is defined according to the following
grammar:
                                 𝜙 := 𝑎 ∈ 𝒜 | ⊤ | ¬𝜙 | 𝜙 ∧ 𝜙 | X 𝜙 | 𝜙 U 𝜙
   Standard shorthand for propositional logic applies. Moreover, we define the eventually operator
F 𝜙 ≡ ⊤ U 𝜙, the always operator G 𝜙 ≡ ¬F ¬𝜙, and the release operator 𝜙1 R 𝜙2 ≡ ¬(¬𝜙1 U ¬𝜙2 ).
   A trace 𝜋 is a sequence 𝜋 = 𝜋0 , . . . , 𝜋𝑛 − 1, where 𝜋𝑖 ⊆ 𝒜 for each 0 < 𝑖 < 𝑛; we say that 𝑛 is the
length of the trace, denoted by |𝜋|. A trace 𝜋 satisfies an LTLf formula 𝜙 at time 𝑖, denoted by 𝜋, 𝑖 |= 𝜙,
according to the following inductive rules:

    • 𝜋, 𝑖 |= ⊤ for all 𝑖 ∈ {0, . . . , |𝜋|}
    • 𝜋, 𝐼 |= 𝛼 for 𝛼 ∈ 𝒜 if 𝛼 ∈ 𝜋𝑖
    • 𝜋, 𝑖 |= ¬𝜙 if 𝜋, 𝑖 ̸|= 𝜙
    • 𝜋, 𝑖 |= 𝜙1 ∧ 𝜙2 if 𝜋, 𝑖 |= 𝜙1 and 𝜋, 𝑖 |= 𝜙2 ;
    • 𝜋, 𝑖 |= X 𝜙1 if 𝑖 < |𝜋| − 1 and 𝜋, 𝑖 + 1 |= 𝜙1 ;
    • 𝜋, 𝑖 |= 𝜙1 U 𝜙2 if ∃𝑗 with 𝑖 ≤ 𝑗 ≤ |𝜋| s.t. 𝜋, 𝑗 |= 𝜙2 and ∀𝑘 with 𝑖 ≤ 𝑘 < 𝑗.

  In practical applications, states often represent the system’s status at discrete moments, with traces
capturing the system’s evolution over time. Furthermore, we say that 𝜋 is a model of 𝜙 if 𝜋, 0 |= 𝜙.

Example 3. Consider a green-aware energy management system for smart buildings, where 𝒜 =
{lightOff, lowPowerMode}. The formula 𝜙 = G (lightOff U ¬(lowPowerMode)) specifies that
the lights must remain off whenever the system is in low power mode, and this condition
must hold at all times. This constraint ensures continuous energy saving by keeping lights
off during periods of reduced power consumption. An example trace that satisfies 𝜙 is 𝜋 =
{lightOff, lowPowerMode}, {lightOff, lowPowerMode}, {lightOff}, {}, maintaining the lights off consis-
tently until low power mode is exited.
3.2. Answer Set Programming
Answer Set Programming (ASP) [11, 12] is a declarative knowledge representation formalism rooted
in the answer set semantics of logic programs that can solve problems up to Σ𝑃2 in the polynomial
hierarchy. This section briefly summarizes basic notions about its syntax, semantics, and reasoning
tasks. The examples in the rest of the paper will use the clingo input language. Interested readers can
refer to [34] for a reference on the modeling capabilities of the language.

3.2.1. Syntax.
A normal logic program 𝑃 is a set of (normal) rules, expressions ℎ ← 𝑎1 , . . . , 𝑎𝑘 , ¬𝑏1 , . . . , ¬𝑏𝑘 ., where
ℎ, 𝑎𝑖 , 𝑏𝑗 are atoms. An atom is an expression 𝑝(𝑡1 , . . . , 𝑡𝑘 ) where 𝑝 is a predicate name, 𝑡𝑖 are terms built
over a set of constants 𝒞 that appear in 𝑃 . The symbol ¬ denotes negation-as-failure, typeset as not in
code examples. A literal is either an atom 𝑎 or a negated atom ¬𝑎, where we say that ¬𝑎 is the opposite
literal of 𝑎. Given the rule 𝜌 = ℎ ← 𝑎1 , . . . , 𝑎𝑘 , ¬𝑏1 , . . . ¬𝑏𝑘 we denote by 𝐻(𝜌) = {ℎ} its head, 𝐵(𝜌) =
{𝑎1 , . . . , 𝑎𝑘 , ¬𝑏1 , . . . , ¬𝑏𝑘 } its body, which can be partitioned into 𝐵 + (𝜌) = {𝑎1 , . . . , 𝑎𝑘 } (“positive
body”) and 𝐵 − (𝜌) = {𝑏1 , . . . , 𝑏𝑘 } (“negative body”). Modern ASP systems’ input language accepts
many syntactic shortcuts, which ease modeling tasks without increasing the language expressiveness
from a complexity point of view, as for example weight rules, cardinality constraints, and choice rules -
that can all be rewritten into sets of normal rules. In particular, the disjunctive extension of the language,
which allows more atoms in the head of the rule, increases its expressivity up to Σ𝑃2 , while normal logic
programs can model up to NP problems.

3.2.2. Semantics.
Let ℬ(𝑃 ) denote the Herbrand base of a logic program 𝑃 , which is the set of all possible atoms that
can be formed using the predicates and constants present in 𝑃 . A logic program with variables is
considered syntactic sugar for its ground version, which consists of all the rules that can be generated by
substituting variables with atoms from ℬ(𝑃 ). An interpretation ℐ is a subset of ℬ(𝑃 ), and it satisfies a
rule 𝜌 if 𝐵 + (𝜌) ⊆ ℐ and 𝐵 − (𝜌) ∩ ℐ = ∅, where 𝐵 + (𝜌) and 𝐵 − (𝜌) represent the positive and negative
body of the rule, respectively. If ℐ satisfies all rules of 𝑃 , then ℐ is a model of 𝑃 . The reduct of 𝑃 with
respect to ℐ, denoted 𝑃 ℐ , is obtained by removing from 𝑃 all rules 𝜌 where either (i) 𝐵 + (𝜌) ̸⊆ ℐ or (ii)
𝐵 − (𝜌) ∩ ℐ ̸= ∅. A subset-minimal model of the reduct 𝑃 ℐ is called an answer set (or stable model) of 𝑃 .
A logic program can have zero, one, or multiple answer sets; it is termed coherent if it has at least one
answer set, and incoherent if it has none. The collection of all answer sets of 𝑃 is denoted by 𝐴𝑆(𝑃 ).

3.2.3. Solving Problems via ASP
The standard approach to solve problems using ASP is to write a (typically non-ground) logic program
𝑃 such that, given a problem instance encoded by a set of facts 𝐹 , the answer sets of the logic program
𝑃 ∪ 𝐹 result in solutions to the problem instance at hand. The logic program 𝑃 is usually written
according to the guess & check programming technique, and consists of two subprograms: a guess
program that generates potential answer sets (which typically includes choice rules or disjunctive rules);
and a check component that asserts solution’s properties (e.g., discarding unfit candidate solutions) by
means of constraints. An illustrative example of this approach is the subgraph isomorphism problem.

Example 4 (Green-Aware Subgraph Isomorphism). Subgraph isomorphism is a classic NP-complete
problem [35]. Given two graphs, 𝐺(𝑉, 𝐸) and 𝐻(𝑉 ′ , 𝐸 ′ ), the aim is to determine whether there exists a
subgraph of 𝐺 that is isomorphic to 𝐻. This involves finding a bijection 𝜎 : 𝑉 ′ → 𝑉0 , where 𝑉0 ⊆ 𝑉 ,
such that an edge (𝑥, 𝑦) ∈ 𝐸 ′ corresponds precisely to an edge (𝜎(𝑥), 𝜎(𝑦)) ∈ 𝐸. Subgraph isomorphism
can be applied to check the efficient energy distribution in smart grids. Consider two graphs: 𝐺(𝑉, 𝐸)
representing the full power grid and 𝐻(𝑉 ′ , 𝐸 ′ ) representing an energy-efficient subnetwork configuration.
The task is to determine whether a subgraph of 𝐺 exists that is isomorphic to 𝐻, reflecting an optimal
way to manage energy flow. In this context, finding a subgraph isomorphism corresponds to identifying an
energy-efficient setup within the larger grid. The bijection 𝜎 : 𝑉 ′ → 𝑉0 , where 𝑉0 ⊆ 𝑉 , maps nodes (e.g.,
energy sources, transformers, and consumers) of the desired configuration 𝐻 onto nodes in the larger grid
𝐺, such that every connection (𝑥, 𝑦) ∈ 𝐸 ′ matches a corresponding connection (𝜎(𝑥), 𝜎(𝑦)) ∈ 𝐸.
  The problem can be modeled using the following logic program. An atom 𝑚𝑎𝑡𝑐ℎ(𝑥, 𝑦) encodes that
node 𝑥 ∈ 𝑉 ′ is matched to node 𝑦 ∈ 𝑉 . The background knowledge is the set of facts 𝑛𝑜𝑑𝑒/1, 𝑒𝑑𝑔𝑒/2
that encode 𝑉 and 𝐸, plus ℎ𝑛𝑜𝑑𝑒/1, ℎ𝑒𝑑𝑔𝑒/2 that encode 𝑉 ′ and 𝐸 ′ .

{ match(HX,X): node(X) } = 1 :- hnode(HX).
:- match(HX,X), match(HY,Y), hedge(HX,HY), not edge(X,Y).

   The choice rule generates graph matching between the energy-efficient subnetwork and the full power
grid, where the 𝑚𝑎𝑡𝑐ℎ(𝐻𝑋, 𝑋) atom models that the node 𝐻𝑋 in 𝐻 is matched onto the active node 𝑋
in 𝐺. Finally, a constraint discards candidate solutions that violate the definition of graph isomorphism.
The answer sets of the above program encode possible 𝜎 that yield a valid matching between 𝐻 and 𝐺.

   Let 𝑃 be a logic program. The cautious consequences of 𝑃 , denoted by Cautious(𝑃 ), are the atoms
that are true in all answer sets of 𝑃 , while the brave consequences, denoted by Brave(𝑃 ), are the atoms
that are true in at least one answer set. If 𝑃 has a unique answer set, as is often the case when 𝑃 is a
Datalog program, then Cautious(𝑃 ) = Brave(𝑃 ). For an atom 𝛼 and a set of positive literals 𝑀 , we
say ¬𝛼 ∈ 𝑀 if 𝛼 ̸∈ 𝑀 . An atom 𝛼 bravely holds in 𝑃 , denoted 𝑃 |=𝑏 𝛼, if there exists an answer set
𝑀 ∈ 𝐴𝑆(𝑃 ) such that 𝛼 ∈ 𝑀 . Conversely, 𝛼 cautiously holds in 𝑃 , denoted 𝑃 |=𝑐 𝛼, if 𝛼 is present in
all answer sets of 𝑃 . By definition, 𝑃 |=𝑏 𝛼 if and only if 𝑃 ̸|=𝑐 ¬𝛼.
   In a green-aware context, consider a scenario where we use these reasoning modes to optimize
energy distribution in a smart grid by finding energy-efficient subgraph configurations. Let Π𝑆𝐺𝐼 be
the program reported in Example 4, 𝐹 (𝐺) and 𝐹 (𝐻) be the set of facts encoding the graphs 𝐺 and 𝐻,
respectively.

Example 5 (Brave Reasoning in Energy Optimization). Suppose we want to determine if there is
an energy-efficient subgraph configuration between two power grid structures, 𝐺 and 𝐻, that does not use
a specific node 𝑥 ∈ 𝑉 (e.g., a transformer station). This question can be addressed using a brave query on
the atom 𝑛𝑜𝑡_𝑢𝑠𝑒𝑑(𝑥), which indicates whether node 𝑥 is part of any feasible configuration:

used(X) :- match(_,X).
not_used(X) :- not used(X), node(X).

This query checks if there exists at least one subgraph isomorphism where the node 𝑥 is not used, aligning
with a potential energy-saving configuration.

Example 6 (Cautious Reasoning in Grid Stability). To ensure grid stability, we might need to verify
if a specific mapping 𝜎(𝑥) = 𝑦 holds in all valid energy-efficient subgraph configurations. This can be
formulated as a cautious query, Π𝑆𝐺𝐼 ∪ 𝐹 (𝐺) ∪ 𝐹 (𝐻) |=𝑐 𝑚𝑎𝑡𝑐ℎ(𝑦, 𝑥), ensuring that 𝑥 consistently
maps to 𝑦 across all subgraph isomorphisms, thus confirming its necessity for stable and sustainable grid
operations.


4. The LTLASP
          f   Framework
In this section, we introduce the syntax and semantics of LTLASPf , an extension of LTLf within the LTLf
                                                                                                        MT

framework that incorporates queries over logic programs with answer set semantics as an external
theory. The core idea, detailed further in the following, is to specify how system properties, represented
as cautious and brave queries over a logic program, should evolve over time. In this framework, traces
capture the temporal evolution of the system’s state in a relational form. Logic programs enrich this
relational representation by defining additional domain-specific concepts through rules. Queries over
these programs allow us to verify whether certain properties hold at given points in time. Standard
linear temporal logic operators are then used to impose constraints on how these properties evolve,
providing a powerful mechanism for temporal reasoning within knowledge-intensive environments.
   Let ℬ be an ASP program, referred to as the background knowledge. In typical ASP modeling, ℬ has
a fixed fact schema, meaning that all atoms conforming to a specific signature are considered input
facts representing the problem instance and do not appear in the head of any rule within ℬ. We denote
the set of all possible input facts for ℬ as ℱ. Let 𝒜 be a finite set of propositional symbols, such that
𝒜 ∩ ℱ = ∅.
                                                                                         * , or simply 𝜋 * ,
   Given a trace 𝜋 over the alphabet 𝒜 and a fact projection 𝑝𝑟𝑗, the trace projection 𝜋𝑝𝑟𝑗
is defined as a trace over ℱ (interpreted as propositional symbols), specified as:
                                                       ⋃︁
                                          𝜋 * (𝑖) =            𝑝𝑟𝑗(𝑎)
                                                      𝑎∈𝜋(𝑖)


Example 7. Consider the trace 𝜋 = {𝑎, 𝑏}, {𝑏, 𝑐}, {𝑎, 𝑐} over 𝒜 = {𝑎, 𝑏, 𝑐}, and 𝑝𝑟𝑗 to be de-
fined as 𝑝𝑟𝑗(𝑎) = {𝑓 (𝑥)}, 𝑝𝑟𝑗(𝑏) = {𝑓 (𝑦)} and 𝑝𝑟𝑗(𝑐) = {𝑔(𝑧), ℎ(𝑦, 𝑥)}. Then 𝜋 * =
{𝑓 (𝑥), 𝑓 (𝑦)}, {𝑓 (𝑦), 𝑔(𝑧), ℎ(𝑦, 𝑥)}, {𝑓 (𝑥), 𝑔(𝑧), ℎ(𝑦, 𝑥)}.

   Whenever this does not cause ambiguities, with a slight abuse of notation we will describe traces 𝜋
directly as a sequence of sets of facts, rather than explicitly stating the projection function 𝑝𝑟𝑗.

4.1. Syntax & Semantics
An LTLASP
      f   formula over a program ℬ and a propositional alphabet 𝒜 is defined by extending the LTLf
grammar with additional atomic formulae, as follows:

                                            𝜓 := 𝑎 | 𝑏?ℎ | 𝑐?ℎ
                                   𝜙 := 𝜓 | ¬𝜙 | 𝜙 ∧ 𝜙 | X 𝜙 | 𝜙 U 𝜙
where 𝑎 ∈ 𝒜, ℎ ∈ ℬ(𝑃 ), and 𝑏? and 𝑐? denote brave entailment and cautious entailment, respectively.
Standard shorthands for propositional and temporal logic apply. The satisfaction relation for a formula 𝜙
is defined inductively, with propositional and temporal operators following the standard LTLf semantics.
The specific semantics for atomic formulae 𝑎, 𝑏?ℎ, and 𝑐?ℎ are as follows:

    • 𝜋, 𝑖 |= 𝑎 if 𝑎 ∈ 𝜋(𝑖);
    • 𝜋, 𝑖 |= 𝑐?ℎ if ℬ ∪ 𝜋𝑝𝑟𝑗* (𝑖) cautiously entails ℎ, meaning ℎ is present in all answer sets of the
                       *
      program ℬ ∪ 𝜋𝑝𝑟𝑗 (𝑖);
    • 𝜋, 𝑖 |= 𝑏?ℎ if ℬ ∪ 𝜋𝑝𝑟𝑗* (𝑖) bravely entails ℎ, meaning ℎ appears in at least one answer set of
             *
      ℬ ∪ 𝜋𝑝𝑟𝑗 (𝑖).

  It is important to note that LTLASP
                                   f   extends LTLf only at the level of atomic formulae, leaving the
temporal semantics of LTLf unchanged. Thus, any LTLf formula is also a valid LTLASP
                                                                                  f  formula (using a
                                                                ′
projection function which assigns each 𝑎 ∈ 𝒜 the singleton {𝑎 }). Subformulae of the types 𝑏?ℎ and
𝑐?ℎ express additional constraints in terms of brave or cautious entailment over ℬ ∪ 𝜋 * (𝑖), enriching
the expressive power of the logic.

4.2. Trace Verification
We focus on the trace verification problem for LTLASP
                                                  f , defined as follows:

Definition 1 (Trace Verification). Let 𝜙 be an LTLASP
                                                  f   formula and 𝜋 a trace. The trace verification
problem consists of determining whether 𝜋 |= 𝜙.
   To address the trace verification problem, we can apply any standard technique used for evaluating
LTLf formulas over a trace, handling standard temporal operators and atomic formulae directly, while
using an external oracle to evaluate the brave and cautious entailment of specific atomic formulae.
Specifically, given a formula 𝜙, we define its boolean abstraction 𝜙* as the LTLf formula obtained by
replacing each brave and cautious entailment atomic formula with a propositional variable, effectively
treating 𝑐?ℎ and 𝑏?ℎ as propositional symbols.
   We then use standard techniques to check whether 𝜋 |= 𝜙* . However, when an entailment needs
evaluation, we delegate the task to an external ASP oracle. In the worst case, this approach may require
up to |𝜋| × |𝑄| calls to the external oracle, where |𝑄| represents the number of entailment queries.
   From an implementation perspective, another viable approach could be a two-phase process: first,
evaluate all entailment queries over the trace to generate a projection, and then verify the resulting
LTLf formula against this projection.


5. Green-Aware Application Scenarios of LTLASP
                                           f

The introduction of LTLASP
                         f  offers powerful tools for reasoning about dynamic, knowledge-intensive
systems in green-aware applications. By combining the temporal reasoning capabilities of LTLf with
the expressive power of Answer Set Programming (ASP), LTLASP     f   enables advanced modeling and
verification of complex temporal behaviors that are crucial for sustainable resource management. In
this section, we explore several application scenarios where LTLASPf  can be effectively employed to
enhance energy efficiency, optimize resource utilization, and support decision-making processes in
environmentally conscious contexts.
Green-Aware Energy Flow Control. Consider an energy distribution network modeled as a directed
graph 𝐺(𝑉, 𝐸), where nodes represent substations and consumers, and edges represent power lines
connecting them. The goal is to verify that critical nodes, represented by the set 𝐶 ⊂ 𝑉 (e.g., hospitals,
data centers), remain powered while the network configuration is dynamically adjusted to minimize
energy losses. Figure 1 depicts an example. Red nodes represent critical nodes, the yellow one is the
power source node and the green ones the functioning nodes at each time instant.
   We can model this scenario as follows. The background knowledge ℬ captures the “static” properties
of the network, its underlying graph as facts, as well as the notions of node isolation and being powered
(e.g., connected to the source node).

% Network Topology
node(1). node(2). node(3). node(4). node(5). node(6). node(7). node(s).
edge(1,2). edge(1,6). edge(2,3). edge(2,6). edge (2,7). edge(3,4).
edge(3,7). edge(4,7). edge(4,5). edge(5,7). edge(6,7).
edge(source,1). edge(source,6).
criticalConsumer(2). criticalConsumer(4).
% Domain definition: Connectedness & Isolation
reachable(X, Y) :- edge(X, Y), on(X), on(Y).
reachable(X, Z) :- edge(X, Y), on(X), reachable(Y, Z).
isolated(X) :- node(X), not reachable(source, X).
% A critical consumer is not connected to power
fail :- criticalConsumer(X), isolated(X).

   The rule fail :- criticalConsumer(X), isolated(X). derives the atom fail whenever
there’s a critical, isolated node. Notice that since ℬ is a Datalog program with a unique answer set,
brave reasoning and cautious reasoning coincide. Input facts for this program will match the signature
𝑜𝑛/1, where an atom 𝑜𝑛(𝑥) denotes that node 𝑥 is powered on.
   The LTLASP f     formula below specifies that certain critical consumers (represented by
criticalConsumer(𝑥)) should not be isolated, i.e., they must remain connected to an energy
Figure 1: Temporal evolution of a green-aware energy management system showing critical consumers (in red),
source node (in yellow), and active components (in green) at each time step.


source. This requirement is enforced over time using a cautious entailment query. Moreover, to avoid
node overload it also specifies that each (not critical) node must be switched off at a certain point.
                                                       ⋀︁
                                 𝜙 = G (¬𝑐?fail) ∧            (F (¬on(𝑛)))
                                                     𝑛∈𝑉 ∖𝐶

   Traces capture the “dynamic” part of the system, that is which nodes are powered over time. The
following trace encodes the network evolution in Figure 1:


      𝜋 = {on(𝑠𝑜𝑢𝑟𝑐𝑒), on(6), on(7), on(2), on(4)}, {on(𝑠𝑜𝑢𝑟𝑐𝑒), on(6), on(3), on(2), on(4)},

         {on(𝑠𝑜𝑢𝑟𝑐𝑒), on(1), on(3), on(2), on(4)}, {on(𝑠𝑜𝑢𝑟𝑐𝑒), on(6), on(7), on(2), on(4)}
   The trace 𝜋 satisfies the formula 𝜙. In fact, for every non-critical consumer node there is at least one
time instant in which the node is switched off and, in all time instants, critical nodes are reachable from
the source node by only passing through functioning nodes.
Efficient Energy Distribution in Smart Grids. Consider two graphs: 𝐺(𝑉, 𝐸), representing a full
power grid, and 𝐻(𝑉 ′ , 𝐸 ′ ), representing an energy-efficient subnetwork configuration. Nodes in the
smart grid may be damaged, overloaded, or under maintenance, making them temporarily unavailable.
The task is to determine whether, during the grid’s operation, there always exists a subgraph of the
evolving grid 𝐺 that is isomorphic to 𝐻, reflecting an optimal energy flow configuration. Similarly to
the previous apprication scenario, the background knowledge ℬ is used to capture the structure of the
two networks, as well as the notion of isomorphism.
   To model this scenario, we assume the input trace contains facts matching the signature 𝑜𝑛/1, to
model that a certain node is active. The background knowledge ℬ models the full power grid by means
of facts 𝑛𝑜𝑑𝑒/1, 𝑒𝑑𝑔𝑒/2 that encode 𝑉 and 𝐸, while the energy-efficient subnetwork is modeled by the
predicates ℎ𝑛𝑜𝑑𝑒/1, ℎ𝑒𝑑𝑔𝑒/2.

success.
active(X,Y) :- on(X), on(Y), edge(X,Y).
{ match(HX,X): on(X) } = 1 :- hnode(HX).
:- match(HX,X), match(HY,Y), hedge(HX,HY), not active(X,Y).

  The 𝑎𝑐𝑡𝑖𝑣𝑒/2 predicate filters grid links between active nodes, discarding ones where at least one of
the endpoints is not active. The choice rule generates graph matching between the energy-efficient
subnetwork and the active power grid, where the 𝑚𝑎𝑡𝑐ℎ(𝐻𝑋, 𝑋) atom models that the node 𝐻𝑋 in
the energy-efficient subnetwork is matched onto the active node 𝑥 of the full power grid. Finally, a
constraint discards candidate solutions that violate the definition of graph isomorphism.
   As in the previous application case, input facts for this program have signature 𝑜𝑛/1, where an atom
𝑜𝑛(𝑥) denotes that node 𝑥 is functioning.
   The LTLASP
            f   formula below specifies that always, during its working, the subnetwork of 𝐺 induced
by only functioning nodes, contains the given optimal energy flow configuration, i.e., a subgraph
isomorphic to the energy-efficient subnetwork. This requirement is enforced over time using a brave
uentailment query.

                                             𝜙 = G (𝑏?success)


6. Conclusion
In this paper, we introduced LTLASP
                                  f , a novel framework that extends Linear Temporal Logic over Finite
Traces (LTLf ) by integrating it with Answer Set Programming (ASP), offering a powerful approach for
reasoning about dynamic systems in green-aware applications. By combining the temporal reasoning
capabilities of LTLf with the declarative and expressive power of ASP, LTLASP
                                                                           f  enables efficient modeling
and verification of complex temporal behaviors, making it particularly well-suited for knowledge-
intensive domains.
   Through a series of examples, we demonstrated how LTLASP    f   provides expressive and manageable
solutions, particularly when handling properties like node reachability or graph connectivity. The
integration of ASP allows for high-level, declarative reasoning about individual states derived from
temporal specifications, significantly enhancing the framework’s flexibility and expressiveness in
modeling complex systems. Future work will explore additional reasoning tasks within the LTLASP      f
framework, such as satisfiability checking, and extend its applicability beyond green-aware domains to
other dynamic systems requiring advanced temporal reasoning.

Acknowledgments. This work was supported by the Italian Ministry of Research (MUR) under PRIN project
PINPOINT - CUP H23C22000280006; PRIN project HypeKG - CUP H53D23003710006; PRIN 2022 PNRR project
DISTORT funded by European Union Next Generation EU Mission 4 Component 1 - CUP: H53D23008170001;
PNRR projects FAIR “Future AI Research” - Spoke 9 - WP9.1 and WP9.2, Spoke 5 - WP5.1 and Spoke 6, through
the NRRP MUR Program funded by the NextGenerationEU and by the ERC-ADG WhiteMech (No. 834228).


References
 [1] V. Bolón-Canedo, L. Morán-Fernández, B. Cancela, A. Alonso-Betanzos, A review of green artificial
     intelligence: Towards a more sustainable future, Neurocomputing 599 (2024) 128096.
 [2] A. Pnueli, The temporal logic of programs, in: 18th Annual Symposium on Foundations of Computer
     Science, IEEE Computer Society, 1977, pp. 46–57.
 [3] D. Calvanese, G. De Giacomo, M. Y. Vardi, Reasoning about actions and planning in LTL action theories, in:
     KR, 2002, pp. 593–602.
 [4] G. De Giacomo, F. M. Maggi, A. Marrella, S. Sardiña, Computing trace alignment against declarative process
     models through planning, in: ICAPS, 2016, pp. 367–375.
 [5] G. De Giacomo, M. Y. Vardi, Automata-theoretic approach to planning for temporally extended goals, in:
     ECP, volume 1809 of LNCS, 1999, pp. 226–238.
 [6] G. De Giacomo, M. Y. Vardi, Linear temporal logic and linear dynamic logic on finite traces, in: Proceedings
     of the 23rd International Joint Conference on Artificial Intelligence, IJCAI/AAAI, 2013, pp. 854–860.
 [7] V. Fionda, G. Greco, LTL on finite and process traces: Complexity results and a practical reasoner, J. Artif.
     Intell. Res. 63 (2018) 557–623.
 [8] C. Dodaro, V. Fionda, G. Greco, LTL on weighted finite traces: Formal foundations and algorithms, in: IJCAI,
     ijcai.org, 2022, pp. 2606–2612.
 [9] V. Fionda, A. Guzzo, Control-flow modeling with declare: Behavioral properties, computational complexity,
     and tools, IEEE TKDE 32 (2020) 898–911.
[10] C. Di Ciccio, M. Montali, Declarative process specifications: Reasoning, discovery, monitoring, in: Process
     Mining Handbook, volume 448 of Lecture Notes in Business Information Processing, Springer, 2022, pp.
     108–152.
[11] G. Brewka, T. Eiter, M. Truszczynski, Answer set programming at a glance, Commun. ACM 54 (2011)
     92–103.
[12] M. Gelfond, V. Lifschitz, Classical negation in logic programs and disjunctive databases, New Gener. Comput.
     9 (1991) 365–386.
[13] L. Geatti, A. Gianola, N. Gigante, S. Winkler, Decidable fragments of ltlf modulo theories, in: K. Gal, A. Nowé,
     G. J. Nalepa, R. Fairstein, R. Radulescu (Eds.), ECAI 2023 - 26th European Conference on Artificial Intelligence,
     September 30 - October 4, 2023, Kraków, Poland - Including 12th Conference on Prestigious Applications of
     Intelligent Systems (PAIS 2023), volume 372 of Frontiers in Artificial Intelligence and Applications, IOS Press,
     2023, pp. 811–818.
[14] P. Baldan, P. Mancarella, A. Raffaetà, F. Turini, Mutaclp: A language for temporal reasoning with multiple
     theories, in: Computational Logic: Logic Programming and Beyond, volume 2408 of Lecture Notes in
     Computer Science, Springer, 2002, pp. 1–40.
[15] L. Geatti, N. Gigante, A. Montanari, G. Venturato, SAT meets tableaux for linear temporal logic satisfiability,
     J. Autom. Reason. 68 (2024) 6.
[16] B. Finkbeiner, P. Heim, N. Passing, Temporal stream logic modulo theories, in: FoSSaCS, volume 13242 of
     Lecture Notes in Computer Science, Springer, 2022, pp. 325–346.
[17] S. Demri, D. D’Souza, An automata-theoretic approach to constraint LTL, Inf. Comput. 205 (2007) 380–415.
[18] A. Artale, A. R. Gnatenko, V. Ryzhikov, M. Zakharyaschev, On deciding the data complexity of answering
     linear monadic datalog queries with LTL operators (extended abstract), in: Description Logics, volume 3739
     of CEUR Workshop Proceedings, CEUR-WS.org, 2024.
[19] A. Artale, A. Mazzullo, A. Ozaki, First-order temporal logic on finite traces: Semantic properties, decidable
     fragments, and applications, ACM Trans. Comput. Log. 25 (2024) 13:1–13:43.
[20] T. Eiter, W. Faber, N. Leone, G. Pfeifer, A. Polleres, A logic programming approach to knowledge-state
     planning: Semantics and complexity, ACM Trans. Comput. Log. 5 (2004) 206–263.
[21] F. Aguado, P. Cabalar, M. Diéguez, G. Pérez, T. Schaub, A. Schuhmann, C. Vidal, Linear-time temporal
     answer set programming, Theory Pract. Log. Program. 23 (2023) 2–56.
[22] E. D. Valle, S. Ceri, F. van Harmelen, D. Fensel, It’s a streaming world! reasoning upon rapidly changing
     information, IEEE Intell. Syst. 24 (2009) 83–89.
[23] H. Beck, T. Eiter, C. Folie, Ticker: A system for incremental asp-based stream reasoning, Theory Pract. Log.
     Program. 17 (2017) 744–763.
[24] M. Gebser, R. Kaminski, B. Kaufmann, M. Ostrowski, T. Schaub, P. Wanko, Theory solving made easy with
     clingo 5, in: ICLP (Technical Communications), volume 52 of OASIcs, Schloss Dagstuhl - Leibniz-Zentrum
     für Informatik, 2016, pp. 2:1–2:15.
[25] C. W. Barrett, C. Tinelli, Satisfiability modulo theories, in: Handbook of Model Checking, Springer, 2018, pp.
     305–343.
[26] A. Armando, C. Castellini, E. Giunchiglia, M. Idini, M. Maratea, TSAT++: an open platform for satisfiability
     modulo theories, in: D/PDPAR@IJCAR, volume 125 of Electronic Notes in Theoretical Computer Science,
     Elsevier, 2004, pp. 25–36.
[27] M. Ehsanpour, L. Baresi, M. Rossi, E. Damiani, Analysis of energy-efficient buildings through simulation
     and formal methods, in: SIMPDA, volume 1757 of CEUR Workshop Proceedings, CEUR-WS.org, 2016, pp.
     113–119.
[28] M. Selvi, R. Logambigai, S. Ganapathy, L. S. Ramesh, H. K. Nehemiah, K. Arputharaj, Fuzzy temporal
     approach for energy efficient routing in WSN, in: ICIA, ACM, 2016, pp. 117:1–117:5.
[29] F. Bacchus, F. Kabanza, Planning for temporally extended goals, Ann. Math. Artif. Intell. 22 (1998) 5–27.
[30] S. Sohrabi, J. A. Baier, S. A. McIlraith, Preferred explanations: Theory and generation via planning, in:
     AAAI, AAAI Press, 2011, pp. 261–267.
[31] L. Bobadilla, O. Sanchez, J. Czarnowski, K. Gossman, S. M. LaValle, Controlling wild bodies using linear
     temporal logic, in: Robotics: Science and Systems, 2011.
[32] X. C. Ding, S. L. Smith, C. Belta, D. Rus, Optimal control of markov decision processes with linear temporal
     logic constraints, IEEE Trans. Autom. Control. 59 (2014) 1244–1257.
[33] F. M. Maggi, M. Westergaard, M. Montali, W. M. P. van der Aalst, Runtime verification of ltl-based declarative
     process models, in: RV, volume 7186 of Lecture Notes in Computer Science, Springer, 2011, pp. 131–146.
[34] M. Gebser, R. Kaminski, B. Kaufmann, T. Schaub, Multi-shot ASP solving with clingo, Theory Pract. Log.
     Program. 19 (2019) 27–82.
[35] M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H.
     Freeman, 1979.

</pre>