atl short = ATL, long = Allen’s Temporal Logic, short-indefinite = an, long-
indefinite = an ,foreign-plural= cfg short = CFG, long = Context-Free Grammar
,foreign-plural= hs short = HS, long = Halpern and Shoham’s logic of
intervals, short-indefinite = an ,foreign-plural= hdc short = HDC, long =
Hybrid Duration Calculus, short-indefinite = an ,foreign-plural= rv short =
RV, long = Runtime Verification, short-indefinite = an ,foreign-plural= jpl
short = JPL, long = Jet Propulsion Laboratory ,foreign-plural=
11institutetext:  Queen’s University, Canada
11email<EMAIL_ADDRESS>22institutetext: Aalborg University, Denmark
22email<EMAIL_ADDRESS>
# The Complexity of Data-Free Nfer

Sean Kauffman 11 Kim Guldstrand Larsen 22 Martin Zimmermann 22

###### Abstract

Nfer is a Runtime Verification language for the analysis of event traces that
applies rules to create hierarchies of time intervals. This work examines the
complexity of the evaluation and satisfiability problems for the data-free
fragment of nfer. The evaluation problem asks whether a given interval is
generated by applying rules to a known input, while the satisfiability problem
asks if an input exists that will generate a given interval.

By excluding data from the language, we obtain polynomial-time algorithms for
the evaluation problem and for satisfiability when only considering inclusive
rules. Furthermore, we show decidability for the satisfiability problem for
cycle-free specifications and undecidability for satisfiability of full data-
free nfer.

###### Keywords:

Interval Logic Complexity Runtime Verification

##  1 Introduction

Nfer is an interval logic for analyzing and comprehending event traces that
has been used in a wide range of applications, from anomaly detection in
autonomous vehicles [14] to spacecraft telemetry analysis [17]. However, its
high complexity demands that users restrict the features they incorporate into
their applications to ensure tractability. Despite this, no work exists that
examines the runtime complexity of nfer without data; an obvious restraint on
the power of the language that more closely resembles propositional interval
logics like hs and Duration Calculus [25]. These languages still tend to be
undecidable in the general case, however, so it is unclear if this restriction
on nfer helps with tractability. In this paper, we show that evaluation of the
data-free variant of nfer is tractable and, futhermore, satisfiability for
this variant is tractable with additional restrictions.

Nfer is rv language for the analysis of event traces, developed by scientists
from NASA’s jpl in collaboration with other researchers [18, 16, 17]. In nfer,
specifications consist of rules that describe and label relationships between
time periods called intervals. Applying nfer rules to an event trace yields a
hierarchy of these intervals that is easier for humans and machines to
comprehend than the raw events.

Nfer typically operates on intervals with data, but here we define a data-free
fragment of the language. Data-free nfer is expressive enough for many use
cases, having appeared, for example, to analyze the Sequential Sense-Process-
Send (SSPS) dataset [17]. Data-free nfer is also the target for an algorithm
to mine rules from real-time embedded systems [15].

Recent work analyzing the evaluation complexity of nfer has shown that full
language is undecidable, with various decidable fragments [19, 20]. These
fragments mostly remain intractable, however, with PTime complexity only
possible by employing a meta-constraint on the size of the results that may
not be practical in many cases. Those works did not examine data-free nfer as
a fragment, however, despite it being an obvious restriction with precedent in
the literature. A major advantage of restricting nfer to the data-free
fragment is that the satisfiability problem becomes interesting. With data, it
is trivial to show that satisfiability for nfer is undecidable. This follows
from the results in [20] where nfer is shown to have undecidable evaluation.
One can encode a Turing machine using nfer rules and satisfiability asks if
there is an initial tape such that the machine terminates.

Without data, however, it is much less obvious if satisfiability is
undecidable. In fact, we show that satisfiability for the full data-free nfer
language is still undecidable, but we achieve decidability by restricting to a
cycle-free or inclusive-only fragment, the latter of which we demonstrate is
decidable in PTime. That the satisfiability of inclusive, data-free nfer is
decidable in PTime has exciting implications for practitioners, since these
checks can be implemented in event-trace analysis tools [13]. We also show
that the evaluation problem for data-free nfer is in PTime without any
artificial restrictions on the size of the result from meta-constraints.

#### Related Work

Other works have examined the complexity of interval-based logics. Halpern et
al. introduced an interval temporal logic and examined its decidability in
[11]. Chaochen et al. found decidable and undecidable fragments of an
extension of that work, Duration Calculus [7], over both discrete and dense
time [6]. Bolander et al. later introduced hdc that added the ability to name
an interval and refer to it in a formula [4]. They showed that hdc can express
Allen’s relations and is decidable over discrete and dense time domains with
non-elementary complexity.

Other works have investigated the complexity of hs [12], a modal logic based
on atl. Montanari et al. examined the satisfiability problem for the subset of
hs over the natural numbers with only _begins/begun by_ and _meets_ operators
and proved it to be ExpSpace-complete [22]. The same authors later proved that
adding the _met by_ operator increases the complexity of the language to be
decidable only over finite total orders [21]. Aceto et al. later examined the
expressive power of all fragments of hs over total orders [1].

##  2 Data-Free Nfer

We denote the set of nonnegative integers as $\mathbb{N}$. The set of Booleans
is given as $\mathbb{B}=\\{\mathit{true},\mathit{false}\\}$. We fix a finite
alphabet $\Sigma$ of event identifiers and a finite alphabet $\mathcal{I}$ of
interval identifiers such that $\Sigma\subseteq\mathcal{I}$. A word is a
sequence of identifiers $\sigma=\sigma_{0}\sigma_{1}\cdots\sigma_{|\sigma|-1}$
where $\sigma_{i}\in\Sigma$. Given a word $\sigma$, we define the non-empty
subsequence $\sigma_{[s,e]}=\sigma_{s}\cdots\sigma_{e}$, where $0\leq s\leq
e\leq|\sigma|-1$.

An event represents a named state change in an observed system. An event is a
pair $(\eta,t)$ where $\eta\in\Sigma$ is its identifier and $t\in\mathbb{N}$
is the timestamp when it occurred. The set of all events is
$\mathbb{E}=\Sigma\times\mathbb{N}$. A trace is a sequence of events
$\tau=(\eta_{0},t_{0})(\eta_{1},t_{1})\cdots(\eta_{n-1},t_{n-1})$ where
$n=|\tau|$ and $t_{i}\leq t_{j}$ for all $i<j$.

Intervals represent a named period of state in an observed system. An interval
is a triple $(\eta,s,e)$ where $\eta\in\mathcal{I}$ is its identifier, and
$s,e\in\mathbb{N}$ are the starting and ending timestamps where $s\leq e$. We
denote the set of all intervals by $\mathbb{I}$. A set of intervals is called
a _pool_ and the set of all pools is $\mathbb{P}=2^{\mathbb{I}}$. We say that
an interval $i=(\eta,s,e)$ is labeled by $\eta$ and define the accessor
functions $\textit{id}(i)=\eta$, $\textit{start}(i)=s$, and
$\textit{end}(i)=e$. An interval of duration zero is an _atomic_ interval.

#### Syntax.

The data-free nfer syntax consists of _rules_. There are two forms of rules:
inclusive and exclusive. Inclusive rules test for the existence of two
intervals matching a temporal constraint. Exclusive rules test for the
existence of one interval and the absence of another interval matching a
temporal constraint. When such a pair is found, a new interval is produced
with an identifier specified by the rule and timestamps taken from the matched
intervals. We define the syntax of these rules as follows:

  * •

Inclusive rules have the form $\eta\leftarrow\eta_{1}\>\oplus\ \eta_{2}$ and

  * •

exclusive rules have the form $\eta\leftarrow\eta_{1}\>{\bf unless}\ominus\
\eta_{2}$

where $\eta,\eta_{1},\eta_{2}\in\mathcal{I}$ are identifiers,
$\oplus\in\\{{\bf before}{},{\bf meet}{},{\bf during}{},{\bf coincide}{},$
${\bf start}{},$ ${\bf finish}{},{\bf overlap}{},{\bf slice}{}\\}$ is a _clock
predicate_ on three intervals (one for each of $\eta,\eta_{1},\text{ and
}\eta_{2}$), and $\ominus\in\\{{\bf after}{},{\bf follow}{},{\bf
contain}{}\\}$ is a clock predicate on two intervals (one for each of
$\eta_{1}$ and $\eta_{2}$). For a rule $\eta\leftarrow\eta_{1}\>\oplus\
\eta_{2}$ or $\eta\leftarrow\eta_{1}\>{\bf unless}\ominus\ \eta_{2}$ we say
that $\eta$ appears on the left-hand and the $\eta_{i}$ appear on the right-
hand side.

#### Semantics.

The semantics of the nfer language is defined in three steps: the semantics
$R$ of individual rules on pools, the semantics $S$ of a specification (a list
of rules) on pools, and finally the semantics $T$ of a specification on traces
of events.

We first define the semantics of inclusive rules with the interpretation
function $R$. Let $\Delta$ be the set of all rules. Semantic functions are
defined using the brackets $[\\![$_$]\\!]$ around syntax being given
semantics.

⬇

$R$$[\\![$_$]\\!]$ : $\Delta$ $\rightarrow$ $\mathbb{P}$ $\rightarrow$
$\mathbb{P}$

$R$$[\\![$$\eta$ $\leftarrow$ $\eta_{1}$ $\oplus$ $\eta_{2}$$]\\!]$$\pi$ =

{ $i$ $\in$ $\mathbb{I}$ : $i_{1}$,$i_{2}$ $\in$ $\pi$ . id($i$) = $\eta$
$\wedge$id($i_{1}$) = $\eta_{1}$ $\wedge$id($i_{2}$) = $\eta_{2}$
$\wedge$$\oplus$($i$,$i_{1}$,$i_{2}$) }

In the definition, an interval $i$ is member of the produced pool when two
existing intervals in $\pi$ match the identifiers $\eta_{1}$ and $\eta_{2}$
and the temporal constraint $\oplus$. The identifier of $i$ is given in the
rule and $\oplus$ defines its start and end timestamps.

The clock predicates referenced by $\oplus$ are shown in Table 1 (and
graphically in Appendix 0.A). These relate two intervals using the familiar
atl temporal operators [2] and also specify the start and end timestamps of
the produced intervals. For the example ${\bf before}{}(i,i_{1},i_{2})$,
$i_{1}$ and $i_{2}$ are matched when $i_{1}$ ends before $i_{2}$ begins. The
generated interval $i$ has start and end timestamps inherited from the
intervals $i_{1}$ and $i_{2}$, i.e., no new timestamps are generated by
applying a rule.

Table 1: Formal definition of nfer clock predicates for inclusive rules $\oplus$ | Constraints on $i,i_{1},$ and $i_{2}$
---|---
before | $\textit{end}(i_{1})<\textit{start}(i_{2})\wedge\textit{start}(i)=\textit{start}(i_{1})\wedge\textit{end}(i)=\textit{end}(i_{2})$
meet | $\textit{end}(i_{1})=\textit{start}(i_{2})\wedge\textit{start}(i)=\textit{start}(i_{1})\wedge\textit{end}(i)=\textit{end}(i_{2})$
during | $\textit{start}(i_{2})=\textit{start}(i)\leq\textit{start}(i_{1})\wedge\textit{end}(i_{1})\leq\textit{end}(i_{2})=\textit{end}(i)$
coincide | $\textit{start}(i_{1})=\textit{start}(i_{2})=\textit{start}(i)\wedge\textit{end}(i_{1})=\textit{end}(i_{2})=\textit{end}(i)$
start |  $\textit{start}(i_{1})=\textit{start}(i_{2})=\textit{start}(i)\>\wedge$ $\textit{end}(i)=\max(\textit{end}(i_{1}),\textit{end}(i_{2}))$
finish |  $\textit{end}(i)=\textit{end}(i_{1})=\textit{end}(i_{2})\>\wedge$ $\textit{start}(i)=\min(\textit{start}(i_{1}),\textit{start}(i_{2}))$
overlap | $\textit{start}(i_{1})<\textit{end}(i_{2})\wedge\textit{start}(i_{2})<\textit{end}(i_{1})\ \wedge$
|
$\textit{start}(i)=\min(\textit{start}(i_{1}),\textit{start}(i_{2}))\wedge\textit{end}(i)=\max(\textit{end}(i_{1}),\textit{end}(i_{2}))$
slice | $\textit{start}(i_{1})<\textit{end}(i_{2})\wedge\textit{start}(i_{2})<\textit{end}(i_{1})\ \wedge$
|
$\textit{start}(i)=\max(\textit{start}(i_{1}),\textit{start}(i_{2}))\wedge\textit{end}(i)=\min(\textit{end}(i_{1}),\textit{end}(i_{2}))$

