# PSL is Dead. Long Live PSL

Kevin Smith  Rice University
Houston, U.S.A.
<EMAIL_ADDRESS>Hai Lin  Palo Alto Networks
Santa Clara, U.S.A.
<EMAIL_ADDRESS>Praveen Tiwari  Marjorie Sayer  Palo Alto Networks
Santa Clara, U.S.A.
<EMAIL_ADDRESS>Palo Alto Networks
Santa Clara, U.S.A.
<EMAIL_ADDRESS>Claudionor Coelho  Palo Alto Networks
Santa Clara, U.S.A.
<EMAIL_ADDRESS>
###### Abstract

Property Specification Language (PSL) is a form of temporal logic that has
been mainly used in discrete domains (e.g. formal hardware verification). In
this paper, we show that by merging machine learning techniques with PSL
monitors, we can extend PSL to work on continuous domains. We apply this
technique in machine learning-based anomaly detection to analyze scenarios of
real-time streaming events from continuous variables in order to detect
abnormal behaviors of a system. By using machine learning with formal models,
we leverage the strengths of both machine learning methods and formal
semantics of time. On one hand, machine learning techniques can produce
distributions on continuous variables, where abnormalities can be captured as
deviations from the distributions. On the other hand, formal methods can
characterize discrete temporal behaviors and relations that cannot be easily
learned by machine learning techniques. Interestingly, the anomalies detected
by machine learning and the underlying time representation used are discrete
events. We implemented a temporal monitoring package (TEF) that operates in
conjunction with normal data science packages for anomaly detection machine
learning systems, and we show that TEF can be used to perform accurate
interpretation of temporal correlation between events.

###### Index Terms:

formal methods, PSL, anomaly detection

##  I Introduction

Property Specification Language (PSL) is a form of temporal logic that is
designed to capture temporal relations between discrete variables over
discrete time. Due to this nature, PSL has been mainly used in hardware design
and verification since it was standardized by IEEE in 2004 [1, 2, 8]. There
have been attempts to extend PSL to deal with continuous variables over
continuous time [6]. Due to its inherent limitation of expressibility, there
have not been many successful applications.

In recent years, anomaly detection has been widely used in practice [3, 13].
There are many applications where real-time streaming events are monitored and
analyzed in order to detect abnormal behaviors. For example, if the amount of
free memory of a computer is below a certain threshold, it can be considered
as an anomaly. As another example, if there is an anomalous drop in purchase
of a product in an online store, it is possible that the product is out of
stock, which needs attention. The state-of-the-art technique for anomaly
detection is machine learning [4, 7, 9, 11, 12, 14]. Machine learning
techniques learn distributions on continuous variables. Anomaly events can be
captured as deviations from established patterns (distributions). However,
there are certain temporal behaviors and relations that cannot be easily
learned by machine learning techniques, but can be easily characterized by
formal languages such as PSL.

In this paper, we propose a new framework called TEmporal Filtering (TEF) for
anomaly detection (Fig. 1). The idea is to merge machine learning with PSL
monitors. The machine learning module takes as input a number of continuous
variables $x_{1},x_{2},\ldots\ldots,x_{m}$, and outputs some discrete events
$y_{1},y_{2},\ldots\ldots,y_{n}$, which become the input of the PSL monitor.
The PSL monitor encodes a user-defined temporal relation, which filters the
output from the machine learning module. In this new framework, machine
learning techniques extend the capability of PSL by discretizing continuous
time and events; the PSL monitor refines the results produced by the machine
learning module. This combination of machine learning and formal methods
yields a whole that is greater than the sum of its parts.

The rest of this paper is organized as follows. In Section II, we give a brief
introduction to anomaly detection. Section III discusses the overall
architecture of TEF. In Section IV, we describe how TEF is implemented.
Section V illustrates how TEF can be used to capture temporal relations.
Section VI summarizes the conclusions of the paper and future work.

Figure 1: A New Framework for Anomaly Detection

##  II Anomaly Detection

Anomaly detection is the process of identifying events that deviate from
established patterns. Anomaly detection is widely used in many applications
such as detecting cyber intrusions, credit card fraud, and health monitoring.
In many applications, input variables have continuous values that vary with
time, such as temperature. A time series anomaly detection model learns
baseline behavior from training data and predicts a discrete set of anomalies.
In time series anomaly detection the discretizing mechanism is simply that
input timestamps are taken from discrete measurements, and there will always
be a minimum nonzero granularity of inputs. These models provide a rich set of
examples where a continuous valued problem maps to a discrete space, where
formal methods can be applied.

Anomaly detection modeling faces two major challenges. One, unbalanced data
sets: anomalies are rare, and thus data sets will have few examples of
anomalies which the model can learn. Two, characterization of anomalies:
different types of models detect different types of anomalies. Level based
methods find metric outliers. Distribution based methods find anomalies in
distributions. Features might not contain the signal needed to detect
anomalies. Being able to characterize anomalies helps, but unseen anomalies
cannot be characterized. In such cases, model selection is difficult. The next
sections describe some common types of anomaly detection models.

