=Paper=
{{Paper
|id=Vol-3203/paper9
|storemode=property
|title=A Formal Comparison between Datalog-based Languages for Stream Reasoning
|pdfUrl=https://ceur-ws.org/Vol-3203/paper9.pdf
|volume=Vol-3203
|authors=Nicola Leone,Marco Manna,Maria Concetta Morelli,Simona Perri
|dblpUrl=https://dblp.org/rec/conf/datalog/LeoneMMP22
}}
==A Formal Comparison between Datalog-based Languages for Stream Reasoning==
https://ceur-ws.org/Vol-3203/paper9.pdf
A Formal Comparison between Datalog-based
Languages for Stream Reasoning
Nicola Leone1,† , Marco Manna1,† , Maria Concetta Morelli1,*,† and Simona Perri1,†
1
Department of Mathematics and Computer Science, University of Calabria, Rende, Italy
Abstract
The paper investigates the relative expressiveness of two logic-based languages for reasoning over
streams, namely LARS Programs — the language of the Logic-based framework for Analytic Reasoning
over Streams called LARS — and LDSR — the language of the recent extension of the 𝐼 -DLV system for
stream reasoning called I-DLV-sr. Although these two languages build over Datalog, they do differ both
in syntax and semantics. To reconcile their expressive capabilities for stream reasoning, we define a
comparison framework that allows us to show that, without any restrictions, the two languages are
incomparable and to identify fragments of each language that can be expressed via the other one.
Keywords
Stream Reasoning, Datalog, Knowledge Representation and Reasoning, Relative Expressiveness
1. Introduction
Stream Reasoning (SR) [1] is a recently emerged research area that consists in the application of
inference techniques to heterogeneous and highly dynamic streaming data. Stream reasoning
capabilities are nowadays a key requirement for deploying effective applications in several real-
world domains, such as IoT, Smart Cities, Emergency Management. Different SR approaches have
been proposed in contexts such as Complex Event Processing, Semantic Web and Knowledge
Representation and Reasoning (KRR) [2, 3, 4, 5]. In the KRR research field, the Answer Set
Programming (ASP) declarative formalism [6, 7] has been acknowledged as a particularly
attractive basis for SR [1] and a number of SR solutions relying on ASP have been recently
proposed [8, 9, 10, 11, 12, 13, 4, 14, 15, 16]. Among these, I-DLV-sr [16] is a SR system that
efficiently scale over real-world application domains thanks to a proper integration of the well-
established stream processor Apache Flink [17] and the incremental ASP reasoner ℐ 2 -DLV [18].
Its input language, called LDSR (the Language of 𝐼 -DLV for Stream Reasoning) inherits the
highly declarative nature and ease of use from ASP, while being extended with new constructs
that are relevant for practical SR scenarios.
Although LDSR enjoys valuable knowledge modelling capabilities together with an efficient
and effective reasoner, it would be desirable to formally investigate its expressive power. This is
Datalog 2.0 2022: 4th International Workshop on the Resurgence of Datalog in Academia and Industry, September 05,
2022, Genova - Nervi, Italy
*
Corresponding author.
†
These authors contributed equally.
$ nicola.leone@unical.it (N. Leone); marco.manna@unical.it (M. Manna); maria.morelli@unical.it (M. C. Morelli);
simona.perri@unical.it (S. Perri)
© 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
Proceedings
http://ceur-ws.org
ISSN 1613-0073
CEUR Workshop Proceedings (CEUR-WS.org)
151
Nicola Leone et al. CEUR Workshop Proceedings 151–165
exactly the mission of the present paper. To this aim, the prime objective is to compare LDSR
with one of the most famous and well-studied formalisms for reasoning over streams that goes
under the name of LARS Programs (the language of LARS), where LARS is the Logic-based
framework for Analytic Reasoning over Streams [8]. More precisely, the paper investigates the
relative expressiveness of LDSR and LARS Programs. Despite the fact that these languages build
over Datalog and represent the information via sets of ASP ground predicate atoms associated
with different time points, unfortunately they overall differ both in syntax and semantics. In
particular, LDSR associates information that is true at every time point with standard ASP facts,
whereas LARS Programs involve background atoms whose truth is not directly associated with
all the time points. Moreover, given an input stream, LDSR returns a single set of information
related to the most recent time point (streaming model), whereas LARS Programs associate, for
each different time point of the stream, another stream called answer stream at that time point.
To reconcile the expressive capabilities for stream reasoning of LDSR and LARS Programs,
we first define a comparison framework that allows to understand in which cases, starting from
the same input stream, both languages may produce the same output. Inside this framework,
we identify three output profiles —called atomic, bound, and full— that fix the form of the
output stream. Without any restriction on the two languages, the paper shows that they are
incomparable under all the output profiles. Eventually, for each output profile, the paper isolates
large fragments of each of the two languages that can be expressed via the other one.
2. Preliminaries
We assume to have finite sets 𝒱, 𝒞, 𝒫 and 𝒰 consisting of variables, constants, predicate names
and 𝑡𝑖𝑚𝑒 𝑣𝑎𝑟𝑖𝑎𝑏𝑙𝑒𝑠 respectively; we constrain 𝒱 and 𝒞 to be disjoint. A term is either a variable
in 𝒱 or a constant in 𝒞. A predicate atom has the form 𝑝(𝑡1 , . . . , 𝑡𝑛 ), where 𝑝 ∈ 𝒫 is a predicate
name, 𝑡1 , . . . , 𝑡𝑛 are terms and 𝑛 ≥ 0 is the arity of the predicate atom; a predicate atom 𝑝() of
arity 0 can be also denoted by 𝑝. A predicate atom is ground if none of its terms is a variable.
We denote by 𝐺 the set of all ground predicate atoms constructible from predicate names in
𝒫 and constants in 𝒞. We divide the set of predicates 𝒫 into two disjoint subsets, namely the
extensional predicates 𝒫 𝜀 and the intensional predicates 𝒫 𝐼 . Extensional predicates are further
partitioned into 𝒫𝐵 𝜀 for background data and 𝒫 𝜀 for data streams. The mentioned partitions
𝑆
are analogously defined for ground atoms 𝐺𝐼 ,𝐺𝜀𝐵 and 𝐺𝜀𝑆 . In what follows we will introduce
different types of constructs peculiar to the two languages considered in this paper. In both,
given a set of constructs 𝐶, we will denote by 𝑝𝑟𝑒𝑑(𝐶) the set of predicates appearing in 𝐶.
A stream Σ is a sequence of sets of ground predicate atoms ⟨𝑆0 , . . . , 𝑆𝑛 ⟩ such that for
0 ≤ 𝑖 ≤ 𝑛, 𝑆𝑖 ⊆ 𝐺. Each natural number 𝑖 is called time point. A ground predicate atom 𝑎 ∈ 𝑆𝑖
is true at the 𝑖-th time point. Given a value 𝑚 ∈ N s.t. 0 ≤ 𝑚 ≤ 𝑛, we define the restriction of
Σ to 𝑚 the stream ⟨𝑆0 , . . . , 𝑆𝑚 ⟩ denoted
⋃︀ with Σ|𝑚 . Moreover, let 𝐹 ⊆ 𝒫 we indicate with Σ|𝐹
the stream ⟨𝑆0′ , . . . , 𝑆𝑛′ ⟩ with 𝑆𝑖′ = {𝑎∈𝑆𝑖 |𝑝𝑟𝑒𝑑(𝑎)∈𝐹 } 𝑎 for each 𝑖 ∈ {0, . . . , 𝑛}. A subset of a
stream Σ = ⟨𝑆0 , . . . , 𝑆𝑛 ⟩ is a stream Σ′ = ⟨𝑆0′ , . . . , 𝑆𝑛′ ⟩ such that 𝑆𝑖′ = ∅ for each 𝑖 ̸∈ 𝑡(Σ′ )
where 𝑡(Σ′ ) is a subset of consecutive numbers of the set {0, . . . , 𝑛} and for each 𝑖 ∈ 𝑡(Σ′ )
𝑆𝑖′ ⊆ 𝑆𝑖 . For a stream Σ = ⟨𝑆0 , . . . , 𝑆𝑛 ⟩, a backward observation identifies ground predicate
atoms that are true at some time points preceding the 𝑛-th time point. More formally, given
152
Nicola Leone et al. CEUR Workshop Proceedings 151–165
a stream Σ = ⟨𝑆0 , . . . , 𝑆𝑛 ⟩ and a set of numbers 𝐷 ⊂ N, we define the backward observation
of Σ w.r.t. 𝐷 as the family of sets {𝑆𝑖 | 𝑖 = 𝑛 − 𝑑 with 𝑑 ∈ 𝐷 ∧ 𝑖 ≥ 0}, and we denote it as
𝑂(Σ, 𝐷). Given 𝑤 ∈ N, a backward observation of Σ w.r.t. {0, . . . , 𝑤} is called window.
2.1. LARS syntax and semantics
A window function is a function 𝑓𝑤 that returns, given a stream Σ and a time point 𝑡 ∈ {1, ..., 𝑛},
a substream of Σ. We consider only time-based window functions, which select all the atoms
appearing in the last 𝑤 time points, to which a window is trivially associated according to
the definition above. Given a predicate atom 𝑎, a term 𝑡 ∈ 𝑁 ∪ 𝒰 and a window function 𝑓𝑤 ,
formulas 𝛼 are defined by the following grammar:
𝛼 ::= 𝑎 | ¬𝛼 | 𝛼 ∧ 𝛼 | 𝛼 ∨ 𝛼 | 𝛼 → 𝛼 | ◇ 𝛼 | □𝛼 | @𝑡 𝛼 | ⊞𝑓𝑤 𝛼 | ◁ 𝛼.
A LARS program P is a set of rules of the form 𝛼 ← 𝛽1 , . . . , 𝛽𝑛 , where 𝛼, 𝛽1 , . . . , 𝛽𝑛 are
formulas. Given a rule 𝑟, we call 𝛼 the head of 𝑟, denoted with 𝐻(𝑟), and we call the conjunction
𝛽1 ∧ · · · ∧ 𝛽𝑛 the body of 𝑟, denoted with 𝐵(𝑟). A ground formula can be satisfied at a time
point 𝑡 in a 𝑠𝑡𝑟𝑢𝑐𝑡𝑢𝑟𝑒 that is a triple 𝑀 = (Σ, 𝑊, 𝐵) where Σ is a stream, 𝑊 is a set of window
functions and 𝐵 ⊆ 𝐺𝜀𝐵 . Let Σ′ ⊆ Σ, we start defining the entailment relation ⊩ between
(𝑀, Σ′ , 𝑡) and formulas:
• 𝑀, Σ′ , 𝑡 ⊩ 𝑎 iff 𝑎 ∈ 𝑆𝑡 or 𝑎 ∈ 𝐵
• 𝑀, Σ′ , 𝑡 ⊩ ¬𝛼 iff 𝑀, 𝑡 ̸⊩ 𝛼
• 𝑀, Σ′ , 𝑡 ⊩ 𝛼 ∧ 𝛽 iff 𝑀, 𝑡 ⊩ 𝛼 and 𝑀, 𝑡 ⊩ 𝛽
• 𝑀, Σ′ , 𝑡 ⊩ 𝛼 ∨ 𝛽 iff 𝑀, 𝑡 ⊩ 𝛼 or 𝑀, 𝑡 ⊩ 𝛽
• 𝑀, Σ′ , 𝑡 ⊩ 𝛼 → 𝛽 iff 𝑀, 𝑡 ̸⊩ 𝛼 or 𝑀, 𝑡 ⊩ 𝛽
• 𝑀, Σ′ , 𝑡 ⊩ ◇𝛼 iff 𝑀, Σ′ , 𝑡 ⊩ 𝛼 for some 𝑡′ ∈ 𝑡(Σ′ )
• 𝑀, Σ′ , 𝑡 ⊩ □𝛼 iff 𝑀, Σ′ , 𝑡 ⊩ 𝛼 for all 𝑡′ ∈ 𝑡(Σ′ ) ,
• 𝑀, Σ′ , 𝑡 ⊩ @𝑡′ 𝛼 iff 𝑀, Σ′ , 𝑡′ ⊩ 𝛼 and 𝑡′ ∈ 𝑡(Σ′ ) ,
• 𝑀, Σ′ , 𝑡 ⊩ ⊞𝑓𝑤 𝛼, iff 𝑀, Σ′′ , 𝑡 ⊩ 𝛼 where Σ′′ = 𝑓𝑤 (Σ′ , 𝑡),
• 𝑀, Σ′ , 𝑡 ⊩ ◁𝛼 iff 𝑀, Σ, 𝑡 ⊩ 𝛼.
The structure 𝑀 = (Σ, 𝑊, 𝐵) satisfies 𝛼 at time 𝑡 (𝑀, 𝑡 |= 𝛼) if 𝑀, Σ′ , 𝑡 ⊩ 𝛼. Given a ground
LARS program 𝑃 , a stream Σ and a structure 𝑀 we say that: (𝑖) 𝑀 is a model of rule 𝑟 ∈ 𝑃 for
𝐼 at time 𝑡, denoted 𝑀, 𝑡 |= 𝑟, if 𝑀, 𝑡 |= 𝐵(𝑟) → 𝐻(𝑟); (𝑖𝑖) 𝑀 is a model of 𝑃 for 𝐼 at time
𝑡, denoted 𝑀, 𝑡 |= 𝑃 , if 𝑀, 𝑡 |= 𝑟 for all rules 𝑟 ∈ 𝑃 ; (𝑖𝑖𝑖) 𝑀 is a minimal model, if no model
𝑀 ′ = (Σ′ , 𝑊, 𝐵) of 𝑃 for 𝐼 at time 𝑡 exists such that Σ′ ⊂ Σ and 𝑡(Σ) = 𝑡(Σ′ ); and (𝑖𝑣) The
reduct of a program 𝑃 with respect to 𝑀 at time 𝑡 is defined by 𝑃 𝑀,𝑡 = {𝑟 ∈ 𝑃 |𝑀, 𝑡 |= 𝐵(𝑟)}.
Fixed an input stream 𝐼, contains only atoms belong to 𝐺𝜀𝑆 , we call 𝑖𝑛𝑡𝑒𝑟𝑝𝑟𝑒𝑡𝑎𝑡𝑖𝑜𝑛 𝑠𝑡𝑟𝑒𝑎𝑚
𝑓 𝑜𝑟 𝐼 any stream Σ such that all atoms that occur in Σ but not in 𝐼 have intensional predicates.
An interpretation stream Σ for a stream 𝐼 is an 𝑎𝑛𝑠𝑤𝑒𝑟 𝑠𝑡𝑟𝑒𝑎𝑚 of a program 𝑃 𝑓 𝑜𝑟 𝐼 𝑎𝑡 𝑡, if
𝑀 = (Σ, 𝑊, 𝐵) is a ⊆-minimal model of the reduct 𝑃 𝑀,𝑡 for 𝐼 at time 𝑡. The semantics of the
non-ground programs is given by the answer streams of according groundings, obtained by
replacing variables with constants from 𝒞, respectively time points from 𝑡(Σ), in all possible
ways. We consider LARS programs with a single answer stream for each time point, denoted
with LARSD , and we indicate the single answer stream of 𝑃 for 𝐼 at 𝑡 with 𝐴𝑆(𝑃, 𝐼, 𝑡).
153
Nicola Leone et al. CEUR Workshop Proceedings 151–165
Table 1
Entailment of ground streaming literals.
𝛼 Σ |= 𝛼 Σ |= not 𝛼
𝑎 at least 𝑐 in {𝑑1 , . . . , 𝑑𝑚 } |{𝐴 ∈ 𝑂(Σ, 𝐷) : 𝑎 ∈ 𝐴}| ≥ 𝑐 |{𝐴 ∈ 𝑂(Σ, 𝐷) : 𝑎 ∈ 𝐴}| < 𝑐
𝑎 always in {𝑑1 , . . . , 𝑑𝑚 } ∀𝐴 ∈ 𝑂(Σ, 𝐷), 𝑎 ∈ 𝐴 ∃𝐴 ∈ 𝑂(Σ, 𝐷) : 𝑎 ̸∈ 𝐴
𝑎 count 𝑐 in {𝑑1 , . . . , 𝑑𝑚 } |{𝐴 ∈ 𝑂(Σ, 𝐷) : 𝑎 ∈ 𝐴}| = 𝑐 |{𝐴 ∈ 𝑂(Σ, 𝐷) : 𝑎 ∈ 𝐴}| =
̸ 𝑐
2.2. LDSR syntax and semantics
Given a predicate atom 𝑎, a term 𝑐 ∈ 𝒞 ∩ N+ , a counting term 𝑡 ∈ (𝒞 ∩ N+ ) ∪ 𝒱, and a finite
non-empty set 𝐷 = {𝑑1 , . . . , 𝑑𝑚 } ⊂ N, we define three types of streaming atoms:
𝑎 at least 𝑐 in {𝑑1 , . . . , 𝑑𝑚 } | 𝑎 always in {𝑑1 , . . . , 𝑑𝑚 } | 𝑎 count 𝑡 in {𝑑1 , . . . , 𝑑𝑚 }
In particular, if 𝐷 is of the form {0, ..., 𝑤}, then this set can be alternatively written as [𝑤]
inside streaming atoms; also we may write 𝑎 in place of 𝑎 at least 1 in [0]. A streaming
atom 𝛼 (resp., not 𝛼) is said to be a positive streaming literal (resp., negative streaming literal),
where not denotes negation as failure. A streaming literal is said to be harmless if it has form
𝑎 at least 𝑐 in 𝐷 or 𝑎 always in 𝐷; otherwise, it is said to be non-harmless. A streaming
literal is said to be ground if none of its terms is a variable.
A rule is a formula of form (1) 𝑎 : - 𝑙1 , . . . , 𝑙𝑏 . or (2) #temp 𝑎 : - 𝑙1 , . . . , 𝑙𝑏 ., where 𝑎 is
a predicate atom, 𝑏 ≥ 0 and 𝑙1 , . . . , 𝑙𝑏 represent a conjunction of literals (streaming literals or
other literals defined in the ASP-Core-2 standard [19]).
For a rule 𝑟, we say that the head of 𝑟 is the set 𝐻(𝑟) = {𝑎}, whereas the set 𝐵(𝑟) =
{𝑙1 , . . . , 𝑙𝑏 } is referred to as the body of 𝑟. A rule 𝑟 is safe if all variables in 𝐻(𝑟) or in a negative
streaming literal of 𝐵(𝑟) also appear in a positive streaming literal of 𝐵(𝑟).
A program 𝑃 is a finite set of safe rules. We denote with form (1) (𝑃 ) the set of rules of 𝑃 of
form (1) and with form (2) (𝑃 ) the set of rules of 𝑃 of form (2).
A program 𝑃 is stratified if there is a partition of disjoint sets of rules 𝑃 = Π1 ∪ · · · ∪ Π𝑘
(called strata) such that for 𝑖 ∈ {1, . . . , 𝑘} both these conditions hold: (𝑖) for each harmless
literal in the body of a rule in Π𝑖 with predicate 𝑝, {𝑟 ∈ 𝑃 |𝐻(𝑟) = {𝑝(𝑡1 , . . . , 𝑡𝑛 )}} ⊆ 𝑖𝑗=1 Π𝑗 ;
⋃︀
(𝑖𝑖) for each non-harmless literal in the body of a rule in Π𝑖 with predicate 𝑝, {𝑟 ∈ 𝑃 |𝐻(𝑟) =
{𝑝(𝑡1 , . . . , 𝑡𝑛 )}} ⊆ 𝑖−1 𝑗=1 𝑗 . We call Π1 , . . . , Π𝑘 a stratification for 𝑃 and 𝑃 is stratified by
⋃︀
Π
Π1 , . . . , Π𝑘 . An LDSR program is a program being also stratified.
A backward observation allows to define the truth of a ground streaming literal at a given
time point. Given a stream Σ = ⟨𝑆0 , . . . , 𝑆𝑛 ⟩, 𝐷 = {𝑑1 , . . . , 𝑑𝑚 } ⊂ N, 𝑐 ∈ 𝒞 ∖ {0} and the
backward observation 𝑂(Σ, 𝐷), Table 1 reports when Σ entails a ground streaming atom 𝛼
(denoted Σ |= 𝛼) or its negation (Σ |= not 𝛼). If Σ |= 𝛼 ( Σ |= not 𝛼) we say that 𝛼 is true
(false) at time point 𝑛.
To make a comparison between LARSD and LDSR, we defined also for LDSR a model-theoretic
semantics that can be shown to be equivalent to the operational semantics originally defined.
Moreover, besides the concept of streaming model for LDSR, we defined the concept of answer
stream.
154
Nicola Leone et al. CEUR Workshop Proceedings 151–165
Consider an LDSR program 𝑃 . Given a rule 𝑟 ∈ 𝑃 , the ground instantiation 𝐺𝑟(𝑟) of 𝑟
denotes the set of rules obtained by applying all possible substitutions 𝜎 from the variables in
𝑟 to elements of 𝒞. In particular, to the counting terms are applied ⋃︀ only constants belong to
𝒞 ∩ N+ . Similarly, the ground instantiation 𝐺𝑟(𝑃 ) of 𝑃 is the set 𝑟∈𝑃 𝐺𝑟(𝑟). Given a ground
rule 𝑟 ∈ 𝑃 , a stream Σ = ⟨𝑆0 , . . . , 𝑆𝑛 ⟩ and a stream Σ′ = ⟨𝑆0′ , . . . , 𝑆𝑛′ ⟩ such that Σ ⊆ Σ′ , we
say that Σ′ is a model of 𝑟 for Σ, denoted Σ′ |= 𝑟, if Σ′ |= 𝐻(𝑟) when Σ′ |= 𝐵(𝑟). We say that
Σ′ is a model of 𝑃 for Σ, denoted Σ′ |= 𝑃 , if Σ′ |= 𝑟 for all rules 𝑟 ∈ 𝐺𝑟(𝑃 ). Moreover, Σ′ is a
minimal model, if no model Ω of 𝑃 exists such that Ω ⊂ Σ′ and 𝑡(Ω) = 𝑡(Σ′ ). Let Σ′ be a model
of 𝑃 for Σ, an atom 𝑎 ∈ 𝑆𝑛′ is temporary in Σ′ if 𝑎 ̸∈ 𝑆𝑛 and there exists no rule 𝑟 ∈ form (1) (𝑃 )
such that Σ′ |= 𝐵(𝑟) and Σ′ |= 𝐻(𝑟). Accordingly, let 𝑇 (𝑆𝑛′ ) be the set of all temporary atoms
in 𝑆𝑛′ , the stream ⟨𝑆0′ , . . . , 𝑆𝑛′ ∖ 𝑇 (𝑆𝑛′ )⟩ is called the permanent part of Σ′ . Eventually, the reduct
′
of 𝑃 w.r.t. Σ′ , denoted by 𝑃 Σ , consists of the rules 𝑟 ∈ 𝐺𝑟(𝑃 ) such that Σ′ |= 𝐵(𝑟).
Definition 1. Given an LDSR program 𝑃 , a stream Σ = ⟨𝑆0 , . . . , 𝑆𝑛 ⟩ and a stream Σ′ =
⟨𝑆0′ , . . . , 𝑆𝑛′ ⟩ such that Σ ⊆ Σ′ , Σ′ is called answer stream and 𝑆𝑛′ streaming model of 𝑃 for Σ if:
(1) if 𝑛 > 0, ⟨𝑆0′ ⟩ is the permanent part of the minimal model 𝑀 of the reduct 𝑃 𝑀 for the stream
⟨𝑆0 ⟩; (2) if 𝑛 > 0, for all 𝑖 ∈ 1, . . . , 𝑛 − 1, Σ′|𝑖 is the permanent part of the minimal model 𝑀
of the reduct 𝑃 𝑀 for the stream ⟨𝑆0′ , . . . , 𝑆𝑖−1 ′ , 𝑆 ⟩; and (3) Σ′ is a minimal model of the reduct
𝑖
Σ ′ ′ ′
𝑃 for the stream ⟨𝑆0 , . . . , 𝑆𝑛−1 , 𝑆𝑛 ⟩.
Note that, differently from LARS, for which the information associated with each time point
is entirely derived at the time point of evaluation, for LDSR, each time point 𝑡 in the answer
stream is associated with the information derived when the time point 𝑡 has been evaluated. In
other words, the answer stream for LDSR is obtained by collecting the results of the previous
time points and integrating them with the result of the time point of evaluation.
3. Framework
In this section, we present the framework that has been designed for comparing the languages
LARSD and LDSR. The comparison focuses on different parts of the answer stream. In particular,
given an input stream 𝑆 = ⟨𝑆0 , . . . , 𝑆𝑛 ⟩, when referring to an evaluation time point 𝑡 ≤ 𝑛,
one could compare the answer streams only at 𝑡, or in all the time points up to 𝑡 or also in
all time points up to 𝑛. To this aim, we define three types of streams. Given 𝑛 ∈ N and
𝑡 ∈ {0, . . . , 𝑛}, we say that a stream 𝑆 = ⟨𝑆0 , . . . , 𝑆𝑛 ⟩ is of 𝑡𝑦𝑝𝑒 𝑡-𝑎𝑡𝑜𝑚𝑖𝑐 if 𝑆𝑖 = ∅ for each
𝑖 ∈ {0, . . . , 𝑛} ∖ {𝑡}; 𝑡-𝑏𝑜𝑢𝑛𝑑 if 𝑆𝑖 = ∅ for each 𝑖 ∈ {𝑡 + 1, . . . , 𝑛}; and 𝑡-full if 𝑆𝑖 may be
nonempty for each 𝑖 ∈ {0, . . . , 𝑛}.
Consider a language 𝐿 ∈ {LDSR, LARSD }, an input stream 𝐼 = ⟨𝐼0 , . . . , 𝐼𝑛 ⟩, a set of ground
predicate atoms 𝐵 ⊆ 𝐺𝜀𝐵 and a program 𝑃 ∈ 𝐿, we call (𝐼, 𝐵, 𝑃 ) an 𝐿-tuple. According to the
three types of streams, for a 𝐿-tuple and for each time point 𝑡 ∈ {0, . . . , 𝑛}, we now define
three types of output streams for each language 𝐿.
Given a LDSR-𝑡𝑢𝑝𝑙𝑒 (𝐼, 𝐵, 𝑃 ) and a time point 𝑡 ∈ {0, . . . , 𝑛}, we define:
• 𝑡-𝑎𝑡𝑜𝑚𝑖𝑐(𝐼, 𝐵, 𝑃 ) = ⟨𝑂0 , . . . , 𝑂𝑛 ⟩ where 𝑂𝑖 = ∅ for 𝑖 ̸= 𝑡 and 𝑂𝑡 is the streaming
model of 𝑃 ∪ {𝑏.|𝑏 ∈ 𝐵} on 𝐼|𝑡 = ⟨𝐼0 , . . . , 𝐼𝑡 ⟩.
155
Nicola Leone et al. CEUR Workshop Proceedings 151–165
• 𝑡-𝑏𝑜𝑢𝑛𝑑(𝐼, 𝐵, 𝑃 ) = ⟨𝑂0 , . . . , 𝑂𝑛 ⟩, where ⟨𝑂0 , . . . , 𝑂𝑡 ⟩ is the answer stream of 𝑃 ∪
{𝑏.|𝑏 ∈ 𝐵} for 𝐼|𝑡 = ⟨𝐼0 , . . . , 𝐼𝑡 ⟩ and 𝑂𝑖 = ∅ for 𝑡 < 𝑖 ≤ 𝑛.
• 𝑡-full (𝐼, 𝐵, 𝑃 ) = ⟨𝑂0 , . . . , 𝑂𝑛 ⟩ where ⟨𝑂0 , . . . , 𝑂𝑡 ⟩ is the answer stream of 𝑃 ∪ {𝑏.|𝑏 ∈
𝐵} for 𝐼|𝑡 = ⟨𝐼0 , . . . , 𝐼𝑡 ⟩ and 𝑂𝑖 = 𝐼𝑖 ∪ 𝐵 for 𝑡 < 𝑖 ≤ 𝑛.
Analogously, given a LARSD -𝑡𝑢𝑝𝑙𝑒 (𝐼, 𝐵, 𝑃 ) and a time point 𝑡 ∈ {0, . . . , 𝑛}, and the answer
stream 𝐴𝑆(𝑃, 𝐼, 𝑡) = ⟨𝐴0 , . . . , 𝐴𝑛 ⟩, we define:
• 𝑡-𝑎𝑡𝑜𝑚𝑖𝑐(𝐼, 𝐵, 𝑃 ) = ⟨𝑂0 , . . . , 𝑂𝑛 ⟩ where 𝑂𝑖 = ∅ for 𝑖 ̸= 𝑡 and 𝑂𝑡 = 𝐴𝑡 ∪ 𝐵.
• 𝑡-𝑏𝑜𝑢𝑛𝑑(𝐼, 𝐵, 𝑃 ) = ⟨𝑂0 , . . . , 𝑂𝑛 ⟩, where 𝑂𝑖 = 𝐴𝑖 ∪ 𝐵 for 0 ≤ 𝑖 ≤ 𝑡 and 𝑂𝑖 = ∅ for
𝑡 < 𝑖 ≤ 𝑛.
• 𝑡-full (𝐼, 𝐵, 𝑃 ) = ⟨𝑂0 , . . . , 𝑂𝑛 ⟩ where 𝑂𝑖 = 𝐴𝑖 ∪ 𝐵 for 0 ≤ 𝑖 ≤ 𝑛.
We now define when a fragment of a language can be expressed in the other one in our
framework. In particular, we differentiate expressible fragments from strictly expressible
fragments. Given a stream form 𝜑 ∈ {𝑎𝑡𝑜𝑚𝑖𝑐, 𝑏𝑜𝑢𝑛𝑑, full },and 𝐿1 , 𝐿2 ∈ {LDSR, LARSD } with
𝐿1 ̸= 𝐿2 , a fragment 𝐹 ⊂ 𝐿1 is 𝜑-𝑒𝑥𝑝𝑟𝑒𝑠𝑠𝑖𝑏𝑙𝑒 via 𝐿2 if there exists a mapping 𝜌 : 𝐹 → 𝐿2 such
that, for each 𝐹 -tuple (𝐼, 𝐵, 𝑃 ) and for each time point of evaluation 𝑡 ∈ {0, . . . , 𝑛}, it holds
that 𝑡-𝜑(𝐼, 𝐵, 𝑃 ) = 𝑡-𝜑(𝐼, 𝐵, 𝜌(𝑃 ))|𝑝𝑟𝑒𝑑(𝑃 ∪𝐼∪𝐵) ; moreover, 𝐹 is 𝑠𝑡𝑟𝑖𝑐𝑡𝑙𝑦 𝜑-𝑒𝑥𝑝𝑟𝑒𝑠𝑠𝑖𝑏𝑙𝑒 via 𝐿2
if 𝑡-𝜑(𝐼, 𝐵, 𝑃 ) = 𝑡-𝜑(𝐼, 𝐵, 𝜌(𝑃 )). Basically, for the non strict expressiveness, a translation into
the other language is possible but it can involve the addition of auxiliary predicates, while for
the strict one, there is a translation that does not require auxiliary predicates and thus for which
the outputs coincide without the need of any filtering.
We are now ready to compare the two languages. The first result of the comparison is that,
without any restrictions, the two languages are incomparable. The following two propositions
describe the results. The ideas behind the formal demonstrations, which are instead reported in
Appendix B [20], are also introduced.
Proposition 1. LARSD is not 𝑎𝑡𝑜𝑚𝑖𝑐-𝑒𝑥𝑝𝑟𝑒𝑠𝑠𝑖𝑏𝑙𝑒 via LDSR.
To see this, consider the simple LARSD program 𝑃1 ={@𝑇 −1 𝑎 ← @𝑇 𝑐.}. This program, that
expresses that the presence of an atom 𝑐 in a time point infers the presence of an atom 𝑎 in the
previous time point, is not expressible in LDSR since in its semantic the information associated
at every time point are relative only to the information received and inferred up to it.
Proposition 2. LDSR is not 𝑎𝑡𝑜𝑚𝑖𝑐-𝑒𝑥𝑝𝑟𝑒𝑠𝑠𝑖𝑏𝑙𝑒 via LARSD .
To prove this result, consider the following LDSR program 𝑃2 = {𝑎(𝑌 ) : - 𝑎(𝑋), 𝑏(𝑋, 𝑌 ).}
where the predicate 𝑎 belongs to the input predicates 𝒫𝑆𝜀 . The program 𝑃2 is not expressible in
LARSD since its semantics avoids to infer ground atoms over input predicates.
Since 𝑡-𝑎𝑡𝑜𝑚𝑖𝑐(𝐼, 𝐵, 𝑃 ) ̸= 𝑡-𝑎𝑡𝑜𝑚𝑖𝑐(𝐼, 𝐵, 𝜌(𝑃 )) implies 𝑡-𝜑(𝐼, 𝐵, 𝑃 ) = 𝑡-𝜑(𝐼, 𝐵, 𝜌(𝑃 ))
holds for 𝜑 ∈ {𝑏𝑜𝑢𝑛𝑑, full }, Proposition 1 and 2 imply the following result.
Theorem 1. LARSD and LDSR are incomparable under each of the three stream forms.
156
Nicola Leone et al. CEUR Workshop Proceedings 151–165
Table 2 Table 3
LARSD to LDSR LDSR to LARSD
𝜑 strictly not strictly 𝜑 strictly not strictly
𝑎𝑡𝑜𝑚𝑖𝑐 𝐹1 𝐹1 𝑎𝑡𝑜𝑚𝑖𝑐 𝐹6 ∪ 𝐹7 𝐹4
𝑏𝑜𝑢𝑛𝑑 𝐹2 𝐹2 𝑏𝑜𝑢𝑛𝑑 𝐹 6 ∪ 𝐹7 𝐹4
full 𝐹3 𝐹3 full 𝐹6 𝐹5
LARS LDSR
F1 F4
F7
F5
F2
F6
F3
(a) LARS fragments (b) LDSR fragments
Figure 1: Fragments and their relations
Given the incomparability of the languages, we introduced some restrictions to identify
fragments of a language expressible in the other. Up to now, we identified seven fragments
that are described in detail in sections 3.1 and 3.2. Here, we briefly discuss their relations and
expressiveness (see Fig. 1 and Tables 2 and 3). In particular, Table 2 presents the fragments of
LARSD 𝐹1 , 𝐹2 and 𝐹3 . All of them are strictly expressible via LDSR. 𝐹1 is the largest identified
fragment and it is atomic-expressible; 𝐹2 is obtained from 𝐹1 by imposing some restriction and
it is bound-expressible, while 𝐹3 is obtained by further restricting 𝐹2 , and allows for achieving
full-expressivity.
As for LDSR, Table 3 summarizes its identified fragments 𝐹4 ,𝐹5 ,𝐹6 and 𝐹7 . The largest
fragment is 𝐹4 , which is bound-expressible via LARSD ; the fragment 𝐹5 , that restricts 𝐹4 , allows
full expressiveness; the other two fragments allows for strictly expressiveness: 𝐹6 further
restricts 𝐹5 , and it is full-expressible, while 𝐹7 is obtained by imposing restrictions on 𝐹4 and is
bound-expressible.
3.1. LARSD to LDSR
Here we present the identified fragments of LARSD . We consider two types of rules:
(𝐼) □(𝑎 ← 𝛽1 ∧ · · · ∧ 𝛽𝑏 ) and (II ) 𝑎 ← 𝛽1 , . . . , 𝛽𝑏
where 𝑎 is an intensional predicate atom and 𝛽𝑖 ∈ {⊞𝑚 ♢𝑝, ⊞𝑚 □𝑝, 𝑝, ⊞0 @𝑇 ⊤ ∧ @𝑇 −𝐾 𝑝,
¬ ⊞𝑚 ♢𝑝, ¬ ⊞𝑚 □𝑝, ¬𝑝, ¬(⊞0 @𝑇 ⊤ ∧ @𝑇 −𝐾 𝑝)|𝑝 is a predicate atom, 𝑇 ∈ 𝒰 and 𝑚 ∈ N}
157
Nicola Leone et al. CEUR Workshop Proceedings 151–165
for 𝑖 ∈ {1, . . . , 𝑏}. For a rule of type (𝐼), we denote as 𝑐𝑜𝑛𝑠(𝑟) the consequent {𝑎} of the
implication, and with 𝑝𝑟𝑒𝑚(𝑟) the set of formulas {𝛽1 , . . . , 𝛽𝑏 } in the premise; moreover, for a
rule of type (II ), we denote with ℎ𝑒𝑎𝑑(𝑟) the atom {𝑎} and with 𝑏𝑜𝑑𝑦(𝑟) the set of formulas
{𝛽1 , . . . , 𝛽𝑏 }. Let 𝑃 be a LARSD program, we denote with 𝑡𝑦𝑝𝑒𝐼 (𝑃 ) the set of rules of 𝑃 of type
(𝐼) and with 𝑡𝑦𝑝𝑒II (𝑃 ) the set of rules of 𝑃 of type (II ).
We say that a predicate 𝑝 is marked if there are two rules 𝑟 ∈ 𝑡𝑦𝑝𝑒𝐼 (𝑃 ) and 𝑟′ ∈ 𝑡𝑦𝑝𝑒II (𝑃 )
with 𝑝 = 𝑝𝑟𝑒𝑑(𝑐𝑜𝑛𝑠(𝑟)), ℎ ∈ 𝑝𝑟𝑒𝑑(𝑝𝑟𝑒𝑚(𝑟)) and ℎ = 𝑝𝑟𝑒𝑑(ℎ𝑒𝑎𝑑(𝑟′ )). The set of marked
predicates of a program 𝑃 is denoted with 𝑀 (𝑃 ).
Consider a LARSD program 𝑃 containing rules of type (𝐼) and (II ) only. Let 𝑃1 =
𝑡𝑦𝑝𝑒𝐼 (𝑃 ) and 𝑃2 = 𝑡𝑦𝑝𝑒II (𝑃 ). We define the graph 𝐺(𝑃 ) = ⟨𝑁, 𝐴⟩, where: (1) 𝑁 =
(∪𝑟∈𝑃1 𝑝𝑟𝑒𝑑(𝑐𝑜𝑛𝑠(𝑟))) ∪ (∪𝑟∈𝑃2 𝑝𝑟𝑒𝑑(ℎ𝑒𝑎𝑑(𝑟))); (2) (𝑞, 𝑝, “+”) ∈ 𝐴 if there exists a rule 𝑟 ∈ 𝑃1
with 𝑝𝑟𝑒𝑑(𝑐𝑜𝑛𝑠(𝑟)) = 𝑝 and 𝑞 ∈ 𝑝𝑟𝑒𝑑(𝑝𝑟𝑒𝑚(𝑟)) occurring in a formula without negation
or if there exists a rule 𝑟′ ∈ 𝑃2 with 𝑝𝑟𝑒𝑑(ℎ𝑒𝑎𝑑(𝑟′ )) = 𝑝 and 𝑞 ∈ 𝑝𝑟𝑒𝑑(𝑏𝑜𝑑𝑦(𝑟′ )) occurring
in a formula without negation; and (3) (𝑞, 𝑝, “-”) ∈ 𝐴 if there exists a rule 𝑟 ∈ 𝑃1 with
𝑝𝑟𝑒𝑑(𝑐𝑜𝑛𝑠(𝑟)) = 𝑝 and 𝑞 ∈ 𝑝𝑟𝑒𝑚(𝑟) occurs in a formula with negation or if there exists a
rule 𝑟′ ∈ 𝑃2 with 𝑝𝑟𝑒𝑑(ℎ𝑒𝑎𝑑(𝑟′ )) = 𝑝 and 𝑞 ∈ 𝑝𝑟𝑒𝑑(𝑏𝑜𝑑𝑦(𝑟′ )) occurring in a formula with
negation.
Definition 2. Fragment 𝐹1 of LARSD collects all the programs 𝑃 that meet the next condi-
tions: (𝑖) 𝑃 = 𝑡𝑦𝑝𝑒𝐼 (𝑃 ) ∪ 𝑡𝑦𝑝𝑒II (𝑃 ); (𝑖𝑖) ∪𝑟∈𝑡𝑦𝑝𝑒𝐼 (𝑃 ) 𝑝𝑟𝑒𝑑(𝑝𝑟𝑒𝑚(𝑟)) ∩ 𝑀 (𝑃 ) = ∅; (𝑖𝑖𝑖)
∪𝑟∈𝑡𝑦𝑝𝑒II (𝑃 ) 𝑝𝑟𝑒𝑑(𝑏𝑜𝑑𝑦(𝑟)) ∩ 𝑀 (𝑃 ) = ∅; (𝑖𝑣) no cycle in 𝐺(𝑃 ) contains an arc labeled with “-".
Roughly, 𝐹1 contains only programs that are stratified w.r.t negation, featuring only rules of
types (I) and (II), where no marked predicate appears in premises and in bodies.
Proposition 3. 𝐹1 is strictly atomic-expressible via LDSR.
Indeed, it can be shown that there is a mapping 𝜌1 : 𝐹1 → LDSR such that for each 𝐹1 -𝑡𝑢𝑝𝑙𝑒
(𝐼, 𝐵, 𝑃 ) and for each time point of evaluation 𝑡 ∈ {0, . . . , 𝑛}, it holds that 𝑡-𝑎𝑡𝑜𝑚𝑖𝑐(𝐼, 𝐵, 𝑃 ) =
𝑡-𝑎𝑡𝑜𝑚𝑖𝑐(𝐼, 𝐵, 𝜌1 (𝑃 )). In particular, given a program 𝑃 ∈ 𝐹1 , the LDSR program 𝜌1 (𝑃 ) is
obtained by replacing:
- each rule □(𝑎 ← 𝛽1 , . . . , 𝛽𝑚 ) of type (𝐼) with the LDSR rule 𝑎 : - 𝑓 (𝛽1 ), . . . , 𝑓 (𝛽𝑚 ) of
form (1)
- each rule 𝑎 ← 𝛽1 , . . . , 𝛽𝑚 of type (𝐼𝐼) with the LDSR rule
#temp 𝑎 : - 𝑓 (𝛽1 ), . . . , 𝑓 (𝛽𝑚 ) of form (2)
where 𝑓 associates each LARSD formula in the 𝐹1 fragment with a LDSR streaming atom as
reported below:
- 𝑓 (⊞𝑚 ♢𝑝) = 𝑝 in [𝑚].
- 𝑓 (⊞𝑚 □𝑝) = 𝑝 always in [𝑚].
- 𝑓 (𝑝) = 𝑝.
- 𝑓 (⊞0 @𝑇 ⊤ ∧ @𝑇 −𝐾 𝑝) = 𝑝 in {𝑘}.
- 𝑓 (¬𝛽) = not 𝑓 (𝛽) where 𝛽 is a formula.
158
Nicola Leone et al. CEUR Workshop Proceedings 151–165
Intuitively, the idea of the mapping 𝜌1 is that LARSD rules of type (𝐼) that must be evaluated
at each time point are associated with 𝐿𝐷𝑅𝑆 rules of form (1) and LARSD rules of type (II )
that infer information only at the evaluation time point 𝑡 are associate with LDSR rules of form
(2) which are evaluated at each time point but the derivations of the time points preceding 𝑡
have been forgotten via the #temp operator. Moreover, we impose the restrictions (𝑖𝑖) and
(𝑖𝑖𝑖) for defining 𝐹1 in order to achieve atomic-expressiveness; indeed, they ensure that, if in
LDSR a permanent information is derived relying on a temporary information, this is not used
to derive other information.
Now, we define the fragment 𝐹2 that imposes an additional restriction w.r.t to 𝐹1 , and the
fragment 𝐹3 that further restricts 𝐹2 .
Definition⋃︀3. The fragment 𝐹2 of LARSD is⋃︀the subset of the programs of 𝐹1 that meet the
condition ( 𝑟∈𝑡𝑦𝑝𝑒II (𝑃 ) 𝑝𝑟𝑒𝑑(ℎ𝑒𝑎𝑑(𝑟))) ∩ (( 𝑟∈𝑡𝑦𝑝𝑒𝐼 (𝑃 ) 𝑝𝑟𝑒𝑑(𝑝𝑟𝑒𝑚(𝑟)) = ∅.
Proposition 4. 𝐹2 is strictly bound-expressible via LDSR.
It can be shown that for the mapping 𝜌2 = 𝜌1 |𝐹 , it holds that for each 𝐹2 -𝑡𝑢𝑝𝑙𝑒 (𝐼, 𝐵, 𝑃 ) and for
2
each time point of evaluation 𝑡 ∈ {0, . . . , 𝑛}, 𝑡-𝑏𝑜𝑢𝑛𝑑(𝐼, 𝐵, 𝑃 ) = 𝑡-𝑏𝑜𝑢𝑛𝑑(𝐼, 𝐵, 𝜌2 (𝑃 )). Basi-
cally, the additional condition for fragment 𝐹2 avoids that a temporary information associated
to a time point can generate a permanent information.
We now show an example of a program belonging to fragment 𝐹2 and its image with respect
to the function 𝜌2 . The example is taken from one of the tasks of the “model and solve” Stream
Reasoning Hackathon 2021 [21]. The task concerns urban traffic management. Traffic is
observed from a top-down, third-person perspective, and vehicle movement flows in a given
road network coded as Datalog facts are considered. We want to identify the vehicles that
appear or disappear in the network. It is then necessary to note vehicles that were absent at the
previous time point and are now present and vice versa. A rule of type (𝐼) is used to evaluate
the presence of vehicles at the current and previous time points; then the obtained information
is used in a rule of type (II ) that detects the appearance or disappearance of a vehicle at the
evaluation time point. This task can be modelled via the following program 𝑃 in 𝐹2 :
□(𝑖𝑛𝑁 𝑒𝑡𝑤𝑜𝑟𝑘(𝑉 𝑒ℎ) ← 𝑜𝑛𝐿𝑎𝑛𝑒(𝑉 𝑒ℎ, 𝑋, 𝑌 )).
𝑎𝑝𝑝𝑒𝑎𝑟𝑠(𝑉 𝑒ℎ) ← 𝑜𝑛𝐿𝑎𝑛𝑒(𝑉 𝑒ℎ, 𝑋, 𝑌 ), ¬ ⊞0 @𝑇 ⊤ ∧ @𝑇 −1 𝑖𝑛𝑁 𝑒𝑡𝑤𝑜𝑟𝑘(𝑉 𝑒ℎ).
𝑑𝑖𝑠𝑎𝑝𝑝𝑒𝑎𝑟𝑠(𝑉 𝑒ℎ) ← ⊞0 @𝑇 ⊤ ∧ @𝑇 −1 𝑖𝑛𝑁 𝑒𝑡𝑤𝑜𝑟𝑘(𝑉 𝑒ℎ), ¬𝑖𝑛𝑁 𝑒𝑡𝑤𝑜𝑟𝑘(𝑉 𝑒ℎ).
The corresponding LDSR program, image of the 𝜌2 function, is:
𝑖𝑛𝑁 𝑒𝑡𝑤𝑜𝑟𝑘(𝑉 𝑒ℎ) : - 𝑜𝑛𝐿𝑎𝑛𝑒(𝑉 𝑒ℎ, 𝑋, 𝑌 ).
#temp 𝑎𝑝𝑝𝑒𝑎𝑟𝑠(𝑉 𝑒ℎ) : - 𝑜𝑛𝐿𝑎𝑛𝑒(𝑉 𝑒ℎ, 𝑋, 𝑌 ), not 𝑖𝑛𝑁 𝑒𝑡𝑤𝑜𝑟𝑘(𝑉 𝑒ℎ) in {1}.
#temp 𝑑𝑖𝑠𝑎𝑝𝑝𝑒𝑎𝑟𝑠(𝑉 𝑒ℎ) : - 𝑜𝑛𝐿𝑎𝑛𝑒(𝑉 𝑒ℎ, 𝑋, 𝑌 ) in {1}, not 𝑖𝑛𝑁 𝑒𝑡𝑤𝑜𝑟𝑘(𝑉 𝑒ℎ).
Definition 4. The fragment 𝐹3 of LARSD is the subset of the programs of 𝐹2 that meet the
condition 𝑃 = 𝑡𝑦𝑝𝑒II (𝑃 ).
159
Nicola Leone et al. CEUR Workshop Proceedings 151–165
Proposition 5. 𝐹3 is strictly full-expressible via LDSR.
Similarly to 𝐹2 , it can be shown that, considering the mapping 𝜌3 = 𝜌1 |𝐹 , it holds that that for
3
each 𝐹3 -𝑡𝑢𝑝𝑙𝑒 (𝐼, 𝐵, 𝑃 ) and for each time point of evaluation 𝑡 ∈ {0, . . . , 𝑛}, 𝑡-full (𝐼, 𝐵, 𝑃 ) =
𝑡-full (𝐼, 𝐵, 𝜌3 (𝑃 )). Intuitively, since in LDSR the evaluation of a program with respect to a
time point 𝑡 can not add information in the output stream at time points that are subsequent to
𝑡, to achieve full expressiveness, we impose the restriction to rules of type type (II ) in LARSD
as these are evaluated only at 𝑡 and do not change the output in the subsequent time points.
3.2. LDSR to LARSD
Here we present the identified fragments of LDSR along with their expressiveness. While, for
the fragments of LARSD we obtained strict expressiveness and each rule in LARSD has been
translated into exactly one rule in LDSR, for the fragments of LDSR, the translation, in general,
needs auxiliary atoms and additional rules to simulate the behavior of rules of the form (2) and
of some streaming and aggregates atoms.
The largest identified fragment is 𝐹4 that is defined as follows.
Definition 5. The fragment 𝐹4 is the subset of the LDSR programs 𝑃 that meet the condition
⊂ 𝒫𝐼.
⋃︀
𝑟∈𝑃 𝑝𝑟𝑒𝑑(𝐻(𝑟))
Basically, 𝐹4 is obtained from LDSR by simply imposing that no extensional predicate appears
in the head of a rule.
Proposition 6. 𝐹4 is bound-expressible via LARSD .
It can be shown that there is a mapping 𝜌4 : 𝐹4 → LARSD such that for each 𝐹4 -𝑡𝑢𝑝𝑙𝑒 (𝐼, 𝐵, 𝑃 )
and for each 𝑡 ∈ {0, . . . , 𝑛}, 𝑡-𝑏𝑜𝑢𝑛𝑑(𝐼, 𝐵, 𝑃 ) = 𝑡-𝑏𝑜𝑢𝑛𝑑(𝐼, 𝐵, 𝜌4 (𝑃 ))|𝑝𝑟𝑒𝑑(𝑃 ∪𝐼∪𝐵) . First, we
note that, in general, each streaming atom in 𝐹4 has to properly translated into a LARSD formula;
moreover a special rewriting, requiring additional rules, has to be performed for streaming atoms
of the form 𝑎 count 𝑣 in {𝑑1 , . . . , 𝑑𝑚 }, where 𝑣 is a variable in 𝒞 and for all the aggregate
atoms. Thus, without going into details, the mapping 𝜌4 relies on a function 𝑔 that associates
each streaming atom (but those of form 𝑎 count 𝑣 in {𝑑1 , . . . , 𝑑𝑚 }) with a LARSD formula that
expresses the condition that must be satisfied in the stream for the streaming atom to be true;
moreover, if 𝛼 is an aggregate atom or a streaming atom of the form 𝑎 count 𝑣 in {𝑑1 , . . . , 𝑑𝑚 },
𝑔 associates it with a formula containing auxiliary atoms defined via an additional set of rules
𝐶𝛼 that are needed to simulate its semantics. For the sake of the presentation, the function 𝑔
and the set of additional rules 𝐶𝛼 are reported in Appendix A.1 [20].
Furthermore, given a program 𝑃 ∈ 𝐹4 , the mapping 𝜌4 has to replace each rule 𝑟 in 𝑃 with
one or more LARSD rules. In sum, the program 𝜌4 (𝑃 ) is obtained by:
- replacing each rule 𝑎 : - 𝛽1 , . . . , 𝛽𝑚 of form (1) with the LARSD rule □(𝑎 ← ⊞0 @𝑇 ⊤ ∧
𝑔(𝛽1 ) ∧ · · · ∧ 𝑔(𝛽𝑚 )).
- for each rule #temp 𝑎 : - 𝛽1 , . . . , 𝛽𝑚 of form (2),
- replacing it with the LARSD rule 𝑎 ← ⊞0 @𝑇 ⊤, 𝑔(𝛽1 ), . . . , 𝑔(𝛽𝑚 )
160
Nicola Leone et al. CEUR Workshop Proceedings 151–165
- adding the rule □(𝑎𝑡𝑒𝑚𝑝 ← ⊞0 @𝑇 ⊤ ∧ 𝑔(𝛽1 ) ∧ · · · ∧ 𝑔(𝛽𝑚 )).
- adding for each streaming atom 𝛼 of the form 𝑎 count 𝑣 in {𝑑1 , . . . , 𝑑𝑚 }, where 𝑣 is a
variable in 𝒞 or aggregates atom, a set of rules 𝐶𝛼 .
Basically, the mapping 𝜌4 manages the interaction between the two forms of rules, simulating,
at an evaluation time point 𝑡, the temporary derivations obtained in the previous time points
and evaluating their effect on the permanent derivations that will be part of the output. This
is mainly obtained by creating and handling a copy of each rule of the form (2) where the
suffix “temp” is added to the head predicate. Moreover, since the streaming atoms in LDSR are
evaluated according to the backward observation, we need to identify the reference time point
in which the 𝐿𝐴𝑅𝑆 formulas representing the conditions expressed by the streaming atoms
have to checked. To do this, we use the formula ⊞0 @𝑇 ⊤ that evaluates the tautology within a
window of size 0 and thus, it holds in the rule instance where the variable 𝑇 corresponds to the
reference time point.
We are now ready to define the fragment 𝐹5 that is obtained from 𝐹4 by avoiding rules of
form (1).
Definition 6. The fragment 𝐹5 of LDSR is the subset of the programs of 𝐹4 that meet the condition
𝑃 = form 2 (𝑃 ).
Proposition 7. 𝐹5 is full -𝑒𝑥𝑝𝑟𝑒𝑠𝑠𝑖𝑏𝑙𝑒 via LARSD .
To see this, consider, the mapping 𝜌5 : 𝐹5 → LARSD such that, for each program 𝑃 ∈ 𝐹5 , 𝜌5 (𝑃 )
is obtained by:
- replacing each rule #temp 𝑎 : - 𝛽1 , . . . , 𝛽𝑚 of form (2) , with the LARSD rule 𝑎 ←
⊞0 @𝑇 ⊤, 𝑔 ′ (𝛽1 ), . . . , 𝑔 ′ (𝛽𝑚 ).
- adding for each streaming atom 𝛼 of the form 𝑎 count 𝑣 in {𝑑1 , . . . , 𝑑𝑚 }, where 𝑣 is a
variable in 𝒞 or aggregates atom, a set of rules 𝐶𝛼 .
It can be shown that 𝜌5 is such that for each 𝐹5 -𝑡𝑢𝑝𝑙𝑒 (𝐼, 𝐵, 𝑃 ) and for each 𝑡 ∈ {0, . . . , 𝑛},
𝑡-full (𝐼, 𝐵, 𝑃 ) = 𝑡-full (𝐼, 𝐵, 𝜌5 (𝑃 ))|𝑝𝑟𝑒𝑑(𝑃 ∪𝐼∪𝐵) . Roughly, similarly to 𝜌4 , 𝜌5 relies on a func-
tion 𝑔 ′ for rewriting body atoms and adds auxiliary rules for handling aggregate atoms or a
streaming atoms of the form 𝑎 count 𝑣 in {𝑑1 , . . . , 𝑑𝑚 } (more details on this are reported in
Appendix A.2 [20]); however the translation for the fragment 𝐹5 is simpler than the one for
𝐹4 , as it is sufficient to associate each rule of form (2) with a LARSD rule of type (II). Indeed,
since rules of form (1) are not allowed, there is no need to consider the information that can be
derived in a permanent way through them. The condition defining the fragment 𝐹5 ensures
the full expressiveness: since a program in this fragment features only rules of form (2), and its
translation only rules of type (II), their evaluation at each time point 𝑡 can derive information
only at 𝑡, while leaving unchanged the output in the other time points.
The fragment 𝐹6 restrict 𝐹5 to reach strict full expressiveness.
Definition 7. The fragment 𝐹6 of LDSR is the subset of the programs of 𝐹5 in which streaming
atoms of the form 𝑎 count 𝑣 in {𝑑1 , . . . , 𝑑𝑚 } where 𝑣 ∈ 𝑉 and aggregate atoms are not allowed
in rule bodies.
161
Nicola Leone et al. CEUR Workshop Proceedings 151–165
Proposition 8. 𝐹6 is strictly full-expressible via LARSD .
It can be shown that for the mapping 𝜌6 = 𝜌5 |𝐹 , it holds that for each 𝐹6 -𝑡𝑢𝑝𝑙𝑒 (𝐼, 𝐵, 𝑃 ) and
6
for each 𝑡 ∈ {0, . . . , 𝑛}, 𝑡-full (𝐼, 𝐵, 𝑃 ) = 𝑡-full (𝐼, 𝐵, 𝜌6 (𝑃 )). Since no atoms involving the
addition of auxiliary predicates are considered, 𝐹6 is strictly expressible.
The last considered fragment 𝐹7 still features strict expressiveness, but of bound type, as,
differently from 𝐹6 , it allows also rules of form (1) to some extent.
Definition 8. The fragment 𝐹7 of LDSR is the subset of the programs of 𝐹4 that meet the following
conditions: (𝑖) (∪𝑟∈form 2 (𝑃 ) (𝑝𝑟𝑒𝑑(𝐵(𝑟)))∩(∪𝑟∈form2 (P ) (𝑝𝑟𝑒𝑑(𝐻(𝑟))) = ∅ (𝑖𝑖) streaming atoms
of the form 𝑎 count 𝑣 in {𝑑1 , . . . , 𝑑𝑚 } where 𝑣 ∈ 𝑉 and aggregate atoms are not allowed in
rule bodies.
Proposition 9. 𝐹7 is strictly bound-expressible via LARSD .
It can be shown that there is a mapping 𝜌7 : 𝐹7 → LARSD such that for each 𝐹7 -𝑡𝑢𝑝𝑙𝑒 (𝐼, 𝐵, 𝑃 )
and for each 𝑡 ∈ {0, . . . , 𝑛}, 𝑡-𝑏𝑜𝑢𝑛𝑑(𝐼, 𝐵, 𝑃 ) = 𝑡-𝑏𝑜𝑢𝑛𝑑(𝐼, 𝐵, 𝜌7 (𝑃 )). To see this, consider,
the mapping 𝜌7 : 𝐹7 → LARSD such that, for each program 𝑃 ∈ 𝐹7 , 𝜌7 (𝑃 ) is obtained by:
- replacing each rule #temp 𝑎 : - 𝛽1 , . . . , 𝛽𝑚 of form (2) with the LARSD rule 𝑎 ←
⊞0 @𝑇 ⊤, 𝑔 ′ (𝛽1 ), . . . , 𝑔 ′ (𝛽𝑚 ).
- replacing each rule 𝑎 : - 𝛽1 , . . . , 𝛽𝑚 of form (1) with the LARSD rule □(𝑎 ← ⊞0 @𝑇 ⊤ ∧
𝑔 ′′ (𝛽1 ) ∧ · · · ∧ 𝑔 ′′ (𝛽𝑚 ))
The mapping relies on the same function 𝑔 ′ as 𝜌5 for the rules of form (2). In addition, for the
rule of form (1), a different function 𝑔 ′′ is used to associate the body streaming atoms with
𝐿𝐴𝑅𝑆 formulas based on the following definition.
Definition 9. Given an atom 𝑎(𝑡1 , . . . , 𝑡𝑛 ) and a LDSR rule 𝑟 with 𝐻(𝑟) = 𝑎(𝑡′1 , . . . , 𝑡′𝑛 )
we
⋀︀ call definition of 𝑎(𝑡1 , . . . , 𝑡𝑛 ) in 𝑟, denoted with 𝑑𝑟 (𝑎(𝑡1 , . . . , 𝑡𝑛 )), the conjunction
′
⋀︀
{𝛽∈𝐵(𝑟)} 𝛽 1≤𝑖≤𝑛 𝑡𝑖 = 𝑡𝑖 . Given an⋁︀ LDSR program 𝑃 the definition of 𝑎(𝑡1 , . . . , 𝑡𝑛 ) in 𝑃
is 𝑑𝑃 (𝑎(𝑡1 , . . . , 𝑡𝑛 )) = 𝑎(𝑡1 , . . . , 𝑡𝑛 ) ∨ ( {𝑟∈𝑃 |𝑝𝑟𝑒𝑑(𝐻(𝑟))=𝑎} 𝑑𝑟 (𝑎(𝑡1 , . . . , 𝑡𝑛 ))).
This definition identifies, for each predicate 𝑎 in the head of a rule of form (2), a 𝐿𝐴𝑅𝑆 formula
relying only on permanent information that can be used in the 𝐿𝐴𝑅𝑆 translation in place of
𝑎. Further details on the translation and the 𝑔 ′′ functions are reported in Appendix A.3 [20].
We note here that the strict expressiveness of this fragment is obtained since the translation of
the allowed streaming atoms does not require the use of additional atoms, and condition (𝑖𝑖)
simplifies the rewriting of the rules of form (2) w.r.t what fragment 𝐹4 . Indeed, in this case, it is
not necessary to add the rules used by 𝜌4 such as □(𝑎𝑡𝑒𝑚𝑝 ← ⊞0 @𝑇 ⊤ ∧ 𝑔(𝛽1 ) ∧ · · · ∧ 𝑔(𝛽𝑚 ))
that required additional auxiliary atoms.
Consider, for example, the LDSR program 𝑃 ′ that could be used for monitoring irregularity in
a subway station monitoring system. Three minutes are expected to elapse between the arrival
of one train and the next, so the program records an irregularity when one train passes and
another has already passed in one of the previous two minutes:
𝑃 ′ = {𝑖𝑟𝑟𝑒𝑔𝑢𝑙𝑎𝑟 : - 𝑡𝑟𝑎𝑖𝑛_𝑝𝑎𝑠𝑠, 𝑡𝑟𝑎𝑖𝑛_𝑝𝑎𝑠𝑠 at least 1 in {1, 2}.}
162
Nicola Leone et al. CEUR Workshop Proceedings 151–165
The program belongs to the 𝐹7 fragment, and the corresponding LARSD program with respect
to the 𝜌7 function is as follows:
𝜌7 (𝑃 ′ ) = {□(𝑖𝑟𝑟𝑒𝑔𝑢𝑙𝑎𝑟 ← ⊞0 @𝑇 ⊤ ∧ (@𝑇1 𝑡𝑟𝑎𝑖𝑛_𝑝𝑎𝑠𝑠 ∧ 𝑇1 = 𝑇 − 0)
∧ (@𝑇2 𝑡𝑟𝑎𝑖𝑛_𝑝𝑎𝑠𝑠 ∧ ((𝑇2 = 𝑇 − 1) ∨ (𝑇2 = 𝑇 − 2))).}
4. Conclusion
This work presents a formal comparison about the relative expressiveness of the two languages
LDSR and LARS. The main contribution of the work is twofold: (𝑖) we propose a suitable
framework to compare the two languages, which exhibit different syntax and semantics. and
(𝑖𝑖) for each language, we identify a number of fragments that can be expressed by the other
one, showing possible rewritings. In order to compare the semantics of the two languages, we
first provided an alternative equivalent model-theoretic definition of the semantics of LDSR,
instead of the operational one originally provided. Moreover, we defined the concept of answer
stream also for LDSR, as an extension of the streaming model. The framework allowed us for
focusing the comparison on different forms of the output stream (atomic, bound, full) and on
the nature of the rewriting that could forbid or admit the addition of auxiliary predicates (strict
or not strict expressiveness, respectively). For each given form of output and type of rewriting,
we studied how to build fragments of a language that could meet the desired expressiveness. To
do this, we considered the semantics behind each construct or combination of constructs that
can occur in the rules and the effect of interactions between the different rules. The fragments
𝐹1 , ..., 𝐹7 are the largest we identified so far, but, of course, these could be further enlarged and
new ones could be possibly found; this will be the subject of future works.
Acknowledgments
This work has been partially supported by the project “MAP4ID - Multipurpose Analytics
Platform 4 Industrial Data”, N. F/190138/01-03/X44 and by the Italian MIUR Ministry and the
Presidency of the Council of Ministers under the project “Declarative Reasoning over Streams"
under the “PRIN" 2017 call (CUP 𝐻24𝐼17000080001, project 2017M9C25L_001).
References
[1] D. Dell’Aglio, E. D. Valle, F. van Harmelen, A. Bernstein, Stream reasoning: A survey and
outlook, Data Sci. 1 (2017) 59–83. URL: https://doi.org/10.3233/DS-170006. doi:10.3233/
DS-170006.
[2] D. F. Barbieri, D. Braga, S. Ceri, E. D. Valle, M. Grossniklaus, C-SPARQL: a continuous
query language for RDF data streams, Int. J. Semantic Comput. 4 (2010) 3–25. URL:
https://doi.org/10.1142/S1793351X10000936. doi:10.1142/S1793351X10000936.
[3] J. Hoeksema, S. Kotoulas, High-performance distributed stream reasoning using s4, in:
Ordring Workshop at ISWC, 2011.
163
Nicola Leone et al. CEUR Workshop Proceedings 151–165
[4] T. Pham, M. I. Ali, A. Mileo, C-ASP: continuous asp-based reasoning over RDF streams,
in: M. Balduccini, Y. Lierler, S. Woltran (Eds.), Logic Programming and Nonmonotonic
Reasoning - 15th International Conference, LPNMR 2019, Philadelphia, PA, USA, June 3-7,
2019, Proceedings, volume 11481 of Lecture Notes in Computer Science, Springer, 2019, pp.
45–50. doi:10.1007/978-3-030-20528-7\_4.
[5] D. L. Phuoc, M. Dao-Tran, J. X. Parreira, M. Hauswirth, A native and adaptive ap-
proach for unified processing of linked streams and linked data, in: L. Aroyo, C. Welty,
H. Alani, J. Taylor, A. Bernstein, L. Kagal, N. F. Noy, E. Blomqvist (Eds.), The Seman-
tic Web - ISWC 2011 - 10th International Semantic Web Conference, Bonn, Germany,
October 23-27, 2011, Proceedings, Part I, volume 7031 of Lecture Notes in Computer Sci-
ence, Springer, 2011, pp. 370–388. URL: https://doi.org/10.1007/978-3-642-25073-6_24.
doi:10.1007/978-3-642-25073-6\_24.
[6] G. Brewka, T. Eiter, M. Truszczynski, Answer set programming at a glance, Communica-
tions of the ACM 54 (2011) 92–103. doi:10.1145/2043174.2043195.
[7] M. Gebser, N. Leone, M. Maratea, S. Perri, F. Ricca, T. Schaub, Evaluation techniques
and systems for answer set programming: a survey, in: J. Lang (Ed.), Proceedings of the
Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July
13-19, 2018, Stockholm, Sweden, ijcai.org, 2018, pp. 5450–5456. URL: https://doi.org/10.
24963/ijcai.2018/769. doi:10.24963/ijcai.2018/769.
[8] H. Beck, M. Dao-Tran, T. Eiter, LARS: A logic-based framework for analytic reasoning over
streams, Artif. Intell. 261 (2018) 16–70. URL: https://doi.org/10.1016/j.artint.2018.04.003.
doi:10.1016/j.artint.2018.04.003.
[9] H. R. Bazoobandi, H. Beck, J. Urbani, Expressive stream reasoning with laser, in:
C. d’Amato, M. Fernández, V. A. M. Tamma, F. Lécué, P. Cudré-Mauroux, J. F. Se-
queda, C. Lange, J. Heflin (Eds.), The Semantic Web - ISWC 2017 - 16th International
Semantic Web Conference, Vienna, Austria, October 21-25, 2017, Proceedings, Part I,
volume 10587 of Lecture Notes in Computer Science, Springer, 2017, pp. 87–103. URL:
https://doi.org/10.1007/978-3-319-68288-4_6. doi:10.1007/978-3-319-68288-4\_6.
[10] H. Beck, M. Dao-Tran, T. Eiter, C. Folie, Stream reasoning with LARS, Künstliche In-
tell. 32 (2018) 193–195. URL: https://doi.org/10.1007/s13218-018-0537-9. doi:10.1007/
s13218-018-0537-9.
[11] T. Eiter, P. Ogris, K. Schekotihin, A distributed approach to LARS stream reasoning
(system paper), Theory Pract. Log. Program. 19 (2019) 974–989. URL: https://doi.org/10.
1017/S1471068419000309. doi:10.1017/S1471068419000309.
[12] X. Ren, O. Curé, H. Naacke, G. Xiao, Bigsr: real-time expressive RDF stream reasoning on
modern big data platforms, in: N. Abe, H. Liu, C. Pu, X. Hu, N. K. Ahmed, M. Qiao, Y. Song,
D. Kossmann, B. Liu, K. Lee, J. Tang, J. He, J. S. Saltz (Eds.), IEEE International Conference
on Big Data (IEEE BigData 2018), Seattle, WA, USA, December 10-13, 2018, IEEE, 2018,
pp. 811–820. URL: https://doi.org/10.1109/BigData.2018.8621947. doi:10.1109/BigData.
2018.8621947.
[13] A. Mileo, A. Abdelrahman, S. Policarpio, M. Hauswirth, Streamrule: A nonmonotonic
stream reasoning system for the semantic web, in: W. Faber, D. Lembo (Eds.), Web
Reasoning and Rule Systems - 7th International Conference, RR 2013, Mannheim, Ger-
many, July 27-29, 2013. Proceedings, volume 7994 of Lecture Notes in Computer Sci-
164
Nicola Leone et al. CEUR Workshop Proceedings 151–165
ence, Springer, 2013, pp. 247–252. URL: https://doi.org/10.1007/978-3-642-39666-3_23.
doi:10.1007/978-3-642-39666-3\_23.
[14] T. M. Do, S. W. Loke, F. Liu, Answer set programming for stream reasoning, in: C. J.
Butz, P. Lingras (Eds.), Advances in Artificial Intelligence - 24th Canadian Conference on
Artificial Intelligence, Canadian AI 2011, St. John’s, Canada, May 25-27, 2011. Proceedings,
volume 6657 of Lecture Notes in Computer Science, Springer, 2011, pp. 104–109. URL: https:
//doi.org/10.1007/978-3-642-21043-3_13. doi:10.1007/978-3-642-21043-3\_13.
[15] M. Gebser, T. Grote, R. Kaminski, T. Schaub, Reactive answer set programming, in: J. P.
Delgrande, W. Faber (Eds.), Logic Programming and Nonmonotonic Reasoning - 11th
International Conference, LPNMR 2011, Vancouver, Canada, May 16-19, 2011. Proceedings,
volume 6645 of Lecture Notes in Computer Science, Springer, 2011, pp. 54–66. URL: https:
//doi.org/10.1007/978-3-642-20895-9_7. doi:10.1007/978-3-642-20895-9\_7.
[16] F. Calimeri, M. Manna, E. Mastria, M. C. Morelli, S. Perri, J. Zangari, I-dlv-sr: A stream
reasoning system based on I-DLV, Theory Pract. Log. Program. 21 (2021) 610–628. URL:
https://doi.org/10.1017/S147106842100034X. doi:10.1017/S147106842100034X.
[17] P. Carbone, A. Katsifodimos, S. Ewen, V. Markl, S. Haridi, K. Tzoumas, Apache flink™:
Stream and batch processing in a single engine, IEEE Data Eng. Bull. 38 (2015) 28–38. URL:
http://sites.computer.org/debull/A15dec/p28.pdf.
[18] G. Ianni, F. Pacenza, J. Zangari, Incremental maintenance of overgrounded logic programs
with tailored simplifications, Theory Pract. Log. Program. 20 (2020) 719–734. URL: https:
//doi.org/10.1017/S147106842000040X. doi:10.1017/S147106842000040X.
[19] F. Calimeri, W. Faber, M. Gebser, G. Ianni, R. Kaminski, T. Krennwallner, N. Leone,
M. Maratea, F. Ricca, T. Schaub, Asp-core-2 input language format, TPLP 20 (2020) 294–309.
URL: https://doi.org/10.1017/S1471068419000450. doi:10.1017/S1471068419000450.
[20] N. Leone, M. Manna, M. C. Morelli, S. Perri, A formal comparison between datalog-based
languages for stream reasoning (extended version), 2022. URL: https://arxiv.org/abs/2208.
12726. doi:10.48550/ARXIV.2208.12726.
[21] P. Schneider, D. Alvarez-Coello, A. Le-Tuan, M. N. Duc, D. L. Phuoc, Stream reasoning
playground, in: P. Groth, M. Vidal, F. M. Suchanek, P. A. Szekely, P. Kapanipathi, C. Pesquita,
H. Skaf-Molli, M. Tamper (Eds.), The Semantic Web - 19th International Conference, ESWC
2022, Hersonissos, Crete, Greece, May 29 - June 2, 2022, Proceedings, volume 13261 of
Lecture Notes in Computer Science, Springer, 2022, pp. 406–424. URL: https://doi.org/10.
1007/978-3-031-06981-9_24. doi:10.1007/978-3-031-06981-9\_24.
165