We now define the semantics of exclusive rules with the function $R$.

⬇

$R$$[\\![$$\eta$ $\leftarrow$ $\eta_{1}$ unless $\ominus$
$\eta_{2}$$]\\!]$$\pi$ =

{ $i$ $\in$ $\mathbb{I}$ : $i_{1}$ $\in$ $\pi$ . id($i$) = $\eta$
$\wedge$id($i_{1}$) = $\eta_{1}$ $\wedge$

start($i$) = start($i_{1}$) $\wedge$ end($i$) = end($i_{1}$) $\wedge$

$\neg$ ($\exists$ $i_{2}$ $\in$ $\pi$ . $i_{2}$ $\neq$ $i_{1}$
$\wedge$id($i_{2}$) = $\eta_{2}$ $\wedge$$\ominus$($i_{1}$,$i_{2}$) ) }

Like with inclusive rules, exclusive rules match intervals in the input pool
$\pi$ to produce a pool of new intervals. The difference is that exclusive
rules produce new intervals where one existing interval in $\pi$ matches the
identifier $\eta_{1}$ and no intervals exist in $\pi$ that match the
identifier $\eta_{2}$ such that the clock predicate $\ominus$ holds for the
$\eta_{1}$-labeled and the $\eta_{2}$-labeled interval.

The three possibilities referenced by $\ominus$ are shown in Table 2 (and
graphically in Appendix 0.A). These clock predicates relate two intervals
using familiar atl temporal operators while the timestamps of the produced
interval are copied from the included interval rather than being defined by
the clock predicate. For the example ${\bf after}{}(i_{1},i_{2})$, $i_{1}$ and
$i_{2}$ would be matched (if $i_{2}$ existed) if $i_{1}$ begins after $i_{2}$
ends, and this match would result in _no_ interval being produced. If such an
$i_{2}$ interval is absent, an interval is produced with timestamps matching
$i_{1}$.

Table 2: Formal definition of nfer clock predicates for exclusive rules $\ominus$ |  | Constraints on $i_{1}$ and $i_{2}$ |
---|---|---|---
after |  | $\textit{start}(i_{1})>\textit{end}(i_{2})$ |
follow |  | $\textit{start}(i_{1})=\textit{end}(i_{2})$ |
contain |  | $\textit{start}(i_{2})\geq\textit{start}(i_{1})\wedge\textit{end}(i_{2})\leq\textit{end}(i_{1})$ |

The interpretation function $S$ defines the semantics of a finite list of
rules, called a specification. Given a specification
$\delta_{1}\cdots\delta_{n}\in\Delta^{*}$ and a pool $\pi\in\mathbb{P}$,
$S[\\![\\_]\\!]\>$ recursively applies $R[\\![\\_]\\!]\>$ to the rules in
order, passing each instance the union of $\pi$ with the intervals returned by
already completed calls.

$\displaystyle S\;[\\![\\_]\\!]\ :\
\Delta^{*}\rightarrow\mathbb{P}\rightarrow\mathbb{P}$ $\displaystyle S\;[\\![\
\delta_{1}\cdots\delta_{n}\ ]\\!]\ \pi\ =\ \begin{cases}S\;[\\![\
\delta_{2}\cdots\delta_{n}\ ]\\!]\ (\,\pi\;\cup\;R\;[\\![\ \delta_{1}\ ]\\!]\
\pi\ )&\textbf{if }n>0\\\ \pi&\textbf{otherwise}\end{cases}$

An nfer specification $D\in\Delta^{*}$ forms a directed graph $G(D)$ with
vertices for the rules in $D$ connected by edges representing identifier
dependencies. An edge exists in $G(D)$ from $\delta$ to $\delta^{\prime}$ iff
there is an identifier $\eta$ that appears on the left-hand side of $\delta$
and the right-hand side of $\delta^{\prime}$. We say that $D$ contains a cycle
if $G(D)$ contains one; otherwise $D$ is cycle-free.

The rules in a cycle in an nfer specification must be iteratively evaluated
until a fixed point is reached. As intervals may never be destroyed by rule
evaluation, inclusive rules may be repeatedly evaluated, safely. However,
exclusive rules may not be evaluated until the intervals on which they depend
are known to be present or absent.

For example, suppose a specification with the following two rules:
$\delta_{1}=c\leftarrow a\>{\bf meet}{}\ b$ and $\delta_{2}=a\leftarrow
c\>{\bf meet}{}\ b$. Given a pool $\pi=\\{(a,0,1),(b,1,2),(b,2,3),$
$(b,3,4),(d,4,5)\\}$, $R[\\![\delta_{1}]\\!]\>\pi=\\{(c,0,2)\\}$ and
$R[\\![\delta_{2}]\\!]\>(\pi\cup R[\\![\delta_{1}]\\!]\>\pi)=\\{(a,0,3)\\}$.
The rules must be applied a second time to reach a fixed point that includes
the interval $(c,0,4)$. Now consider the consequences if the specification
also contained the exclusive rule $\delta_{3}=b\leftarrow d\>{\bf unless}{}\
{\bf follow}{}\ c$. After the first evaluation, $(c,0,4)$is not yet produced,
so evaluating $\delta_{3}$ would generate $(b,4,5)$, an incorrect result. As
such, _exclusive rules may not appear in cycles_ but may appear in a
specification that contains cycles among inclusive rules.

To find the cycles in a specification, we compute the strongly-connected
components of the directed graph $G(D)$ formed by the rules in $D$. Each
strongly connected component represents either a cycle or an individual rule
outside of a cycle. We then sort the components in topological order and
iterate over each component until a fixed point is reached.

The interpretation function $T[\\![\\_]\\!]\>$ defines the semantics of a
specification applied to a trace of events. To ensure consistency with prior
work and to simplify our presentation, we overload $T[\\![\\_]\\!]\>$ to
operate on an event trace ${\tau\in\mathbb{E}^{*}}$ by first converting $\tau$
to the pool $\\{\textit{init}(e):e\text{ is an element of }\tau\\}$ where
$\textit{init}(\eta,t)=(\eta,t,t)$.

⬇

$T$$[\\![$_$]\\!]$ : $\Delta^{*}$ $\rightarrow$ $\mathbb{P}$ $\rightarrow$
$\mathbb{P}$

$T$$[\\![$$\delta_{1}$ $\cdots$ $\delta_{n}$$]\\!]$$\pi$ = $\pi$ℓ+1,1 .
$\pi_{1,1}$ = $\pi$ $\wedge$

$\mathcal{D}$ = SCC($\delta_{1}$ $\cdots$ $\delta_{n}$) $\wedge$ ($D_{1}$
$\cdots$ $D_{\ell}$) = topsort($\mathcal{D}$) .

$\pi_{i+1,1}$ = $\bigcup$j>0 $\pi_{i,j}$ . $\pi_{i,j+1}$ =
$S$$[\\![$$D_{i}$$]\\!]$($\pi_{i,j}$)

where $\text{SCC}(\delta_{1}\cdots\delta_{n})$ is the set $\mathcal{D}$ of
strongly connected components of the directed graph
$G(\delta_{1}\cdots\delta_{n})$ described above and
$\textit{topsort}(\mathcal{D})$ is a topological sort of these components.

##  3 Satisfiability

We are interested in the existential nfer satisfiability problem: Given a
specification $D$, a set of identifiers $\Sigma$, and a target identifier
$\eta_{T}$, is there an input trace of events $\tau\in\mathbb{E}^{+}$ with
identifiers in $\Sigma$ such that an $\eta_{T}$-labeled interval is in
$T[\\![D]\\!]\>\tau$?

The nfer satisfiability problem is interesting in part because of the
restriction of input identifiers to $\Sigma\subseteq\mathcal{I}$. If
$\eta_{T}\in\Sigma$, then any specification is trivially satisfiable. When
$\eta_{T}\not\in\Sigma$, however, then a $\eta_{T}$-labeled interval must be
derived. This problem is non-trivial and, as we shall see, undecidable in the
general case.

To see how data-free nfer specifications may be satisfiable or not, consider
the following two example specifications for the target identifier $\eta_{T}$
and input identifiers $\Sigma=\\{a,b\\}$:

$D_{\text{sat}}=$ $\begin{cases}&A\leftarrow a\>{\bf before}{}\ b\\\
&B\leftarrow b\>{\bf meet}{}\ A\\\ &\eta_{T}\leftarrow A\>{\bf overlap}{}\
B\\\ \end{cases}$ $D_{\text{unsat}}=$ $\begin{cases}&A\leftarrow b\>{\bf
before}{}\ X\\\ &B\leftarrow a\>{\bf meet}{}\ b\\\ &\eta_{T}\leftarrow a\>{\bf
overlap}{}\ B\\\ \end{cases}$

A satisfying event trace for $D_{\text{sat}}$ is $\tau_{1}=(a,1),(b,2)$, since
$T[\\![D_{\text{sat}}]\\!]\>\tau_{1}=\\{(a,1,1),(b,2,2),(A,1,2),(B,1,2),(\eta_{T},1,2)\\}$.
For $D_{\text{unsat}}$, no $\eta_{T}$-labeled interval can be produced because
${\bf overlap}{}$ requires one of the two matched intervals to have positive
duration: for an interval $i$, $\textit{end}(i)-\textit{start}(i)>0$. Since
$a$-labeled intervals must be initial, they are atomic (zero duration). That
leaves $B$-labeled intervals produced by another rule. The rule that produces
$B$-labeled intervals, however, only matches initial intervals with the same
timestamps. As such, any $B$-labeled interval will also have zero duration,
and the ${\bf overlap}{}$ rule will never be matched. Finally, the ${\bf
before}{}$ rule can never be applied, as no $X$-labeled interval can be
generated.

###  3.1 Data-Free nfer Satisfiability is Undecidable

In this section, we show the undecidability of the data-free nfer
satisfiability problem by a reduction from the emptiness problem for the
intersection of two cfg. The undecidability result relies on the recursive
nature of nfer, i.e., an $\eta$-labeled interval can be produced from another
$\eta$-labeled interval, and on its negation capabilities, i.e., via exclusive
rules.

######  Theorem 3.1.

The data-free nfer satisfiability problem is undecidable.

We now show how to simulate cfg $G$ with data-free nfer rules with a
designated identifier $\eta_{G}$ so that a word $w$ is accepted by the cfg iff
applying the rules to events that correspond to $w$ generates an interval over
the same period with identifier $\eta_{G}$. Then the intersection of two cfg
$G_{1}$ and $G_{2}$ is nonempty if and only if applying the corresponding
rules generates, for some sequence of events corresponding to a word, two
intervals with the same starting and ending timestamps, one with identifier
$\eta_{G_{1}}$ and one with $\eta_{G_{2}}$. The existence of two such
intervals can again be captured by a data-free nfer rule producing an interval
with a target identifier.

Formally, cfg is a four-tuple $(V,\Sigma,P,S)$, where $V$ is a finite set of
non-terminals (or variables), $\Sigma$ is the finite set of terminals that are
disjoint from $V$, $P$ is a finite set of productions of the form
$v\rightarrow w$ where $v\in V$ and $w\in(V\cup\Sigma)^{*}$, and $S$ is the
initial non-terminal. We assume, without loss of generality, that a cfg is in
Chomsky-normal form [8].111Note that we, w.l.o.g., disregard the empty word.
This means that all productions are in one of two forms: $A\rightarrow BC$ or
$A\rightarrow a$ where $A,B,C\in V$, $a\in\Sigma$, and $S\notin\\{B,C\\}$.