###  II-A Level-Based Anomaly Detection

In these types of models, anomalies in continuous data are defined as values
beyond a specific threshold. The threshold level is typically calibrated to
the expected fraction of anomalies to be detected. A level that is too low
results in false negatives, and one that is high results in false positives.
Often an immediate limitation of level based models is they do not account for
the frequency of threshold crossings. But threshold crossings and the
timestamps they occur do make up a discrete event space for study.

###  II-B Distribution-Based Anomaly Detection

Distribution based models learn the statistical distribution of data in a
baseline or normal state. Anomalies are categorized as events whose predicted
probabilities are lower than a learned threshold. These models can learn more
sophisticated behavior than level-based models - in particular, nonlinear
decision boundaries between anomalous and normal events can be learned. The
challenge of tuning the model remains: both the parameters that affect the
machine learning of the model, and the final tuning of the anomaly probability
thresholds. These challenges are documented in [10].

###  II-C Forecasting Error Methods

A wide range of time series forecasting methods, such as ARIMA, can be used to
predict probable events from past data. Predictions from a recent past period
can be compared with actual data values to determine if the actual values are
anomalous. The comparison of prediction and truth can in turn be level based
or distribution based.

###  II-D Template-based Anomaly Detection

If anomalies follow templates of behavior, established rules of feature
interaction and evolution through time, it’s reasonable to hope that a machine
learning model will learn the rules. The success of machine learning in many
applications has led to extensive efforts in applying machine learning models
to anomaly detection. Given enough features, enough data, enough compute
power, the reasoning goes, a machine learning model will learn all of the
intricate influences that distinguish anomalous behavior from normal. First,
we demonstrate that there are cases where enough data is theoretically
impossible. For instance, in a time stream of data, the event consisting of
repeated events a followed by an event b are not possible to learn from a
finite dataset. Second, while it may be possible to learn an underlying
template for anomalies, the amount of data and compute resources required for
sufficiently accurate results might be prohibitive.

###  II-E A Hybrid Method

Because anomaly detection models create discrete sets of events they naturally
can be described using PSL. Machine learning can make PSL relevant in
continuous applications. Because PSL can easily characterize infinite sets
such as the ”arbitrary stream of a followed by b” example as a simple PSL
expression: $a[+];b$, machine learning anomaly detection can be enhanced. We
aim to show in this paper that time series anomaly detection together with TEF
can improve overall model performance.

##  III TEF Overview

TEF implements a subset of PSL. PSL is an extension of linear temporal logic
and adds a number of operators to express temporal constraints. In particular,
PSL makes use of Sequential Extended Regular Expressions (SEREs), defined
below. If a PSL formula is composed entirely of SEREs, it is said to be
written in SERE-style PSL. TEF implements most of SERE-style PSL.

Propositional formulas (i.e., boolean variables closed under conjunction,
disjunction, and negation) are the atoms of SEREs. SEREs are SERE atoms closed
under the SERE operators, which are analogous to the operators of regular
expressions and also include supplemental operators representing useful
syntactic sugar. Just as regular expressions are used to match strings, SEREs
are used to match traces, that is, sequences of truth assignments. A SERE atom
matches a truth assignment when the truth assignment makes the atom true. The
semantics of compound SEREs are shown in Fig. 3 and Fig. 4.

One of the advantages in using a temporal logic to specify properties is that
logics are declarative. The result can be precisely described without the use
of control flow or statements that modify a program’s state. This allows those
without a background in software engineering to write useful properties.
However, the operators of linear temporal logic, although conceptually simple,
are not trivial to use in practice, and most people are unfamiliar with them.
An advantage of SERE-style PSL is that the functionality of LTL operators is
subsumed by the SERE operators and so familiarity with LTL is not a
requirement to writing properties. The close resemblance between SEREs and
standard regular expressions make the former exceptionally easy to learn if
one is familiar with the latter. And regular expressions are common currency
not just in software engineering, but in data analysis and related fields as
well. This makes SERE-style PSL easily accessible to those with a wide variety
of backgrounds.

So SERE-style PSL is a natural choice for TEF, which aims to provide a simple
and accessible way to express and evaluate temporal constraints. In fact, TEF
extends SERE-style PSL in an intuitive and useful way by allowing the use of
Boolean expressions wherever Boolean variables may occur in SEREs. Another
natural choice is the decision to package TEF as an extension to Pandas, which
is also common currency in the Python world.

TEF makes use of Python’s regex engine, which takes as input a regex pattern
(regular expression) and a string. The regex engine reports all segments of
the string that match the regex pattern. Python’s regex engine is highly
optimized and efficient. Fig. 3 lists the main temporal operators, which TEF
implements, and compares them with Python’s regex patterns. In this table, $r$
values are SEREs, $s$ values are sequences of rows in a DataFrame,
$r^{\prime}$ values are regex patterns, $s^{\prime}$ values are strings.
Readers are referred to [15] for the formal semantics of SERE-style
expressions.

At a high level, TEF takes advantage of the highly efficient regex engine and
the similarity between SERE expressions and regex patterns (shown in Fig. 3).
TEF reduces the problem of checking if a SERE expression matches rows of a
data frame to checking if a regex expression matches a string (Fig. 2). The
reduction is based on the following observation. Let $\mathcal{E}$ be the set
of all SERE expressions, $\mathcal{R}$ be the set of sequences of rows in a
data frame, $P$ be the set of all regex patterns, and $S$ be the set of
strings. There exist two functions $f:\mathcal{E}\rightarrow\mathcal{P}$ and
$g:\mathcal{R}\rightarrow\mathcal{S}$ s.t. $\forall
e\\!:\\!\mathcal{E},\;\;r\\!:\\!\mathcal{R}.\;\;matches(e,r)\leftrightarrow
matches(f(e),g(r))$. Intuitively, Fig. 3 justifies this observation.

Figure 2: How TEF is implemented

TEF also implements some additional operators as syntatic sugar (shown in Fig.
4). TEF also adds the “[]” operator for use in Boolean expressions, which
allows further flexibility in the expression of temporal relations. It
functions in the following way. Suppose we have a data frame with a column
$c$. Then $c[-1]$ refers to the value at the previous row in column $c$. Also,
$c[1]$ refers to the value at the next row in column $c$. In general, if $i$
is the index of the current row and $j$ is an integer, then $c[j]$ refers to
the value at row $i+j$ of column $c$. As syntactic sugar, $c$ may be used as
an abbreviation for $c[0]$. An illustrative example of a property making use
of the “[]” operator is $(c>c[-1])[*5]$, which matches all segments of the
trace in which the value at $c$ increases five times consecutively.

SERE Syntax | Meaning | Regex Syntax | Meaning
---|---|---|---
$r_{1};r_{2}$ | $\text{matches }s\text{ if }s=s_{1}s_{2},r_{1}\text{ matches }s_{1}\text{ and }r_{2}\text{ matches }s_{2}$ | $r_{1}^{\prime}r^{\prime}_{2}$ | $\text{matches }s^{\prime}\text{ if }s^{\prime}=s^{\prime}_{1}s^{\prime}_{2},r^{\prime}_{1}\text{ matches }s^{\prime}_{1}\text{ and }r^{\prime}_{2}\text{ matches }s^{\prime}_{2}$
$r_{1}|r_{2}$ | $\text{matches }s\text{ if }r_{1}\text{ matches }s\text{ or }r_{2}\text{ matches }s$ | $r^{\prime}_{1}|r^{\prime}_{2}$ | $\text{matches }s^{\prime}\text{ if }r^{\prime}_{1}\text{ matches }s^{\prime}\text{ or }r^{\prime}_{2}\text{ matches }s^{\prime}$
$r_{1}\&r_{2}$ | $\text{matches }s\text{ if }r_{1}\text{ matches }s\text{ and }r_{2}\text{ matches }s$ | $?=r^{\prime}$ | $\text{matches }s^{\prime}\text{ if }r^{\prime}\text{ matches }s^{\prime},butitdoesnotconsumeanyr^{\prime}$
$r[*]$ | $\text{matches }s\text{ if }0\text{ or more concatenations of }r\text{ matches }s$ | $r^{\prime}*$ | $\text{matches }s^{\prime}\text{ if }0\text{ or more concatenations of }r^{\prime}\text{ matches }s^{\prime}$
$r[+]$ | $\text{matches }s\text{ if }1\text{ or more concatenations of }r\text{ matches }s$ | $r^{\prime}+$ | $\text{matches }s^{\prime}\text{ if }1\text{ or more concatenations of }r^{\prime}\text{ matches }s^{\prime}$
$r[*n]$ | $\text{matches }s\text{ if }n\text{ concatenations of }r\text{ matches }s$ | $r^{\prime}\\{n\\}$ | $\text{matches }s^{\prime}\text{ if }n\text{ concatenations of }r^{\prime}\text{ matches }s^{\prime}$
$r[*n..m]$ | $\text{matches }s\text{ if between }n\text{ and }m\text{ concatenations of }r\text{ matches }s$ | $r^{\prime}\\{n,m\\}$ | $\text{matches }s^{\prime}\text{ if between }n\text{ and }m\text{ concatenations of }r^{\prime}\text{ matches }s^{\prime}$
$r[*n..]$ | $\text{matches }s\text{ if }n\text{ or more concatenations of }r\text{ matches }s$ | $r^{\prime}\\{n,\\}$ | $\text{matches }s^{\prime}\text{ if }n\text{ or more concatenations of }r^{\prime}\text{ matches }s^{\prime}$
$r[*..m]$ | $\text{matches }s\text{ if }m\text{ or fewer concatenations of }r\text{ matches }s$ | $r\\{0,m\\}$ | $\text{matches }s^{\prime}\text{ if }m\text{ or fewer concatenations of }r^{\prime}\text{ matches }s^{\prime}$