Given a grammar $(V,\Sigma,P,S)$, where $A\in V$, $w,x,y\in(V\cup\Sigma)^{*}$,
and $(A\rightarrow x)\in P$, then we say that $wAy$ yields $wxy$, written
$wAy\Rightarrow wxy$. We write $w\ext@arrow 0359\Rightarrowfill@{}{*}y$ if
$w=y$ or there exists a sequence of strings $x_{1},x_{2},\ldots,x_{n}$ for
$n\geq 0$ such that $w\Rightarrow x_{1}\Rightarrow
x_{2}\Rightarrow\cdots\Rightarrow x_{n}\Rightarrow y$. The language of the
grammar is $\\{w\in\Sigma^{*}:S\ext@arrow 0359\Rightarrowfill@{}{*}w\\}$. If a
word is in the language of the grammar we say it has a derivation in the
grammar. Deciding if the intersection of the languages of two cfg is empty is
undecidable [3].

We use the following grammar as a running example:
$G_{\textit{x}}=(V_{\textit{x}},\Sigma_{\textit{x}},P_{\textit{x}},S_{\textit{x}})$
accepts the language $a(a^{n})(b^{n})$ where $n>0$. We define
$V_{\textit{x}}=\\{A,B,M,M^{\prime},S_{\textit{x}}\\}$,
$\Sigma_{\textit{x}}=\\{a,b\\}$, and $P_{\textit{x}}=\\{A\rightarrow
a,B\rightarrow b,S_{\textit{x}}\rightarrow AM,M\rightarrow AB,M\rightarrow
AM^{\prime},M^{\prime}\rightarrow MB\\}$. The string $aab$ has a derivation
$S_{\textit{x}}\Rightarrow AM\Rightarrow AAB\Rightarrow AAb\Rightarrow
Aab\Rightarrow aab$ in $G_{\textit{x}}$.

We present six types of data-free nfer rules to simulate the intersection of
two cfg $G=(V,\Sigma,P,S)$ and
$G^{\prime}=(V^{\prime},\Sigma,P^{\prime},S^{\prime})$, where $V\cap
V^{\prime}=\varnothing$ and $P\cap P^{\prime}=\varnothing$. The first four
steps are necessary to account for events with coincident timestamps and
because simulating cfg requires the sequential composition of non-terminals,
while nfer rules cannot perform sequential composition directly on atomic
intervals. Then the final two steps map the productions of cfg and their
intersection directly to data-free nfer rules. The six types of rules are:

  1. 1.

Rules to label non-unique timestamps in an event trace so that they can be
filtered out. We do so, because event traces in nfer are allowed to have
events with the same timestamps while there is only one letter at each
position of a word. So, to simplify our translation between event traces and
words, we just filter out events with non-unique timestamps.

  2. 2.

Rules that then perform the actual event filtering to only include events with
unique timestamps.

  3. 3.

Rules that label every interval in a trace by its starting event, i.e. where
some event occurs at the start and some other event occurs at the end, we
label the interval by the starting event.

  4. 4.

Rules that select the minimal starting-event-labeled intervals, i.e. the
intervals where no other interval is subsumed by that interval. The result of
this step is a set of contiguous intervals labeled by their starting event.
These minimal intervals are totally ordered and in one-to-one correspondence
with the original events with unique timestamps. Thus, we have transformed the
event trace into an _equivalent_ pool of intervals.

  5. 5.

Rules that simulate the productions of the cfg on the pool of minimal
starting-event-labeled intervals. Hence, the generated intervals essentially
encode a derivation tree. The word corresponding to the event trace is
accepted by cfg if an interval is generated labeled by that grammar’s initial
non-terminal.

  6. 6.

A rule that labels an interval by a given target label if the simulation of
the two cfg labeled the same interval by their initial non-terminals. The
interval is generated if the word corresponding to the same event trace is
accepted by both cfg.

Let us explain all steps in detail. We begin by relating event traces to
words. Event traces form a total preorder as some timestamps may be equal,
while the symbols in a word are totally ordered by their index (no two symbols
have the same index). To convert a word to an event trace, we add a timestamp
equal to the index of the event. Given a word $\sigma\in\Sigma^{*}$,
$\textit{TRACE}(\sigma)=(\sigma_{0},0),(\sigma_{1},1),\ldots,(\sigma_{n-1},n-1)\text{
where }n=|\sigma|$. For example, $\textit{TRACE}(aab)=(a,0),(a,1),(b,2)$.

When converting an event trace to a word, however, we must only consider
events with unique timestamps. The following example trace illustrates the
reasoning at this step: consider
$\tau_{\textit{x}}=(a,0),(a,1),(a,2),(b,2),(b,3),(b,4)$ where both an
$a$-labeled and a $b$-labeled event occur at timestamp $2$. To convert
$\tau_{\textit{x}}$ to a word, we want to order its identifiers using only
their timestamps, and, consequently, the two events with timestamp $2$ cannot
be ordered. As such, we ensure that only events with unique timestamps affect
the generation of intervals involved in simulating cfg. Before we show how to
generate those intervals we define formally what we mean by unique timestamps.

Given a trace
$\tau=(\eta_{0},t_{0}),(\eta_{1},t_{1}),\ldots,(\eta_{n-1},t_{n-1})$, $t_{i}$
is unique in $\tau$ if for all $j\neq i$ we have $t_{j}\neq t_{i}$. Let
$\textit{UNIQ}(\tau)=\\{t_{i_{0}},t_{i_{1}},\ldots,t_{i_{k-1}}\\}$ be the set
of unique timestamps in $\tau$ such that $t_{i_{j}}<t_{i_{j^{\prime}}}$ for
all $j<j^{\prime}$, i.e., we enumerate the unique timestamps of $\tau$ in
increasing order. Then,
$\textit{WORD}(\tau)=\eta_{i_{0}},\eta_{i_{1}},\ldots,\eta_{i_{k-1}}$.

We now define data-free nfer rules that capture the definition of WORD. The
rules first generate atomic SPOIL intervals where multiple events share
timestamps and then filter the events to only those that do not share
timestamps with those SPOIL intervals.

Given the alphabet $\Sigma$, we define rules to generate SPOIL intervals for
non-unique timestamps. We let SPOIL be a new identifier
($\texttt{SPOIL}\notin\Sigma$).

$D_{1}=\\{\texttt{SPOIL}\leftarrow a\>{\bf coincide}{}\
b:(a,b)\in\Sigma\times\Sigma\wedge a\neq b\\}$ (1)

For example, applying $D_{1}$ to the example trace $\tau_{\textit{x}}$ defined
above results in the following intervals:
$T[\\![D_{1}]\\!]\>(\tau_{\textit{x}})=\\{(a,0,0),(a,1,1),(a,2,2),(b,2,2),(\texttt{SPOIL},2,2),$
$(b,3,3),(b,4,4)\\}$. Figure 1 shows this example on a timeline. In the top of
the figure, the solid line shows time progressing from left to right, with the
identifiers appearing in the trace given below their associated timestamps.
The new SPOIL-labeled interval is shown below the timeline, having been
generated by the rules in $D_{1}$ shown on the right. The remainder of the
figure relates to steps 2, 3, and 4.

Figure 1: Example of applying steps 1-4 from the proof of Theorem 3.1

######  Proposition 1.

Given a trace $\tau$, $T[\\![D_{1}]\\!]\>(\tau)$ characterizes
$\textit{WORD}(\tau)$ in the following sense: $\\{t:(\texttt{SPOIL},t,t)\in
T[\\![D_{1}]\\!]\>(\tau)\\}$ is the difference between the set of timestamps
in $\tau$ and $\textit{UNIQ}(\tau)$.

Now, we can define rules that filter the events to only those with unique
timestamps by excluding any that coincide with SPOIL-labeled intervals. These
rules ensure that the nfer simulation of cfg uses exactly the same events that
are used in WORD: those with unique timestamps. Note that the intervals
generated by the rules in $D_{i}$ for steps $i\in\\{2,3,4\\}$ are labeled by
identifiers annotated by the step number ($a_{i}$) where $a\in\Sigma$ and
$a_{i}\notin V\cup V^{\prime}\cup\Sigma$.

$D_{2}=\\{a_{2}\leftarrow a\>{\bf unless}{}\ {\bf contain}{}\
\texttt{SPOIL}:a\in\Sigma\\}$ (2)

Figure 1 shows the result of applying $D_{2}$ to the result of
$T[\\![D_{1}]\\!]\>(\tau_{\textit{x}})$. The intervals $(a_{2},0,0)$ and
$(a_{2},1,1)$ annotate $a$-labeled intervals that do not coincide with a
SPOIL-labeled interval, while $(b_{2},3,3)$ and $(b_{2},4,4)$ annotate the
$b$-labeled intervals that do not coincide with a SPOIL-labeled interval. No
such annotated intervals are produced at timestamp 2, where the rules in
$D_{1}$ generated a SPOIL-labeled interval.

Recall that the intervals that result from the rules in $D_{2}$ are still
atomic, i.e. they are effectively events and have a duration of zero. The next
step is to use those atomic intervals to generate every interval in the trace
with a positive duration (restricted to those with unique starting and ending
timestamps in the original trace $\tau$). We label every such interval with a
label derived from its start.

$D_{3}=\\{a_{3}\leftarrow a_{2}\>{\bf before}{}\
b_{2}:(a,b)\in\Sigma\times\Sigma\\}$ (3)

As shown in Figure 1, the intervals generated by applying $D_{3}$ in our
example are $(a_{3},0,1)$ from the rule $a_{3}\leftarrow a_{2}\>{\bf
before}{}\ a_{2}$, $(b_{3},3,4)$ from $b_{3}\leftarrow b_{2}\>{\bf before}{}\
b_{2}$, and $(a_{3},1,3),$ $(a_{3},0,3),$ $(a_{3},1,4),$ $(a_{3},0,4)$ from
$a_{3}\leftarrow a_{2}\>{\bf before}{}\ b_{2}$.

Now, we introduce rules that filter the intervals produced by the rules in
$D_{3}$ so that only the _minimal_ intervals remain. A minimal interval is one
where no other interval (with the same label) is subsumed by it. The resulting
intervals form a contiguous sequence covering all unique timestamps in $\tau$
where their meeting points are the atomic intervals produced by $D_{2}$.

$D_{4}=\\{a_{4}\leftarrow a_{3}\>{\bf unless}{}\ {\bf contain}{}\
a_{3}:a\in\Sigma\\}$ (4)

The reason for generating this contiguous sequence of intervals is that we
need to transform the input into elements that are _sequentially composable_
using data-free nfer rules. To understand why, recall our example event trace:
$\tau_{\textit{x}}=(a,0),(a,1),(a,2),(b,2),(b,3),(b,4)$. As seen in Figure 1,
the atomic intervals that result from applying $D_{1}$ and $D_{2}$ to this
trace are $\\{(a_{2},0,0),(a_{2},1,1),$ $(b_{2},3,3),(b_{2},4,4)\\}$. Because
these intervals do not overlap (they are atomic and have unique timestamps) we
can see from Table 1 that the only clock predicate that can match two
subsequent intervals (i.e., no labeled interval exists between the end of the
first and beginning of the second) is ${\bf before}{}$. The rules in $D_{3}$,
then, do that (match intervals using ${\bf before}{}$ rules) but these match
both subsequent and non-subsequent intervals. Applying the rule
$a_{3}\leftarrow a_{2}\>{\bf before}{}\ b_{2}$, for example, produces
$(a_{3},1,3),$ $(a_{3},0,3),$ $(a_{3},1,4),$ and $(a_{3},0,4)$. To match only
subsequent intervals requires the rules from step four (in $D_{4}$). Applying
$a_{4}\leftarrow a_{3}\>{\bf unless}{}\ {\bf contain}{}\ a_{3}$ only generates
$(a_{4},0,1),(a_{4},1,3)$ because they do not _contain_ another
$a_{3}$-labeled interval, while $(a_{3},0,3)$, $(a_{3},1,4)$, and
$(a_{3},0,4)$ do contain $(a_{3},0,1)$ and $(a_{3},1,2)$.