Figure 3: SERE expressions and Python’s regex patterns

$\begin{array}[]{ |c|c| }\hline\cr\text{Syntax}&\text{Intuitive Meaning}\\\
\hline\cr\hline\cr[+]&\text{True}[+]\\\ \hline\cr[*]&\text{True}[*]\\\
\hline\cr[*n]&\text{True}[*n..]\\\ \hline\cr[*n..m]&\text{True}[*n..m]\\\
\hline\cr[*n..]&\text{True}[*n..]\\\ \hline\cr[*..m]&\text{True}[*..m]\\\
\hline\cr r[->]&!r[*];r\\\ \hline\cr r[->n]&!r[*];r[*n]\\\ \hline\cr
r[->n..m]&!r[*];r[*n..m]\\\ \hline\cr r[=n]&(!r[*];r)[*n];!r[*]\\\ \hline\cr
r[=n..m]&(!r[*];r)[*n..m];!r[*]\\\ \hline\cr r[=n..]&(!r[*];r)[*n..];!r[*]\\\
\hline\cr r[=..m]&(!r[*];r)[*..m];!r[*]\\\ \hline\cr\end{array}$

Figure 4: Additional SERE-style operators Algorithm 1 An algorithm for
converting a SERE expression $e$ to a regex expression

1:function psl_to_regex($e$)

2: if $e$ is a Boolean expression $b$ then

3: return the disjunction of truth assignments that make $b$ true, in string
form.

4: else if $e$ is $r_{1};r_{2}$ then

5: $s_{1}\leftarrow$ psl_to_regex($r_{1}$)

6: $s_{2}\leftarrow$ psl_to_regex($r_{2}$)

7: return ‘(’ + $s_{1}+s_{2}$ \+ ‘)’

8: else if $e$ is $r_{1}|r_{2}$ then

9: $s_{1}\leftarrow$ psl_to_regex($r_{1}$)

10: $s_{2}\leftarrow$ psl_to_regex($r_{2}$)

11: return ‘(’ + $s_{1}+$ ‘$|$’ $+s_{2}$ \+ ‘)’

12: else if $e$ is $r_{1}\&r_{2}$ then

13: $s_{1}\leftarrow$ psl_to_regex($r_{1}$)

14: $s_{2}\leftarrow$ psl_to_regex($r_{2}$)

15: left = ’(’ + ’(?=’ + $s_{1}$ \+ ’)’ + $s_{2}$ \+ ’)’

16: right = ’(’ + ’(?=’ + $s_{2}$ \+ ’)’ + $s_{1}$ \+ ’)’

17: return ’(’ + left + ’$|$’ + right + ’)’

18: else if $e$ is $r[*]$ then

19: $s\leftarrow$ psl_to_regex($r$)

20: return ‘(’ + $s$ \+ ‘*’ + ‘)’

21: else if $e$ is $r[+]$ then

22: $s\leftarrow$ psl_to_regex($r$)

23: return ‘(’ + $s$ \+ ‘+’ + ‘)’

24: else if $e$ is $r[*n]$ then

25: $s\leftarrow$ psl_to_regex($r$)

26: return ’((’ + s + ’)’ + ’{’ + n + ’}’ + ’)’

27: else if $e$ is $r[*n..m]$ then

28: $s\leftarrow$ psl_to_regex($r$)

29: return ’((’ + s + ’)’ + ’{’ + n + ‘,’ + m + ’}’ + ’)’

30: else if $e$ is $r[*n..]$ then

31: $s\leftarrow$ psl_to_regex($r$)

32: return ’((’ + s + ’)’ + ’{’ + n + ‘,’ + ’}’ + ’)’

33: else if $e$ is $r[*..m]$ then

34: $s\leftarrow$ psl_to_regex($r$)

35: return ’((’ + s + ’)’ + ’{0’ + ‘,’ + m + ’}’ + ’)’

36: end if

37:end function

##  IV TEF Implementation

TEF shadows the Pandas DataFrame eval method. It takes as input a SERE-style
PSL property in the form of a string, and it matches it against the DataFrame,
which is interpreted as a trace. As we discussed in Section III, TEF reduces
the problem of checking if a SERE expression matches rows of a data frame to
checking if a Python regex pattern matches a string. In order to make the
reduction work, we just need to build two functions: (1) $f$ which converts a
SERE expression to a regex pattern. (2) $g$ which converts a data frame to a
string.

To build the function $f$, we use a simple recursion based on how the SERE
expression is constructed. The simplest SERE expression is a Boolean
expression. To convert a Boolean expression to a regex pattern, we rewrite the
expression in the form of the disjunction of its set of satisfying truth
assignments, in string form. As a result, the length of the pattern is
exponential in the number of distinct boolean expressions used in the
property. In practice we have found that many problems need make use of only a
few expressions. Often only a single expression is used to express a useful
property. To convert more complicated SERE expressions involving SERE
operators, the individual pieces are converted recursively, then the results
are combined based on the SERE operator. For example, suppose that we want to
convert $r_{1};r_{2}$. We first recursively convert $r_{1}$ and $r_{2}$, get
two regex strings, and then concatenate the two regex strings. The details of
converting a SERE expression into a Python regex pattern is shown in Algorithm
1.

To build the function $g$, TEF does two steps:

  * •

Step 1 (Booleanize a data frame) TEF identifies all the Boolean expressions
used in the property, and evaluates them with respect to each row in the data
frame. It keeps track of the results in a new data frame, in which the results
of each Boolean expression are kept in new columns. The details of
Booleanizing a data frame is shown in Algorithm 2.

  * •

Step 2 (convert to a string) The Booleanized DataFrame is converted to a
string by using ‘,’ to seperate columns and using ‘()’ to group characters
within the same rows.

After converting a SERE expression into a regex pattern and converting a data
frame into a string, Python’s regex engine is used to find matches. Results
are returned in the form of a list of index pairs indicating where in the
trace the property is satisfied.

Algorithm 2 An algorithm for Booleanizing a data frame $df$ w.r.t. a compound
Boolean expression $e$

1:function Booleanize_dataframe($df,e$)

2: Initialize $b\\_df$ to be an empty data frame.

3: for all row $r$ in $df$ do

4: Initialize $r^{\prime}$ to be an empty row.

5: for all atom $a$ in $e$ do

6: Evaluate $a$ w.r.t. $r$, add the result to $r^{\prime}$

7: end for

8: Add $r^{\prime}$ to $b\\_df$

9: end for

10: return $b\\_df$

11:end function

##  V Case Studies

###  V-A Analyzing Weather Patterns using TEF

Figure 6 shows a data frame containing the weather information in Amarillo,
TX, in April 2021. The weather data is taken from [16]. We make the following
queries to the data frame. Pandas DataFrame eval method can handle queries
involving only one row. If the query refers to multiple rows, we need to use
TEF eval method.

Figure 5: Data Frame: df

Figure 6: Booleanized Data Frame: b_df

1\. Find all individual days, when the temperature is either too hot
(temp_high $\geq$ 80) or too cold(temp_low $\leq$ 40). We can use Pandas
DataFrame eval method, which returns the set of individual rows, where the
constraint is satisfied (Fig. 7).

Figure 7: Query using Pandas DataFrame eval method

2\. Find two consecutive days where a hot day (temp_high $\geq$ 80) is
followed by a cold day (temp_low $\leq$ 40). The Pandas DataFrame eval method
cannot handle this query, since it cannot reason about temporal relations
involving multiple rows of a data frame. We use TEF eval method instead. TEF
does the following 3 steps to evaluate “temp_high $\geq$ 80; temp_low $\leq$
40” against the data frame $df$ (Fig. 6).

Figure 8: Query using TEF eval method

  * •

Step 1: As discussed in Section IV, TEF identifies all the Boolean expressions
used in the property, and evaluates them with respect to each row in df. This
particular query contains two Boolean expressions “high_temperature $\geq$ 80”
and “low_temperature $\leq$ 40”. The Booleanized data frame b_df (Fig. 6) has
two columns and has the same number of rows as df. b_df is transformed into
the following string by using ‘,’ to seperate columns and using ‘()’ to group
characters within the same rows.

(0,1)(0,0)(0,0)(0,0)(1,0)(1,0)(0,0)(0,0)(0,0)(0,1)(1,0)

(0,1)(0,1)(0,0)(0,0)(0,1)(0,1)(0,1)(0,1)(0,1)(0,1)(0,1)

(0,0)(0,0)(1,0)(1,0)(0,0)(0,0)(0,0)(0,0)

  * •

Step 2: The PSL property is compiled to a Python regex pattern:
$(\backslash\left(1,0\backslash\right)|\backslash\left(1,1\backslash\right))(\backslash\left(0,1\backslash\right)|\backslash\left(1,1\backslash\right))$.

  * •

Step 3: Python’s regex engine is used to find matches.

The result is shown in Fig. 8.

3\. Find two consecutive days when (1) temp_high $\leq$ 80 and temp_low $\geq$
40 (2) humidity $\geq$ 20 and humidity $\leq$ 70 (3) wind_speed $<$ 30\.
Again, this is a temporal relation involving multiple rows of the data frame.
We should use TEF eval method. The result is shown in Fig. 9.