At this point, we must discuss what we call the _Ancillary Event Phenomenon_.
Because we must generate sequentially composable intervals to simulate cfg,
and because these intervals must label the time _between_ events, inevitably
one event per trace must be unrepresented by such intervals. Since we choose
to label the intervals by their starting event, the final event in the trace
with a unique timestamp does not label an interval. We call this the
_ancillary event_ in a trace. In $\tau_{\textit{x}}$, the ancillary event is
$(b,4)$.

After applying $D_{1}\cup D_{2}\cup D_{3}\cup D_{4}$, we have the intervals
$(a_{4},0,1),(a_{4},1,3),$ and $(b_{4},3,4)$. These intervals are now
_sequentially composable_ because they (uniquely) ${\bf meet}{}$ at timestamps
$1$ and $3$, meaning we can use the ${\bf meet}{}$ clock predicate to match
only the contiguous intervals and no others.

With the sequentially composable intervals produced by the rules in $D_{4}$,
we now can simulate the productions of the two cfg. Recall that $P$ and
$P^{\prime}$ are the disjoint sets of these productions.

$\displaystyle\begin{split}D_{5}=\ &\\{\ A\leftarrow a_{4}\>{\bf coincide}{}\
a_{4}:(A\rightarrow a)\in P\cup P^{\prime}\ \\}\ \cup\\\ &\\{\ A\leftarrow
B\>{\bf meet}{}\ C:(A\rightarrow BC)\in P\cup P^{\prime}\ \\}\end{split}$ (5)

Unlike the rules from $D_{1}\cup D_{2}\cup D_{3}\cup D_{4}$, the rules in
$D_{5}$ may contain cycles and must be iterated over until a fixed point is
reached.

Figure 2 shows the result of applying $D_{5}$ to the running example. Each
rule in $D_{5}$, shown on the right side of the figure, maps to a production
in $P_{\textit{x}}$ and the intervals they produce simulate a derivation for
$\tau_{\textit{x}}$ in $G_{\textit{x}}$. Applying $A\leftarrow a_{4}\>{\bf
before}{}\ a_{4}$ produces $(A,0,1)$ and $(A,1,3)$, while $B\leftarrow
b_{4}\>{\bf before}{}\ b_{4}$ produces $(B,3,4)$. Then, applying $M\leftarrow
A\>{\bf meet}{}\ B$ produces $(M,1,4)$ and applying $S_{\textit{x}}\leftarrow
A\>{\bf meet}{}\ M$ produces $(S_{\textit{x}},0,4)$. As $S_{\textit{x}}$ is
the initial non-terminal for $G_{\textit{x}}$, an $S_{\textit{x}}$-labeled
interval in the fixed point indicates that the trace $\tau_{\textit{x}}$
during that interval is in the language of $G_{\textit{x}}$.

Figure 2: Example of applying step 5 from the proof of Theorem 3.1

Next, we show that the data-free nfer simulation has the desired properties.
We begin by showing correctness for a single grammar, starting with soundness.

######  Lemma 1.

Given cfg $G=(V,\Sigma,P,S)$ and a word $\sigma\in\Sigma^{*}$, fix an
identifier $a\in\Sigma$ for the ancillary event. Then,
$\sigma\in\mathcal{L}(G)$ $\Leftrightarrow$ $(S,0,|\sigma|-1)\in
T[\\![\bigcup_{i=1}^{5}D_{i}]\\!]\>(\ \textit{TRACE}(\sigma\cdot a)\ )$.

###### Proof.

The proof is by induction over $j-i$, showing that for a non-terminal $A\in
V$, $A\ext@arrow
0359\Rightarrowfill@{}{*}\sigma_{[i,j]}\Leftrightarrow(A,i,j)\in
T[\\![\bigcup_{i=1}^{5}D_{i}]\\!]\>(\textit{TRACE}(\sigma\cdot a))$. ∎

We now show completeness for a single grammar.

######  Lemma 2.

Given cfg $G=(V,\Sigma,P,S)$ and a trace $\tau\in\mathbb{E}^{*}$ such that
$|\tau|\geq 2$, let $t$ be the second largest timestamp in
$\textit{UNIQ}(\tau)$ and let $\sigma=\textit{WORD}(\tau)$. Then, $(S,0,t)\in
T[\\![\bigcup_{i=1}^{5}D_{i}]\\!]\>(\tau)$ $\Leftrightarrow$
$\sigma_{[0,|\sigma|-2]}\in\mathcal{L}(G)$.

###### Proof.

The proof is by induction over $j-i$, showing that for a non-terminal $A\in
V$, where $\tau=(\eta_{0},t_{0})(\eta_{1},t_{1})\cdots(\eta_{n-1},t_{n-1})$,
$A\ext@arrow
0359\Rightarrowfill@{}{*}\textit{WORD}(\tau_{[i,j]})\Leftrightarrow(A,t_{i},t_{j})\in
T[\\![\bigcup_{i=1}^{5}D_{i}]\\!]\>(\tau)$. ∎

Finally, we check that a word is accepted by both grammars by labeling as
$\eta_{T}$ where the timestamps of any $S$-and-$S^{\prime}$-labeled intervals
are the same. If any word has a derivation in both $G$ and $G^{\prime}$, then
applying $\bigcup_{i=1}^{6}D_{i}$ to the corresponding trace will result in a
$\eta_{T}$-labeled interval in the fixed point.

$D_{6}=\\{\eta_{T}\leftarrow S\>{\bf coincide}{}\ S^{\prime}\\}$ (6)

For example, suppose a second grammar $G^{\prime}_{\textit{x}}$ was introduced
accepting the language $a^{+}b^{+}$, where its initial non-terminal was
$S^{\prime}_{\textit{x}}$. The word $aab$ is in the language of
$G^{\prime}_{\textit{x}}$ and so applying $\bigcup_{i=1}^{5}D_{i}$ for
$G^{\prime}_{\textit{x}}$ to the trace $\tau_{\textit{x}}$ would yield a fixed
point containing the interval $(S^{\prime}_{\textit{x}},0,4)$. Since
$(S_{\textit{x}},0,4)$ coincides with this interval, applying the rule in
$D_{6}$ will yield $(\eta_{T},0,4)$.

######  Lemma 3.

Given cfg $G$ and $G^{\prime}$ and a word $\sigma\in\Sigma^{*}$, fix an
identifier $a\in\Sigma$ for the ancillary event. Then,
$\sigma\in\mathcal{L}(G)\cap\mathcal{L}(G^{\prime})$ $\Leftrightarrow$
$(\eta_{T},0,|\sigma|-1)\in$
$T[\\![\bigcup_{i=1}^{6}D_{i}]\\!]\>(\textit{TRACE}(\sigma\cdot a))$.

###### Proof.

Lemma 1 implies that the cfg $G$ and $G^{\prime}$ are simulated by
$\bigcup_{i=1}^{5}D_{i}$ for a word $\sigma$ and applying $D_{6}$ finds words
in the language of both grammars. ∎

######  Lemma 4.

Given cfg $G$ and $G^{\prime}$ and a trace $\tau\in\mathbb{E}^{*}$ such that
$|\tau|\geq 2$, let $t$ be the second largest timestamp in
$\textit{UNIQ}(\tau)$ and let $\sigma=\textit{WORD}(\tau)$. Then,
$(\eta_{T},0,t)\in T[\\![\bigcup_{i=1}^{5}D_{i}]\\!]\>(\tau)$
$\Leftrightarrow$
$\sigma_{[0,|\sigma|-2]}\in\mathcal{L}(G)\cap\mathcal{L}(G^{\prime})$

###### Proof.

Lemma 2 implies that the cfg $G$ and $G^{\prime}$ are simulated by
$\bigcup_{i=1}^{5}D_{i}$ for a trace $\tau$ and applying $D_{6}$ finds words
in the language of both grammars. ∎

Now, we can prove Theorem 3.1.

###### Proof.

Applying Lemmas 3 and 4 we obtain that
$\mathcal{L}(G)\cap\mathcal{L}(G^{\prime})$ is non-empty if and only if there
is a $\tau\in\mathbb{E}^{+}$ such that $(\eta_{T},\underline{{\
}}\;,\underline{{\ }}\;)\in T[\\![\bigcup_{i=1}^{6}D_{i}]\\!]\>(\tau)$. This
shows that the undecidable non-emptiness problem for the intersection of two
cfg can be reduced to the data-free nfer satisfiability problem. ∎

Due to the undecidability of satisfiability of data-free nfer, we now turn our
attention to examining fragments with decidable satisfiability. We identify
two such fragments: Inclusive nfer, where only inclusive rules are permitted,
and Cycle-free nfer, where specifications can be evaluated without a fixed-
point computation.

###  3.2 Inclusive Data-Free nfer Satisfiability is in PTime

We begin our study with the case where an nfer specification may contain
cycles but only contains inclusive rules.

######  Theorem 3.2.

The data-free, inclusive nfer satisfiability problem is in PTime.

We show that there is a polynomial-time algorithm that determines if an input
trace $\tau$ exists such that an $\eta_{T}$-labeled interval is in
$T[\\![D]\\!]\>\tau$ for a given specification $D$. To do this, we show how
the satisfiability of a data-free Inclusive-nfer specification can be proven
through an analysis of the rules without guessing a witnessing trace. This is
due to the monotone nature of inclusive nfer rules: new events added to an
input trace only add intervals and cannot invalidate existing ones. We
leverage this fact to show how only two factors influence the satisfiability
of cycle-free, inclusive nfer specifications: producibility from events in
$\Sigma$ and the requirement of positive duration for some intervals.

To begin, observe that inclusive nfer rules are monotone in nature. The
interpretation functions $R$, $S$, and $T$ only add intervals; they never
remove them. Furthermore, if the rule is inclusive, $R$ only tests for the
existence of intervals; it only tests for non-existence in the case of
exclusive rules. This means that we may always introduce new events into an
input trace without needing to keep track of prior results. The consequence is
that ensuring that a $\eta_{T}$-labeled interval appears in a fixed-point of
$T[\\![D]\\!]\>\tau$ only requires showing that a rule $\delta_{T}$ exists in
$D$ with $\eta_{T}$ on its left-hand side and that $\delta_{T}$ may be matched
by intervals resulting from $\Sigma$-labeled events. This concept is very
similar to graph reachability and we define it here inductively.

######  Definition 1.

Let $\Sigma$ be a set of input identifiers and $D$ an inclusive nfer
specification. An identifier $\eta$ is _producible_ by $D$ iff $\eta\in\Sigma$
or if there exists a rule $(\eta\leftarrow\eta_{1}\>\oplus\ \eta_{2})\in D$
and both $\eta_{1}$ and $\eta_{2}$ are producible by $D$.

We now prove that satisfiability for an nfer specification using only rules
with the ${\bf before}{}$ operator is equivalent to producibility. We discuss
specifications with only ${\bf before}{}$-rules here because they allow us to
ignore the interaction between events, which have zero duration, and nfer
operators which require positive duration. We address this complication after
proving Proposition 2.

######  Proposition 2.

Given a set of input identifiers $\Sigma$ and a target identifier $\eta_{T}$,
an nfer specification $D_{b}$ containing only ${\bf before}{}$ rules is
satisfiable iff $\eta_{T}$ is producible by $D_{b}$.

###### Proof.

If $\eta_{T}\in\Sigma$, then $D_{b}$ is satisfied by the trace $(\eta_{T},0)$.
If $\eta_{T}\not\in\Sigma$, then for $D_{b}$ to be satisfiable there must a
rule $\delta_{T}$ in $D_{b}$ with $\eta_{T}$ on its left-hand side. Next,
observe from the definition of ${\bf before}{}$ in Table 1 that the only
requirement of $\delta_{T}$ to produce a $\eta_{T}$-labeled interval is that
there exist intervals $i_{1}$ and $i_{2}$ such that
$\textit{end}(i_{1})<\textit{start}(i_{2})$. Clearly, if
$\textit{id}(i_{1})\in\Sigma$ and $\textit{id}(i_{2})\in\Sigma$ we can create
an input trace that satisfies this. If either identifier on the right-hand
side of $\delta_{T}$ is not in $\Sigma$, then apply the same logic inductively
for that identifier.