Figure 9: Query using TEF eval method

###  V-B Analyzing Dow Jones Industrial Average (DJIA) index using TEF

In this section, we show how TEF can be used to analyze patterns in Dow Jones
Industrial Average (DJIA) index. This dataset contains data from 01/01/1980 to
12/31/2012, and is taken from [17]. All experiments are done on a Macbook,
with 2.6 GHz 6-Core Intel Core i7 and 16 GB 2667 MHz DDR4.

1\. [Rise_after_Drop] Find all periods where the index has been dropping for 5
consecutive days and rises on the next day. The result is shown in Fig. 10.

Figure 10: Rise_after_Drop

2\. [Fluctuation] Find all periods where the index decreases on one day and
increases on the next day, and this pattern repeats for at least 5 times. The
result is shown in Fig. 11.

Figure 11: Flunctuation

3\. [Steady] Find all periods where the index stays between 5000 and 6000 for
at least 10 days. The result is shown in Fig. 12.

Figure 12: Steady

4\. [Jump] Find all periods where the index increases by at least 10% compared
to the previous day. The result is shown in Fig. 13.

Figure 13: Jump

###  V-C Isolation Forest Anomaly Detection Models and TEF

Using examples from publicly available data sets, we show cases where false
positives from a trained isolation forest model can be filtered by rules. The
data is taken from [18]. The entire dataset collection consists of 250
datasets from domains such as medical monitoring, motion sensors, and weather.
We identified 130 examples where the model output could be improved by a rule
based filter.

Figure 14: Identify cluster of predictions

In Fig. 14 the anomaly is difficult to detect as it has similar amplitude and
frequency to the baseline pattern. But the detected anomalies are clustered in
time and anomalies that are farther apart could be ruled out by a simple rule
filter. We can use TEF to specify that within a cluster, the total number of
anomalies needs to reach a certain threshold. For example, $cluster_{2,5}$ =
“$anomaly[-2]+anomaly[-1]+anomaly+anomaly[1]+anomaly[2]\geq 2$” specifies that
at least 2 anomalies need to occur within a cluster of width 5. The width of
the cluster and the threshold can be adjusted for different applications. Fig.
15 is an example where the anomaly can be detected by a gap that follows
detected anomalies. In order to specify that a gap of width $x$ needs to
follow a detected anomaly, we can use: “$[*];anomaly;!anomaly[*x]$”. The
original data, shown in the upper graph, has an anomaly that is difficult to
characterize.

Figure 15: Identify by gap

As a final example, Fig. 16 shows a case where a suitable filtering rule would
take into account both cluster and gap behavior.
“$cluster_{2,5};!anomaly[*5];cluster_{2,5}$” specifies a sequence of events:
at least 2 anomalies occur within a cluster of width 5, followed by a gap of
width 5, followed by at least 2 anomalies occurring within a cluster of width
5. Again, the width of the cluster and the width of the gap can be adjusted
for different applications.

Figure 16: Identify by gap

##  VI Conclusions and Future Work

For many years, the use of PSL has been limited to hardware design and
verification, since PSL is designed to deal with discrete variables over
discrete time. In this paper, we propose that PSL can be used in continuous
domain for anomaly detection. The idea is to merge PSL with machine learning
and use a hybrid framework for anomaly detection. This hybrid framework
consists of a machine learning module and a PSL monitor. The machine learning
module outputs anomalies in the form of discrete time and events. The PSL
monitor further refines the output of the machine learning module by checking
if some user-defined temporal relation is satisfied. We implemented a temporal
monitoring package (TEF), and we show that TEF can be used to perform accurate
interpretation of temporal correlation between events.

For future work we are experimenting with the following cases: multivariate
anomaly detection problems, and TEF in conjunction with ensemble models. With
TEF, we have the opportunity to transform anomaly characterization rules into
data, and develop models from there.

## References

  * [1] Roderick Bloem, Stefan J. Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli, Martin Weiglhofer: “Specify, Compile, Run: Hardware from PSL.” Electron. Notes Theor. Comput. Sci. 190(4): 3-16 (2007)
  * [2] Marc Boule, Zeljko Zilic: “Efficient Automata-Based Assertion-Checker Synthesis of SEREs for Hardware Emulation.” ASP-DAC 2007: 324-329
  * [3] Varun Chandola, Arindam Banerjee, Vipin Kumar: “Anomaly detection: A survey.” ACM Comput. Surv. 41(3): 15:1-15:58. 2009.
  * [4] Lei Cui, Youyang Qu, Gang Xie, Deze Zeng, Ruidong Li, Shigen Shen, Shui Yu: “Security and Privacy-Enhanced Federated Learning for Anomaly Detection in IoT Infrastructures.” IEEE Trans. Ind. Informatics 18(5): 3492-3500 (2022)
  * [5] Cindy Eisner, Dana Fisman, “A Practical Introduction to PSL.” Series on Integrated Circuits and Systems, Springer 2006, ISBN 978-0-387-35313-5, pp. 1-240
  * [6] Ning Ge, Silvano Dal-Zilio, Hongyu Liu, Li Zhang, Lianyi Zhang, “RT-MOBS: A compositional observer semantics of time Petri net for real-time property specification language based on $\mu$-calculus.” Sci. Comput. Program. 206: 102624 (2021)
  * [7] Meenal Jain, Gagandeep Kaur, Vikas Saxena: “A K-Means clustering and SVM based hybrid concept drift detection technique for network anomaly detection.” Expert Syst. Appl. 193: 116510 (2022)
  * [8] Fatemeh Negin Javaheri, Katell Morin-Allory, Dominique Borrione: Synthesis of Regular Expressions Revisited: From PSL SEREs to Hardware. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 36(5): 869-882 (2017)
  * [9] Ömer Kasim: “An efficient and robust deep learning based network anomaly detection against distributed denial of service attacks.” Comput. Networks 180: 107390 (2020)
  * [10] Siwon Kim, Kukjin Choi, Hyun-Soo Choi, Byunghan Lee, Sungroh Yoon: “Towards a Rigorous Evaluation of Time-series Anomaly Detection” https://arxiv.org/pdf/2109.05257.pdf
  * [11] Jinbo Li, Hesam Izakian, Witold Pedrycz, Iqbal Jamal: “Clustering-based anomaly detection in multivariate time series data.” Appl. Soft Comput. 100: 106919 (2021)
  * [12] Hualin Ma, Liyan Zhang: “Attention-based framework for weakly supervised video anomaly detection.” J. Supercomput. 78(6): 8409-8429 (2022)
  * [13] Animesh Patcha, Jung-Min Park, “An overview of anomaly detection techniques: Existing solutions and latest technological trends.” Comput. Networks 51(12): 3448-3470. 2007.
  * [14] Jiaming Pei, Kaiyang Zhong, Mian Ahmad Jan, Jinhai Li, “Personalized federated learning framework for network traffic anomaly detection.” Comput. Networks 209: 108906 (2022)
  * [15] Ingo Pill, “Requirements Engineering and Efficient Verification of PSL Properties”, Doctoral Thesis, Institute for Software Technology, Graz University of Technology, 2008.
  * [16] https://www.wunderground.com/history/monthly/us/tx/amarillo/KAMA/date/2021-4
  * [17] https://vincentarelbundock.github.io/Rdatasets/datasets.html
  * [18] https://www.cs.ucr.edu/~eamonn/time_series_data_2018/UCR_TimeSeriesAnomalyDatasets2021.zip


Table 8: Sample of 8 bursts from 2FLGC. Temporal and spectral PL indices are taken from Ajello et al. (2019) with $\beta_{\rm L}=\Gamma_{\rm L}-1$. GRB | $\alpha_{\rm L}\pm\delta_{\alpha_{\rm L}}$ | $\beta_{\rm L}\pm\delta_{\beta_{\rm L}}$
---|---|---
090902B | $1.63\pm 0.08$ | $0.92\pm 0.06$
090926A | $1.82\pm 0.08$ | $0.86\pm 0.07$
100116A | $2.70\pm 0.20$ | $0.60\pm 0.20$
100414A | $1.30\pm 0.10$ | $0.80\pm 0.10$
130327B | $1.60\pm 0.20$ | $0.80\pm 0.10$
141207A | $1.88\pm 0.03$ | $0.80\pm 0.30$
160625B | $2.20\pm 0.30$ | $0.80\pm 0.30$
180526A | $1.30\pm 0.70$ | $0.80\pm 0.30$
Table 9: Sample of 4 bursts detected with VHE photons. Temporal and spectral
PL indices are taken from H. E. S. S. Collaboration et al. (2021); MAGIC
Collaboration et al. (2019b, a); Abdalla et al. (2019); LHAASO Collaboration
et al. (2023) with $\beta_{\rm VHE}=\Gamma_{\rm VHE}-1$.

GRB | $\alpha_{\rm L}\pm\delta_{\alpha_{\rm L}}$ | $\beta_{\rm L}\pm\delta_{\beta_{\rm L}}$ | $\alpha_{\rm VHE}\pm\delta_{\alpha_{\rm VHE}}$ | $\beta_{\rm VHE}\pm\delta_{\beta_{\rm VHE}}$
---|---|---|---|---
180720B | $1.90\pm 0.10$ | $1.15\pm 0.10$ | $-$ | $-$
190114C | $1.10\pm 0.15$ | $1.06\pm 0.30$ | $1.60\pm 0.07$ | $1.22\pm 0.23$
190829A | $-$ | $-$ | $1.09\pm 0.05$ |  $1.06\pm 0.10$ ∗
| $-$ | $-$ | $1.09\pm 0.05$ |  $0.86\pm 0.26$ ∗∗
221009A | $1.32\pm 0.05$ | $0.87\pm 0.04$ | $1.115\pm 0.012$ | $1.320\pm 0.015$