The reverse follows by a similarly straightforward induction: if a
$\eta_{T}$-labeled interval is producible then $D_{b}$ is satisfiable. ∎

To permit inclusive operators beyond before, we must address the requirement
of _positive duration_. To see why we need to address positive duration, take,
for example, the ${\bf overlap}{}$ operator. Again from Table 1, we see that
${\bf overlap}{}$ requires that $\textit{start}(i_{1})<\textit{end}(i_{2})$
and $\textit{start}(i_{2})<\textit{end}(i_{1})$. If we assume a zero duration
for $i_{2}$, we still must have positive duration for $i_{1}$:
$\textit{start}(i_{1})<\textit{start}(i_{2})=\textit{end}(i_{2})<\textit{end}(i_{1})$,
and the same holds for $i_{2}$ if we assume zero duration for $i_{1}$. This
means that, for an ${\bf overlap}{}$-rule to match, at least one interval it
matches must have positive duration. As such, ${\bf overlap}{}$-rules cannot
match two initial intervals (events), as they have zero duration.

Thus, producibility is insufficient to show satisfiability for inclusive-nfer
specifications. We must augment our definition of what is producible to
account for what intervals may be produced with positive duration.

Table 3 defines two functions from rules to sets of subsets of identifiers,
$\text{match}_{+}:\Delta\rightarrow 2^{2^{\mathcal{I}}}$ and
$\text{add}_{+}:\Delta\rightarrow 2^{2^{\mathcal{I}}}$. The $\text{match}_{+}$
function returns the identifiers that must appear in intervals with positive
duration for a given rule to match (produce an interval). The $\text{add}_{+}$
function returns the identifiers that must appear in intervals with positive
duration for a given rule to produce an interval with a positive duration.
Both functions return values in Conjunctive-Normal Form (CNF), meaning that at
least one element of each set must have positive duration. For example,
$\text{match}_{+}(\eta\leftarrow\eta_{1}\>{\bf meet}{}\ \eta_{2})=\varnothing$
because ${\bf meet}{}$ can match two intervals with zero duration, but
$\text{add}_{+}(\eta\leftarrow\eta_{1}\>{\bf meet}{}\
\eta_{2})=\\{\eta_{1},\eta_{2}\\}$ because at least one of the two intervals
it matches must have positive duration for the result to have positive
duration.

Table 3: Positive duration requirements on $\delta=(\eta\leftarrow\eta_{1}\>\oplus\ \eta_{2})$ in CNF (for the sake of readability, we identify a set of sets by a list of sets) $\oplus$ X |  before |  meet |  during |  coincide |  start |  finish |  overlap |  slice
---|---|---|---|---|---|---|---|---
$\text{match}_{+}(\delta)$ | $\varnothing$ | $\varnothing$ | $\varnothing$ | $\varnothing$ | $\varnothing$ | $\varnothing$ | $\\{\eta_{1},\eta_{2}\\}$ | $\\{\eta_{1},\eta_{2}\\}$
$\text{add}_{+}(\delta)$ | $\varnothing$ | $\\{\eta_{1},\eta_{2}\\}$ | $\\{\eta_{2}\\}$ | $\\{\eta_{1}\\},\\{\eta_{2}\\}$ | $\\{\eta_{1},\eta_{2}\\}$ | $\\{\eta_{1},\eta_{2}\\}$ | $\\{\eta_{1},\eta_{2}\\}$ | $\\{\eta_{1},\eta_{2}\\}$

######  Definition 2.

Let $\Sigma$ be a set of input identifiers and $D$ an inclusive nfer
specification. An identifier $\eta$ is _positive-duration capable_ in $D$ iff
there exists a rule $(\eta\leftarrow\eta_{1}\>\oplus\ \eta_{2})=\delta\in D$
such that for all $A\in\text{add}_{+}(\delta)$, there exists an identifier in
$A$ that is positive-duration capable in $D$.

Note that ${\bf before}{}$-rules $\delta$ are always positive-duration
capable, as we have $\text{add}_{+}(\delta)=\emptyset$ for such $\delta$. We
now define duration-sensitive producibility for identifiers in an inclusive
nfer specification using $\text{match}_{+}$ and the definition of positive-
duration capable identifiers.

######  Definition 3.

Let $\Sigma$ be a set of input identifiers and $D$ an inclusive nfer
specification. An identifier $\eta$ is _duration-sensitive producible_ by $D$
iff $\eta\in\Sigma$ or if there exists a rule
$(\eta\leftarrow\eta_{1}\>\oplus\ \eta_{2})=\delta\in D$ such that $\eta_{1}$
and $\eta_{2}$ are both duration-sensitive producible by $D$ and for all
$M\in\text{match}_{+}(\delta)$, there exists an identifier in $M$ that is
positive-duration capable in $D$.

It should be clear that the consequence of Definition 3 is the following
lemma.

######  Lemma 5.

Given a target identifier $\eta_{T}$, an inclusive nfer specification $D$ is
satisfiable iff $\eta_{T}$ is duration-sensitive producible by $D$.

Now, we can prove Theorem 3.2.

###### Proof.

By Lemma 5, satisfiability for data-free inclusive nfer is equivalent to
duration-sensitive producibility. As duration-sensitive producibility is
defined inductively, there is a straightforward polynomial-time satisfiability
algorithm implementing Definition 3 (presented and analyzed in Appendix 0.B).
∎

###  3.3 Cycle-Free Data-Free nfer Satisfiability is Decidable

Next, we consider data-free nfer with inclusive and exclusive rules, but
without cycles. Here, our decidability result is obtained by a transformation
to _monadic first order logic_ (MFO) (see, e.g., [10] for details) over
strings.

######  Theorem 3.3.

The data-free, cycle-free nfer satisfiability problem is decidable.

###### Proof.

Given a cycle-free specification $D$, we will, for each identifier $\eta$,
construct an MFO formula ${\varphi}_{D,{\eta}}(t_{0},t_{1})$ with free
variables $t_{0},t_{1}$, such that $\eta$ is satisfiable with respect to $D$
iff ${\varphi}_{D,{\eta}}(t_{0},t_{1})$ is satisfiable, i.e. there exists a
string (word) $w$ over $2^{\Sigma}$ and an assignment
$v:\\{t_{0},t_{1}\\}\rightarrow\\{0,\ldots,|w|-1\\}$ such that
$w,v\models{\varphi}_{D,{\eta}}(t_{0},t_{1})$. Note, that for an event
identifier $\eta\in\Sigma$, $\eta(\cdot)$ is a monadic predicate, where
$\eta(t)$ evaluates to true in a string $w$ over $2^{\Sigma}$ at position $t$
if and only if the set of $w$ at position $t$ contains $\eta$. That is
$w,v\models\eta(t)$ if and only if $\eta\in w_{v(t)}$.

Now from $w,v$, where $w,v\models{\varphi}_{D,{\eta}}(t_{0},t_{1})$, a
satisfying input trace for $\eta$ may be obtained as the concatenation
$\tau_{w,v}=(w_{t_{0}},t_{0})(w_{t_{0}+1},t_{0}+1)\ldots(w_{t_{1}},t_{1})$,
where for a set $\sigma=\\{\eta_{1},\ldots,\eta_{k}\\}\subseteq\Sigma$ and
$t\in\mathbb{N}$, we denote by $(\sigma,t)$ the (any) string
$(\eta_{1},t)(\eta_{2},t)\cdots(\eta_{k},t)$.

Since $D$ is cycle-free, we may order the identifiers by a topological sort of
the directed graph formed by the rules. The construction of
${\varphi}_{D,{\eta}}(t_{0},t_{1})$ now proceeds by induction on this order.
In the base case, $\eta$ is an event identifier. Here
${\varphi}_{D,{\eta}}(t_{0},t_{1})=(t_{0}=t_{1}\wedge\eta(t_{0}))$. For the
inductive case, ${\varphi}_{D,{\eta}}(t_{0},t_{1})$ is obtained by a
disjunction of all the rules for $\eta$ in $D$, i.e.:

${\varphi}_{D,{\eta}}(t_{0},t_{1})=\bigvee\nolimits_{\eta\leftarrow\eta_{1}\>\textbf{op}\
\eta_{2}\in D}\psi_{D,\eta_{1}\,\textbf{op}\,\,\eta_{2}}(t_{0},t_{1})$

where $\textbf{op}\in\\{\oplus,{\bf unless}{}\ \ominus\\}$. Here the
definition $\psi_{D,\eta_{1}\,\textbf{op}\,\,\eta_{2}}(t_{0},t_{1})$ is
obtained using the MFO formulas for $\eta_{1}$ and $\eta_{2}$ from the
induction hypothesis.

Here we just give the definition for two rules, one inclusive and one
exclusive rule, leaving the remaining rules for the reader to provide.

$\displaystyle\psi_{D,\eta_{1}\ {\bf before}\ \eta_{2}}(t_{0},t_{1})=\exists
t^{\prime}_{0},t^{\prime}_{1}\raisebox{-1.07639pt}{\scalebox{1.6}{.}}{\
}t_{0}\leq t^{\prime}_{1}<t^{\prime}_{0}\leq
t_{1}\wedge{\varphi}_{D,{\eta_{1}}}(t_{0},t^{\prime}_{1})\wedge{\varphi}_{D,{\eta_{2}}}(t^{\prime}_{0},t_{1})$
$\displaystyle\psi_{D,\eta_{1}\ {\bf unless}\ {\bf after}\
\eta_{2}}(t_{0},t_{1})={\varphi}_{D,{\eta_{1}}}(t_{0},t_{1})\,\,\wedge\forall
t^{\prime}_{0},t^{\prime}_{1}\raisebox{-1.07639pt}{\scalebox{1.6}{.}}{\
}(t^{\prime}_{0}\leq t^{\prime}_{1}<t_{0}\leq
t_{1})\Rightarrow\neg{\varphi}_{D,{\eta_{2}}}(t^{\prime}_{0},t^{\prime}_{1})$

Thus, decidability of MFO satisfiability over finite strings [5, 9, 24] yields
decidability of data-free, cycle-free nfer satisfiability. ∎

Though the reduction to MFO in Theorem 3.3 yields the desired decidability
result, it comes with a non-elementary complexity [23]. We leave it open
whether the problem has elementary complexity.

##  4 Evaluation of Data-free nfer

The evaluation problem for nfer asks, given a specification $D$, a trace
$\tau$ of events, and a target identifier $\eta_{T}$, is there an
$\eta_{T}$-labeled interval in $T[\\![D]\\!]\>\tau$? The problem has been
extensively studied in the presence of data, with complexities ranging from
undecidable (for arbitrary data and cycles in the rules) to PTime (for finite
data under the minimality constraint). We refer to [20] for an overview of the
results. One case that has not been considered thus far is the complexity of
the evaluation problem for data-free nfer.

Obviously, the result from [20] for finite-data covers the case of data-free
specifications, but without the “minimality” meta-constraint that artificially
limits the size of the result, evaluation with only inclusive rules is PSpace-
complete (without cycles) and respectively ExpTime-complete (with cycles).
Here, we show that these results depend on the availability of (finite) data:
data-free nfer can be evaluated in polynomial time (even without minimality).

######  Theorem 4.1.

The evaluation problem for data-free nfer is in PTime.

###### Proof.

Consider an input consisting of a specification $D$, a trace $\tau$ of events,
and a target identifier $\eta_{T}$, and let $k$ be the number of unique
timestamps in $\tau$.

Recall that an interval is completely specified by its identifier in
$\mathcal{I}$ and its starting and ending timestamp. Hence, as the application
of rules does not create new timestamps (cf. Table 1 and Table 2), the number
of intervals in $T[\\![D]\\!]\>\tau$ is bounded by $k^{2}|\mathcal{I}|$.
Furthermore, whether a rule is applicable to two intervals can be checked in
constant time. Thus, one can compute $T[\\![D]\\!]\>\tau$ in polynomial time
and then check whether it contains an $\eta_{T}$-labeled interval. ∎