∗ These values correspond to the first night of observations.
∗∗ These values correspond to the second night of observations.

Figure 1: Corner plots of MCMC parameter estimation ($a$ and $b$) are shown
for synchrotron CRs for different circumbust environments. The first column
corresponds to a homogeneous medium with ${\rm k=0}$, the second assumes $\rm
k=0.5$ and so on, with the last column taking the value ${\rm k=2.5}$. The
rows, from top to bottom, are in accordance with the cooling condition
${\rm\nu_{m}^{sync}<\nu_{\rm LAT}<\nu_{c}^{sync}}$,
${\rm\nu_{c}^{sync}<\nu_{\rm LAT}<\nu_{m}^{sync}}$ and ${\rm
max\\{\nu_{m}^{sync},\nu_{c}^{sync}\\}<\nu_{\rm LAT}}$, respectively. The
histograms show the marginalized posterior densities with the median values in
red lines. Figure 2: The same as Figure 1, but for SSC process. Figure 3:
Synchrotron CRs for circumbust environments with ${\rm k=0}$, $0.5$, $1.0$,
$1.5$, $2.0$ and $2.5$. From top to bottom corresponds to the cooling
condition ${\rm\nu_{m}^{sync}<\nu_{\rm LAT}<\nu_{c}^{sync}}$,
${\rm\nu_{c}^{sync}<\nu_{\rm LAT}<\nu_{m}^{sync}}$ and ${\rm
max\\{\nu_{m}^{sync},\nu_{c}^{sync}\\}<\nu_{\rm LAT}}$, respectively. The
orange ellipses display the cases in which the CR are satisfied within 1 sigma
error bars for the best-fit values reported in Table 3. The red lines and dots
correspond to the relationships themselves. Figure 4: The same as Figure 3,
but for SSC process. Figure 5: The SSC light curves (right) and spectra (left)
in uniform-density afterglow model with variation of microphysical parameters.
The SEDs are displayed at 10 (first column) and 100 s (second column), and the
light curves for 1 (third column) and 10 (four column) GeV. The SSC spectra
are shown in the left-hand panels together with the CTA (Southern array, green
line), MAGIC (purple line) and Fermi-LAT (red line) sensitivities between 75
and 250 GeV at $3\times 10^{4}\,{\rm s}$ for a zenith angle of 20∘ (Fioretti
et al., 2019). The values of the parameters used are: $E=1\times 10^{52}\,{\rm
erg}$, $n=10^{-1}\,{\rm cm^{-3}}$, $\varepsilon_{\rm e}=0.1$,
$\varepsilon_{\rm e}=0.01$, $p(<2)=1.7$, $p(2<)=2.4$ and $z=0.1$ Figure 6: The
same as Figure 5, but for stellar-wind afterglow model with $A_{\rm W}=0.1$.
Figure 7: PL indices of microphysical variations for which the CRs are
fulfilled for a constant-density medium. The rows, from top to bottom, are in
accordance with the cooling condition ${\rm
max\\{\nu_{m}^{sync},\nu_{c}^{sync}\\}<\nu_{\rm LAT}}$ for synchrotron model
with $1<p<2$, ${\rm max\\{\nu_{m}^{ssc},\nu_{c}^{ssc}\\}<\nu_{\rm LAT}}$ and
${\rm\nu_{m}^{ssc}<\nu_{\rm LAT}<\nu_{c}^{ssc}}$ for SSC model with $1<p<2$
and with $p>2$, respectively.  Figure 8: The same as Figure 7, but for
stellar-wind afterglow model. Figure 9: Fermi-LAT and Swift-XRT observations
of GRB 160509A with the best-fit curves generated by synchrotron forward-
shock, and SSC reverse-shock afterglow model adapted from Fraija et al.
(2020). In addition, we include the SSC flux evolving in constant-density
medium using the best-fit values reported and the LAT data point at $4.2\times
10^{4}\,{\rm s}$ taken from Tam et al. (2017). Figure 10: PL indices of
microphysical variations for which the CRs are fulfilled for a constant-
density medium. The columns, from left to right, are in accordance with the
cooling condition ${\rm max\\{\nu_{m}^{ssc},\nu_{c}^{ssc}\\}<\nu_{\rm LAT}}$,
${\rm\nu_{c}^{ssc}<\nu_{\rm LAT}<\nu_{m}^{ssc}}$ and
${\rm\nu_{m}^{ssc}<\nu_{\rm LAT}<\nu_{c}^{ssc}}$, respectively. The small
starlike symbols ($*$) and (${**}$) in GRB 190829A correspond to the first and
second nights of observations.  Figure 11: The same as Figure 10, but for
stellar-wind afterglow model.