##  5 Conclusion and Future Work

We have studied the complexity of the satisfiability and evaluation problems
for Data-free nfer. We proved that the evaluation problem is in PTime and the
satisfiability problem is undecidable in the general case, but decidable for
cycle-free specifications and in PTime for specifications with only inclusive
rules.

There are still open questions around the complexity of nfer that may be
interesting. We showed that satisfiability for Data-free nfer is decidable for
cycle-free specifications, but we do not prove a tight bound and we suspect it
may be possible to achieve improvements on the non-elementary upper-bound we
give. Another open question is if satisfiability is decidable for restricted
cases of nfer _with data_ , for example if specifications are cycle-free and
data is finite. We are also interested in the complexity of _monitoring_ nfer.
Here and in other works, nfer is presented with an offline semantics. A naïve
monitoring algorithm might simply recompute produced intervals each time a new
event arrives, but we suspect that better monitoring complexity can be
achieved without requiring assumptions beyond temporal ordering. We hope that
this work inspires others to examine the complexity of other modern rv
languages.

## References

  * [1] Aceto, L., Della Monica, D., Goranko, V., Ingólfsdóttir, A., Montanari, A., Sciavicco, G.: A complete classification of the expressiveness of interval logics of Allen’s relations: the general and the dense cases. Acta Informatica 53(3), 207–246 (Apr 2016). https://doi.org/10.1007/s00236-015-0231-4
  * [2] Allen, J.F.: Maintaining knowledge about temporal intervals. Communications of the ACM 26(11), 832–843 (1983)
  * [3] Bar-Hillel, Y., Perles, M., Shamir, E.: On formal properties of simple phrase structure grammars. STUF - Language Typology and Universals 14(1-4), 143–172 (1961). https://doi.org/doi:10.1524/stuf.1961.14.14.143, https://doi.org/10.1524/stuf.1961.14.14.143
  * [4] Bolander, T., Hansen, J.U., Hansen, M.R.: Decidability of a hybrid duration calculus. Electronic Notes in Theoretical Computer Science 174(6), 113–133 (2007). https://doi.org/10.1016/j.entcs.2006.11.029, proceedings of the International Workshop on Hybrid Logic (HyLo 2006)
  * [5] Büchi, J.R.: Weak second-order arithmetic and finite automata. Mathematical Logic Quarterly 6(1-6), 66–92 (1960). https://doi.org/https://doi.org/10.1002/malq.19600060105, https://onlinelibrary.wiley.com/doi/abs/10.1002/malq.19600060105
  * [6] Chaochen, Z., Hansen, M.R., Sestoft, P.: Decidability and undecidability results for duration calculus. In: Theoretical Aspects of Computer Science. pp. 58–68. STACS ’93, Springer-Verlag (1993). https://doi.org/10.5555/646509.694831
  * [7] Chaochen, Z., Hoare, C., Ravn, A.P.: A calculus of durations. Information Processing Letters 40(5), 269–276 (1991). https://doi.org/10.1016/0020-0190(91)90122-X
  * [8] Chomsky, N.: On certain formal properties of grammars. Information and Control 2(2), 137–167 (1959). https://doi.org/10.1016/S0019-9958(59)90362-6
  * [9] Elgot, C.C.: Decision problems of finite automata design and related arithmetics. Transactions of the American Mathematical Society 98(1), 21–51 (1961), http://www.jstor.org/stable/1993511
  * [10] Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games: A Guide to Current Research, LNCS, vol. 2500. Springer (2002). https://doi.org/10.1007/3-540-36387-4, https://doi.org/10.1007/3-540-36387-4
  * [11] Halpern, J., Manna, Z., Moszkowski, B.: A hardware semantics based on temporal intervals. In: Automata, Languages and Programming. pp. 278–291. Springer (1983). https://doi.org/10.1007/BFb0036915
  * [12] Halpern, J.Y., Shoham, Y.: A propositional modal logic of time intervals. J. ACM 38(4), 935–962 (1991). https://doi.org/10.1145/115234.115351
  * [13] Kauffman, S.: Log analysis and system monitoring with nfer. Science of Computer Programming 225 (01 2023). https://doi.org/10.1016/j.scico.2022.102909
  * [14] Kauffman, S., Dunne, M., Gracioli, G., Khan, W., Benann, N., Fischmeister, S.: Palisade: A framework for anomaly detection in embedded systems. Journal of Systems Architecture 113, 101876 (2021). https://doi.org/10.1016/j.sysarc.2020.101876
  * [15] Kauffman, S., Fischmeister, S.: Mining temporal intervals from real-time system traces. In: International Workshop on Software Mining (SoftwareMining’17). pp. 1–8. IEEE (2017). https://doi.org/10.1109/SOFTWAREMINING.2017.8100847
  * [16] Kauffman, S., Havelund, K., Joshi, R.: nfer–a notation and system for inferring event stream abstractions. In: International Conference on Runtime Verification (RV’16). LNCS, vol. 10012, pp. 235–250. Springer (2016). https://doi.org/10.1007/978-3-319-46982-9_15
  * [17] Kauffman, S., Havelund, K., Joshi, R., Fischmeister, S.: Inferring event stream abstractions. Formal Methods in System Design 53, 54–82 (2018). https://doi.org/10.1007/s10703-018-0317-z
  * [18] Kauffman, S., Joshi, R., Havelund, K.: Towards a logic for inferring properties of event streams. In: International Symposium on Leveraging Applications of Formal Methods (ISoLA’16). LNCS, vol. 9953, pp. 394–399. Springer (2016). https://doi.org/10.1007/978-3-319-47169-3_31
  * [19] Kauffman, S., Zimmermann, M.: The complexity of evaluating nfer. In: International Symposium on Theoretical Aspects of Software Engineering (TASE’22). LNCS, vol. 13299, pp. 388–405. Springer (07 2022). https://doi.org/10.1007/978-3-031-10363-6_26
  * [20] Kauffman, S., Zimmermann, M.: The complexity of evaluating nfer. Science of Computer Programming 231 (2024). https://doi.org/10.1016/j.scico.2023.103012
  * [21] Montanari, A., Puppis, G., Sala, P.: Maximal decidable fragments of halpern and shoham’s modal logic of intervals. In: Automata, Languages and Programming. pp. 345–356. Springer (2010). https://doi.org/10.1007/978-3-642-14162-1\\_29
  * [22] Montanari, A., Puppis, G., Sala, P., Sciavicco, G.: Decidability of the interval temporal logic ABB over the natural numbers. In: Theoretical Aspects of Computer Science. pp. 597–608. STACS ’10, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010), https://hal.archives-ouvertes.fr/hal-00717798
  * [23] Stockmeyer, L.J.: The Complexity of Decision Problems in Automata Theory and Logic. Ph.D. thesis, MIT (1974)
  * [24] Trakhtenbrot, B.A.: Finite automata and the logic of one-place predicates. Siberskii Matematicheskii Zhurnal 3(1), 103–131 (1962)
  * [25] Valentin Goranko, A.M., Sciavicco, G.: A road map of interval temporal logics and duration calculi. Journal of Applied Non-Classical Logics 14(1-2), 9–54 (2004). https://doi.org/10.3166/jancl.14.9-54

## Appendix

##  Appendix 0.A A Graphical Explanation of Clock Predicates

In Figure 3, an interval is represented by a line with its label written
above. Here, time moves from left to right and the $B$-labeled interval is
drawn only once and shared by each example. For the example $A\leftarrow
B\>{\bf before}{}\ C$, the $B$-labeled and $C$-labeled intervals are matched
because the $B$-labeled interval ends before the $C$-labeled interval begins.

Figure 3: Nfer clock predicates ($\oplus$) for inclusive rules

In Figure 4, an interval is represented by a line with its label written above
and _the absence_ of an interval is represented by the line being _dashed_.
Like above, time moves from left to right and the $B$-labeled interval is
drawn only once and shared by each example. For the example $A\leftarrow
B\>{\bf unless}{}\ {\bf after}{}\ C$, the $B$-labeled and $C$-labeled
intervals would be matched (if the $C$-labeled interval existed), which would
result in the $A$-labeled interval _not_ being produced.

Figure 4: Nfer clock predicates ($\ominus$) for exclusive rules

##  Appendix 0.B An Algorithm for Duration-Sensitive Producibility

Algorithm 1 implements Definition 3 to determine the satisfiability of an
inclusive nfer specification. It works by computing sets of positive-duration
capable identifiers ($I_{+}$) and duration-sensitive producible identifiers
($I_{\Sigma}$). Recall that the topological sort of the strongly-connected
components of the graph formed by the rules of an nfer specification gives a
dependency ordering for the evaluation of those rules. This order is computed
on Line 2 and the strongly-connected components $\mathcal{D}$ are iterated
over. This set is then looped over $|\mathcal{D}|$ times on Lines 3 and 4. In
the worst case, we must loop $|\mathcal{D}|$ times to reach a fixed point. For
each rule, then, Line 5 tests that both the identifiers on the right-hand side
are duration-sensitive producible for that rule. If they are duration-
sensitive producible, it then tests on Lines 6 and 8 that the rule’s duration
requirements are met using $\text{match}_{+}$ and $\text{add}_{+}$. If, after
iterating over the rules, $\eta_{T}$ is labeled as duration-sensitive
producible, then the $D$ is satisfiable.

Algorithm 1 Algorithm checking Data-Free Inclusive-nfer satisfiability

0: Specification $D$, identifiers $\Sigma$, target identifier $\eta_{T}$

1: $I_{+}\leftarrow\varnothing,\;\;I_{\Sigma}\leftarrow\Sigma$

2: for $\mathcal{D}\in\textit{topsort}(\text{SCC}(D))$ do

3: for $1\cdots|\mathcal{D}|$ do

4: for $\eta\leftarrow\eta_{1}\>\oplus\ \eta_{2}\in\mathcal{D}$ do

5: if $\\{\eta_{1},\eta_{2}\\}\cap I_{\Sigma}=\\{\eta_{1},\eta_{2}\\}$ then

6: if $\forall M\in\text{match}_{+}(\eta\leftarrow\eta_{1}\>\oplus\
\eta_{2})\raisebox{-1.07639pt}{\scalebox{1.6}{.}}{\ }M\cap
I_{+}\neq\varnothing$ then

7: $I_{\Sigma}\leftarrow I_{\Sigma}\cup\\{\eta\\}$

8: if $\forall A\in\text{add}_{+}(\eta\leftarrow\eta_{1}\>\oplus\
\eta_{2})\raisebox{-1.07639pt}{\scalebox{1.6}{.}}{\ }A\cap
I_{+}\neq\varnothing$ then

9: $I_{+}\leftarrow I_{+}\cup\\{\eta\\}$

10: end for looping over rules in $\mathcal{D}$

11: end for repeating $|\mathcal{D}|$ times

12: end for looping over strongly-connected components of $D$

13: if $\eta_{T}\in I_{\Sigma}$ then return SAT

14: else return UNSAT

######  Example 1.

Suppose a target identifier $\eta_{T}$ and a set of input identifiers
$\Sigma=\\{a,b\\}$. We now consider the result of applying Algorithm 1 to a
satisfiable list of inclusive rules with no cycles.

  1. 1.

$A\leftarrow b\>{\bf before}{}\ X$. $X$ is not in $I_{\Sigma}$
($I_{+}=\varnothing$, $I_{\Sigma}=\\{a,b\\}$)

  2. 2.

$A\leftarrow a\>{\bf before}{}\ b$. $a$ and $b$ are both in $I_{\Sigma}$ and
${\bf before}{}$ matches and adds duration without any other requirements
($I_{+}=\\{A\\}$, $I_{\Sigma}=\\{a,b,A\\}$)

  3. 3.

$B\leftarrow a\>{\bf meet}{}\ b$. $a$ and $b$ are both in $I_{\Sigma}$ and
$\text{match}_{+}$ for ${\bf meet}{}$ does not require positive duration, but
$\text{add}_{+}$ does ($I_{+}=\\{A\\}$, $I_{\Sigma}=\\{a,b,A,B\\}$)

  4. 4.

$\eta_{T}\leftarrow a\>{\bf overlap}{}\ B$. $a$ and $B$ are both in
$I_{\Sigma}$, but $\text{match}_{+}$ and $\text{add}_{+}$ require one of $a,B$
to be positive-duration capable ($I_{+}=\\{A\\}$, $I_{\Sigma}=\\{a,b,A,B\\}$)

  5. 5.

$\eta_{T}\leftarrow A\>{\bf overlap}{}\ B$. $A$ and $B$ are both in
$I_{\Sigma}$, and $A$ is positive-duration capable, meeting the requirement
($I_{+}=\\{A,\eta_{T}\\}$, $I_{\Sigma}=\\{a,b,A,B,\eta_{T}\\}$)

######  Lemma 6.

Algorithm 1 runs in $O(n^{2})$ where $n$ is the number of rules.

###### Proof.

The topological sort of the strongly-connected components of the graph of $D$
can be computed in linear time. Then each rule is visited at most $|D|$ times,
if all rules are in the same strongly-connected component. All other
operations are sub-linear. ∎


# strongly primeness of skew Hurwitz polynomial rings

Ali Shahidikia  Department of Mathematics, Dezful branch, Islamic Azad
University, Dezful, Iran<EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract.

For a ring $R$ and an endomorphism $\alpha$ of $R$, we characterize the left
and right strongly primeness of skew Hurwitz polynomial ring $(hR,\alpha)$.

###### Key words and phrases:

strongly prime ring, skew Hurwitz polynomial ring, insulator.

###### 1991 Mathematics Subject Classification:

16D25, 16D80

##

The study of formal power series rings has garnered noteworthy attention and
has been found to be essential in a multitude of fields, particularly in
differential algebra. In [6], Keigher introduced a variant of the formal power
series ring and studied its categorical properties in detail. This ring was
later named Hurwitz series ring. There are many interesting applications of
the Hurwitz series ring in differential algebra as Keigher showed in [7, 8].

Throughout this article, $R$ denotes an associative ring with unity, and
$\mbox{$\alpha$}:R\rightarrow R$ is an endomorphism. We denote
$(H(R),\mbox{$\alpha$})$, or simply $(HR,\mbox{$\alpha$})$, the skew Hurwitz
series ring over a ring $R$ whose elements are the functions
$f:\mbox{$\mathbb{N}$}\rightarrow R$, where $\mathbb{N}$ is the set of all
natural numbers, the addition is defined as usual and the multiplication given
by

$(fg)(n)=\sum_{k=0}^{n}\binom{n}{k}f(k)\mbox{$\alpha$}^{k}(g(n-k))\text{ for
all }n\in\mbox{$\mathbb{N}$},$

where $\binom{n}{k}$ is the binomial coefficient.

Define the mappings $h_{n}:\mbox{$\mathbb{N}$}\rightarrow R$, $n\geq 1$ via
$h_{n}(n-1)=1$ and $h_{n}(m)=0$ for each
$m\in\mbox{$\mathbb{N}$}\setminus\\{n-1\\}$ and
$h^{\prime}_{r}:\mbox{$\mathbb{N}$}\rightarrow R$, $r\in R$ via
$h^{\prime}_{r}(0)=r$ and $h^{\prime}_{r}(n)=0$ for each
$n\in\mbox{$\mathbb{N}$}\setminus\\{0\\}$. It can be easily shown that $h_{1}$
is the unity of $(HR,\mbox{$\alpha$})$.

For $f\in(HR,\mbox{$\alpha$})$, the support of $f$, denoted by $supp(f)$, is
the set $\\{i\in\mbox{$\mathbb{N}$}\mid f(i)\not=0\\}$. The minimal element in
$supp(f)$ is denoted by $\Pi(f)$, and $\Delta(f)$ denotes the greatest element
in $supp(f)$ if it exists. Define $R^{\prime}=\\{h^{\prime}_{r}\mid r\in
R\\}$. $R^{\prime}$ is a subring of $(HR,\mbox{$\alpha$})$ which is
isomorphism to $R$. For any nonempty subset $A$ of $R$ define
$A^{\prime}=\\{h^{\prime}_{r}\mid r\in A\\}.$ If $A$ is an ideal of $R$, then
$A^{\prime}$ is an ideal of $R^{\prime}$.

The ring $(hR,\mbox{$\alpha$})$ of skew Hurwitz polynomials over a ring $R$ is
the subring of $(HR,\mbox{$\alpha$})$ that consists elements of the form
$f\in(HR,\mbox{$\alpha$})$ with $\Delta(f)<\infty$ (see [3]).

The notion of strongly prime rings was introduced by Handelman and Lawrence in
[5]. Since then strongly prime rings have been extensively studied. F.Cedo in
[4] presented an example of a ring $R$ such that $R$ is not strongly prime but
the power series ring $R[[x]]$ is strongly prime on both sides. It is well-
known that the Hurwitz polynomial ring $hR$ is right strongly prime if and
only if the coefficient ring $R$ is right strongly prime. The same argument
can be applied to show that an analogous statement holds for skew Hurwitz
polynomial rings of automorphism type. The aim of this note is to characterize
the left and right strongly primeness of skew Hurwitz polynomial rings of
endomorphism type. It is not a surprise that the obtained characterization is
not left-right symmetric. This, in turn, enable to construct easy examples of
rings which are strongly prime only on one side. The examples known earlier
were much more complicated (see [5, 9]). Recall from [5], that a subset
$F\subseteq R$ is a left (right) insulator if $F$ is finite and
$\ell_{R}(F)=0$ ($r_{R}(F)=0$).
We need the following lemma in the sequel.

######  Lemma 1.

[5] For the ring $R$ the following conditions are equivalent:

  1. (1)

$R$ is left (right) strongly prime.

  2. (2)

Every nonzero ideal of $R$ contains left (right) insulator.

  3. (3)

Every nonzero left (right) ideal of $R$ contains left (right) insulator.

  4. (4)

Every nonzero principal left (right) ideal of $R$ contains left (right)
insulator.

Notice that if $(hR,\alpha)$ is left (right) strongly prime, then $\alpha$ has
to be a monomorphism, as otherwise $(hR,\alpha)$ would not be prime. A left
ideal $I$ of $R$ is called a left $\alpha$-ideal if $\alpha(I)\subseteq I$. We
say that $R$ is left $\alpha$-strongly prime if any nonzero left
$\alpha$-ideal $I$ of $R$ contains a finite subset $F$ such that
$\ell_{R}(\alpha^{k}(F))=0$ for any $k\geq 0$.

######  Remark 2.

  1. (1)

When $\alpha=id_{R}$, then $R$ is left $\alpha$-strongly prime if and only if
it is left strongly prime.

  2. (2)

When $\alpha$ is an automorphism, then $k$ in the above definition can be
replace by $0$.

  3. (3)

If $R$ is left $\alpha$-strongly prime, then $\alpha$ has to be a
monomorphism, since $ker(\alpha)$ is an $\alpha$-ideal of $R$.

######  Theorem 3.

The following conditions are equivalent:

  1. (1)

$(hR,\alpha)$ is a left strongly prime ring.

  2. (2)

$R$ is a left $\alpha$-strongly prime ring.

###### Proof.

(1)$\Rightarrow$(2) Let $I$ be a nonzero left $\alpha$-ideal of $R$ and
$(hI,\alpha)$ denote the set of all Hurwitz polynomials from $(hR,\alpha)$
with all coefficients from $I$. Then $(hI,\alpha)$ is a nonzero left ideal of
$(hR,\alpha)$. Thus, by assumption, it contains a left insulator
$\widehat{F}$. Then $h_{n+1}\widehat{F}$ is also a left insulator for any
$k\geq 0$. Let $F$ denote the set of all coefficients of polynomials from
$\widehat{F}$. Then, for any $k\geq 0$, $\alpha^{k}(F)$ is the set of all
coefficients of polynomials from $h_{n+1}\widehat{F}$. Therefore
$\ell_{R}(\alpha^{k}(F))=0$ for any $k\geq 0$. This shows that $R$ is left
$\alpha$-strongly prime.

(2)$\Rightarrow$(1) Let $J$ be a nonzero left ideal of $(hR,\alpha)$ and $I$
denote the set of leading coefficients of all polynomials from $J$. Then $I$
is an $\alpha$-invariant left ideal of $R$. Hence, by assumption, we can find
a finite set $F\subseteq I$ such that $\ell_{R}(\alpha^{k}(F))=0$ for any
$k\geq 0$. Let $\widehat{F}=\\{f_{a}\mid a\in F\\}$, where $f_{a}\in J$
denotes a polynomial having the leading coefficient $a$, for $a\in F$. Then it
is standard to check that $\widehat{F}$ is a left insulator contained in $J$,
thus $(hR,\alpha)$ is left strongly prime. ∎

The following theorem describes right strongly primeness of $(hR,\alpha)$.

######  Theorem 4.

For $(hR,\alpha)$ the following conditions are equivalent:

  1. (1)

$(hR,\alpha)$ is a right strongly prime ring.

  2. (2)

    1. (a)

$\alpha$ is a monomorphism;

    2. (b)

for any $0\not=a\in R$ and $m\geq 0$ there exist $k\geq 0$ and a finite set
$F\subseteq
a\alpha^{m}(R)+\alpha(a)\alpha^{m+1}(R)+\cdots+\alpha^{k}(a)\alpha^{m+k}(R)$
such that $r_{R}(F)\cap\alpha^{n}(R)=0$ for some $n\geq 0$.

###### Proof.

(1)$\Rightarrow$(2) Clearly $\alpha$ is a monomorphism. Let $0\not=a\in R$ and
$m\geq 0$. Then $J=a\alpha^{m}(R)h_{m+1}(hR,\alpha)$ is a nonzero right ideal
of $(hR,\alpha)$. Thus, by assumption, $J$ contains a right insulator
$\widehat{F}=\\{a_{i,m+k}h_{m+k+1}+\cdots,+a_{i,m}h_{m+1}\in J\mid 1\leq i\leq
s\\}$. Define
$F=\\{a_{i,m+k},\alpha(a_{i,m+k-1}),\ldots,\alpha^{k}(a_{i,m})\mid 1\leq i\leq
s\\}$ and set $n=m+k$. Then $F\subseteq
a\alpha^{m}(R)+\alpha(a)\alpha^{m+1}(R)+\cdots+\alpha^{k}(a)\alpha^{n}(R)$.
Let $r\in R$ be such that $F\alpha^{n}(r)=0$. Then, since $\alpha$ is a
monomorphism,
$a_{i,n}\alpha^{n}(r)=0,a_{i,n-1}\alpha^{n-1}(r)=0,\ldots,a_{i,m}\alpha^{m}(r)=0$
for any $1\leq i\leq s$. This means that $r\in r_{(hR,\alpha)}(\widehat{F})$,
so $r=0$ and $\alpha^{n}(r)=0$. Thus, $r_{R}(F)\cap\alpha^{n}(R)=0$ follows.

(2)$\Rightarrow$(1) Let $J$ be a nonzero ideal of $(hR,\alpha)$ and
$f=h_{m+1}a+\cdots+h_{1}a_{0}\in J$, where $a\not=0$. By assumption, there
exist $k\geq 0$ and a finite subset $F\subseteq
a\alpha^{m}(R)+\cdots+\alpha^{k}(a)\alpha^{m+k}(R)$ such that
$r_{R}(F)\cap\alpha^{n}(R)=0$ for some $n$. Without loss of generality, we may
assume that $F\subseteq
a\alpha^{m}(R)\cup\cdots\cup\alpha^{k}(a)\alpha^{m+k}(R)$ and $0\not\in F$.
Let $u=max\\{n,m+k\\}$. Since $J$ is a two-sided ideal, for any $b\in F$ we
can pick a polynomial $f_{b}\in J$ of degree $u$ having $b$ as the leading
coefficient. Let $\widehat{F}=\\{f_{b}\mid b\in F\\}$. Since $u\geq n$,
$r_{R}(F)\cap\alpha^{u}(R)=0$. This yields easily that
$r_{(hR,\alpha)}(\widehat{F})=0$ and shows that $\widehat{F}$ is a right
insulator of $(hR,\alpha)$. Thus, $(hR,\alpha)$ is right strongly prime. ∎

Notice that when $\alpha$ is an automorphism of $R$ then the property $(b)$
from the above theorem boils down to:
“every nonzero right $\alpha$-ideal of $R$ contains right insulator”. Thus
characterizations obtained in Theorems 3, 4 are symmetric in this case. The
above mentioned theorems enable to construct easy examples of rings which are
strongly prime only on one side.

######  Example 5.

Let $K$ be a field and $R=K\langle x_{0},x_{1},\ldots\mid x_{k}x_{\ell}=0$ for
all $k\geq\ell\rangle$. Let $\alpha$ denote the $K$-endomorphism of $R$ given
by $\alpha(x_{k})=x_{k+1}$ for all $k\geq 0$. Then:

  1. (1)

$(hR,\alpha)$ is not left strongly prime.

  2. (2)

$(hR,\alpha)$ is right strongly prime.

###### Proof.

(1) It is easy to see that for every finite subset $F$ of $R$,
$\ell_{R}(F)\not=0$. Thus, by Theorem 3, $(hR,\alpha)$ is not left strongly
prime.

(2) Let $0\not=a\in R$ and $n=1+max\\{\ell\mid x_{\ell}$ appears in some
monomial from $a\\}$. One can easily check that $r_{R}(a)\cap\alpha^{n}(R)=0$.
Then Theorem 4 yields that $(hR,\alpha)$ is right strongly prime. ∎

## References

  * [1] M. Ahmadi, Singular ideals of skew Hurwitz polynomial rings, Rend. Circ. Mat. Palermo 68, (2019), 589-593.
  * [2] M. Ahmadi, A. Moussavi, V. Nourozi, Nilradicals of skew Hurwitz series rings, Le Matematiche 70(1), (2015), 125–136.
  * [3] M. Ahmadi, A. Moussavi, V. Nourozi, On Skew Hurwitz Serieswise Armendariz Rings, Asian-Eur. J. Math. 7(3) (2014), 1450036.
  * [4] F. Cedo, Strongly prime power series rings, Comm. Algebra 25(7), (1997), 2237–2242.
  * [5] D. Handelman, J. Lawrence, Strongly prime rings, Trans. Amer. Math. Soc. 211, (1975), 209–223.
  * [6] W.F. Keigher. Adjunctions and comonads in differential algebra.Pacific. J. Math. 248, (1975), 99-112.
  * [7] W.F. Keigher. On the ring of Hurwitz series. Comm. Algebra. 25(6), (1997), 1845-1859.
  * [8] W.F. Keigher, F.L. Pritchard. Hurwitz series as formal functions. J. Pure and Applied Algebra. 146, (2000), 291-304.
  * [9] M. M. Parmenter, D. S. Passman, P. N. Steward, The strongly prime radical of crossed products, Comm. Algebra 12(9), (1984), 1099–1113.
  * [10] V. Nourozi, A. Moussavi, M. Ahmadi, On nilpotent elements of skew Hurwitz polynomial rings, Southeast Asian Bull. Math. 41(2), (2017), 239–248.
  * [11] V. Nourozi, F. Rahmati, M. Ahmadi, McCoy property of Hurwitz series rings, Asian-Eur. J. Math. 14(6), ( 2021), 2150105.
  * [12] V. Nourozi, S. Tafazolian, F. Rahmati, The a-number of jacobians of certain maximal curves, Trans. Comb. 10(2), (2021) ,121-128.
  * [13] V. Nourozi, S. Tafazolian, The a-number of maximal curves of third largest genus, AUT J. Math. Com. 3(1), (2022), 11–16.


# Muslim-Violence Bias Persists in Debiased GPT Models

Babak Hemmatian
Beckman Institute for Advanced Science and Technology
University of Illinois Urbana-Champaign
<EMAIL_ADDRESS>
Razan Baltaji
Department of Electrical and Computer Engineering
<EMAIL_ADDRESS>
Lav R. Varshney
Department of Electrical and Computer Engineering
<EMAIL_ADDRESS>

###### Abstract

Abid et al. (2021) showed a tendency in GPT-3 to generate violent completions
when prompted about Muslims, compared with other religions. Two pre-registered
replication attempts found few violent completions and only the weakest anti-
Muslim bias in the Instruct version, fine-tuned to eliminate biased and toxic
outputs. However, more pre-registered experiments showed that using common
names associated with the religions in prompts increases several-fold the rate
of violent completions, revealing a highly significant second-order bias
against Muslims. Our content analysis revealed religion-specific violent
themes containing highly offensive ideas regardless of prompt format.
Replications with ChatGPT suggest that any effects of GPT-3’s de-biasing have
disappeared with continued model development, as this newer model showed both
a strong Muslim-violence bias and rates of violent completions closer to Abid
et al. (2021) . Our results show the need for continual de-biasing of models
in ways that address higher-order associations.

##  1 Introduction and Background

With increasing use of Large Language Models or LLMs (Min et al., 2021), any
stereotypes they reproduce have greater real-world effects (Varshney et al.,
2019; Abbasi et al., 2019). Among these models, OpenAI’s GPT series is hailed
as especially effective for ‘zero-shot learning’, producing reasonable text
completions without further fine-tuning (Brown et al., 2020). But this means
biases affect all downstream tasks. We focus on the Muslim-violence bias,
mentioned by OpenAI developers (Brown et al., 2020; Radford et al., 2019), but
studied systematically by Abid et al. (2021). They used “Two Xs walked into a”
as the prompt with X replaced by religious identities. Most GPT-3 completions
for Muslims were violent, as determined using keywords. Christians had the
next highest rate at 15%. The developers of GPT-3 Instruct responded to
concerns about toxic generations by retraining GPT-3 using human ratings,
actively minimizing undesirable outputs (Ouyang et al., 2022). We examine the
effects of this de-biasing on the Muslim-violence bias in GPT-3 Instruct
series and its successor, ChatGPT. We use disambiguated and extended versions
of Abid et al. (2021) prompts/measures. Because faith identifiers like
"Muslim" are generic terms, we refer to our replications as the "Generic"
conditions.

However, biased sources may not call Muslims violent, but share related
violent content more often (Nacos & Torres-Reyna, 2003). Text-generating
algorithms may similarly identify names as Islamic and produce more violent
content while not calling Muslims “as-a-group” violent, especially if de-
biasing was focused on associations between group labels and stereotypes
(Ouyang et al., 2022). Comparing the rate of violent completions in response
to prompts with first and last names popular in different religions (the
Common Names condition) against those containing only generic faith
identifiers like "Muslim" allows us to test this hypothesis.

Finally, to understand what drives the bias, we performed manual thematic
analysis of the violent completions across Generic and Common Name conditions.
The results clarify the representations these black-box models learn, guiding
the development of training constraints to counteract biases.

##  2 Results

Details and data can be found here. We followed Abid et al. (2021) in using
OpenAI’s default parameters except for _max_tokens_ , where we gave the models
maximum space to demonstrate bias. We expanded on the previous study’s
violence keywords. To prevent false positives, we annotated completions marked
as violent using this method for attributing criminal acts to the target
identities. Average Cohen’s $\kappa$ for inter-rater agreement was .72 across
the annotated dimensions. Among shared completions showing disagreement, we
marked completions as belonging to a violent category if at least one rater
rated them as such.

Our generic conditions with GPT-3 Instruct were replications of Abid et al.
(2021), N=1,200. For higher-order bias, we created full made-up names from
lists of common religion-specific first and last names (see OSF; N=960).
Pooled estimates are shown in Figure 1-left. Religion and common name use both
increased the rate of violence. Violent texts contained both religion-agnostic
(e.g., armed robbery) and religion-specific (e.g., bombing and terrorism; see
Figure 1-right) schemas, some with inflammatory or incoherent content (see OSF
for the full texts).

The shallowness of de-biasing is reflected not only in persistent bias and
undesirable second-order associations, but also in our ChatGPT replication.
Any effects of de-biasing are lost in this later model, which shows Muslim-
violence bias similar in strength to Abid et al. (2021). The bias is
especially strong in the generic condition. The only group showing a low rate
in this condition is Christians, with even that sign of reduced toxicity
disappearing with the use of Common Names.

Figure 1: On the left, the proportion of violent completions (vertical axis)
for Genericity (stacked) and Religion (cluster) in GPT-3 Instruct (left bar)
and ChatGPT (right bar). Error bars show Standard Errors. The right figure
shows the themes of violent completions using the same format.

##  3 Summary

To summarize, the Instruct series’ fine-tuning has had shallow success in
reducing violent generations, but its effects do not override anti-Muslim
biases and are largely limited to explicit mentions of religious identity.
Even those effects disappear in the more recent ChatGPT. These findings
highlight the need for continual de-biasing in LLMs using methods that also
address higher-order associations.

## References

  * Abbasi et al. (2019) Mohsen Abbasi, Sorelle A. Friedler, Carlos Scheidegger, and Suresh Venkatasubramanian.  Fairness in representation: quantifying stereotyping as a representational harm.  In _Proceedings of the 2019 SIAM International Conference on Data Mining (SDM)_ , 2019.  URL https://epubs.siam.org/doi/abs/10.1137/1.9781611975673.90.
  * Abid et al. (2021) Abubakar Abid, Maheen Farooqi, and James Zou.  Large language models associate muslims with violence.  _Nature Machine Intelligence_ , 3(6):461–463, 2021.
  * Brown et al. (2020) Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel Ziegler, Jeffrey Wu, Clemens Winter, Chris Hesse, Mark Chen, Eric Sigler, Mateusz Litwin, Scott Gray, Benjamin Chess, Jack Clark, Christopher Berner, Sam McCandlish, Alec Radford, Ilya Sutskever, and Dario Amodei.  Language models are few-shot learners.  In _Advances in Neural Information Processing Systems 33 (NeurIPS 2020)_ , 2020.  URL https://proceedings.neurips.cc/paper/2020/hash/1457c0d6bfcb4967418bfb8ac142f64a-Abstract.html.
  * Min et al. (2021) Bonan Min, Hayley Ross, Elior Sulem, Amir Pouran Ben Veyseh, Thien Huu Nguyen, Oscar Sainz, Eneko Agirre, Ilana Heinz, and Dan Roth.  Recent advances in natural language processing via large pre-trained language models: A survey.  2021\.  URL https://arxiv.org/abs/2111.01243.
  * Nacos & Torres-Reyna (2003) Brigitte L. Nacos and Oscar Torres-Reyna.  Framing muslim-americans before and after 9/11.  In Pippa Norris, Montague Kern, and Marion Just (eds.), _Framing Terrorism_ , pp. 141–166. Routledge, New York, NY, 2003.  doi: 10.4324/9780203484845.
  * Ouyang et al. (2022) Long Ouyang, Jeff Wu, Xu Jiang, Diogo Almeida, Carroll L. Wainwright, Pamela Mishkin, Chong Zhang, Sandhini Agarwal, Katarina Slama, Alex Ray, John Schulman, Jacob Hilton, Fraser Kelton, Luke Miller, Maddie Simens, Amanda Askell, Peter Welinder, Paul Christiano, Jan Leike, and Ryan Lowe.  Training language models to follow instructions with human feedback.  2022\.  URL https://arxiv.org/pdf/2203.02155.pdf.
  * Radford et al. (2019) Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, and Ilya Sutskever.  Language models are unsupervised multitask learners.  2019\.  URL https://life-extension.github.io/2020/05/27/GPT%E6%8A%80%E6%9C%AF%E5%88%9D%E6%8E%A2/language-models.pdf.
  * Varshney et al. (2019) Lav R. Varshney, Nitish Shirish Keskar, and Richard Socher.  Pretrained ai models: Performativity, mobility, and change.  2019\.  doi: 10.48550/arXiv.1909.03290.