Learning Signal Temporal Logic through Neural Network for Interpretable Classification Danyang Li1 Mingyu Cai2 Cristian-Ioan Vasile2 Roberto Tron1

2025-04-29 0 0 771.74KB 8 页 10玖币

侵权投诉

Learning Signal Temporal Logic through Neural Network for

Interpretable Classiﬁcation

Danyang Li1, Mingyu Cai2, Cristian-Ioan Vasile2, Roberto Tron1

Abstract— Machine learning techniques using neural net-

works have achieved promising success for time-series data

classiﬁcation. However, the models that they produce are

challenging to verify and interpret. In this paper, we propose an

explainable neural-symbolic framework for the classiﬁcation of

time-series behaviors. In particular, we use an expressive formal

language, namely Signal Temporal Logic (STL), to constrain

the search of the computation graph for a neural network.

We design a novel time function and sparse softmax function

to improve the soundness and precision of the neural-STL

framework. As a result, we can efﬁciently learn a compact STL

formula for the classiﬁcation of time-series data through off-the-

shelf gradient-based tools. We demonstrate the computational

efﬁciency, compactness, and interpretability of the proposed

method through driving scenarios and naval surveillance case

studies, compared with state-of-the-art baselines.

I. INTRODUCTION

Binary classiﬁcation is a standard task in Supervised

Machine Learning (ML). Many techniques such as K-Nearest

Neighbors (KNN), Supported Vector Machine (SVM), and

Random Forest can be employed. A particular version of

the procedure introduces data derived from the evolution of

dynamic systems, which are in the form of time-series data;

this task can still be challenging for the current state-of-the-art

ML algorithm.

In recent years, deep learning (DL) methods have achieved

great success in complex pattern recognition, with a variety

of architectures such as convolutional [1], recurrent [2],

etc. However, the common drawback of DL and other ML

techniques is the lack of human-interpretability of the learned

models. This property is very important in control and robotics

since it can support qualitative and quantitative analysis.

In this paper, we propose to use the rich expressivity of

Signal Temporal Logic (STL) [3] for training classiﬁcation

of symbolic neural networks.

Signal Temporal Logic (STL) is a formal language designed

to express rich and human-interpretable speciﬁcations over

time series. Its quantitative satisfaction can be measured via

a recursive deﬁnition of robustness [3], which can be used in

control optimization problems [4] and sequential predication

task [5]. The task of learning STL formulas for classiﬁcation

also leverages the robustness to formulate an optimization

problem. Previous attempts [6]–[8] for learning temporal

logic properties assumed ﬁxed formula structures. Decision

Danyang Li and Roberto Tron are with Mechanical Engi-

neering Department, Boston University, Boston, MA 02215, USA.

danyangl@bu.edu, tron@bu.edu

M. Cai and C.I. Vasile are with the Department of Mechanical

Engineering and Mechanics, Lehigh University, Bethlehem, PA, USA

mingyu-cai@lehigh.edu, cvasile@lehigh.edu

tree based approaches [9]–[13] are proposed to learn both

operators and parameters via growing logic branches. The

branches growing of decision trees increases as the structure

of desired STL formula becomes more complicated. To the

best of our knowledge, the training time for the decision

tree based method is in order of minutes while the temporal

logic neural network can achieve order of seconds. To learn

temporal logic formulas from scratch, developing logic neural

networks [14], [15] attracts more attention. However, the

max/min operations in the computation of robustness are

not continuously differentiable. These operations cannot be

directly applied in a neural network since the network is not

able to learn with it.

Related works: Many works use STL for classiﬁcation.

Some works [16]–[20] use the recursive deﬁnition of the STL

and the structure of multi-layer neural networks, allowing

to directly apply off-the-shelf gradient-based deep learning

software. This kind of work can be divided into two categories

i.e., template-free and template-based learning. Intuitively,

template-based learning [16]–[19] ﬁxes the STL formula to be

learned from data and only learns some parameters. Whereas

template-free learning [20] learns the overall STL formula

including its structure from scratch. Our work uses this latter

category.

To address the non-smooth issues of the original STL

robustness [3], the differentiable versions of robustness

computation were proposed in [16], [18], which, however,

can not guarantee the soundness properties of STL and

the accuracy of satisfaction. The work [20] proposes an

alternative formulation that uses arithmetic-geometric mean

(AGM) STL robustness [21]. The AGM robustness is not

continuous and can not directly be backpropagated in a neural

network, resulting in problems of efﬁciency and adaptation

to gradient-based tools. In addition, both works [18], [20]

learn a weighted STL (wSTL) [22] that is harder for a user

to interpret if the complex weights are not manually omitted.

Contributions: First, we propose a template-free neural

network architecture with given fragments for the classiﬁca-

tion of time-series signals. The network can be interpreted

as level-one STL formulae. Our proposed models rely on

novel activation functions, especially on two new components:

a compact way to represent time intervals for temporal

operators, and a sound, differentiable approximation to

the maximum operator. As an additional contribution, we

introduce a synthetic dataset containing prototypical behaviors

inspired by autonomous driving situations. We use this dataset

to evaluate the performance of our methods, showing that we

are able to achieve high efﬁciency and automatically extract

arXiv:2210.01910v2 [cs.FL] 30 Jun 2023

qualitatively meaningful features of the data. More broadly,

we hope this dataset will serve as a benchmark for future

work in the classiﬁcation of time series.

II. PRELIMINARIES AND PROBLEM FORMULATION

We denote a

-dimensional, discrete-time, real-valued

signal as

s= (s(0), s(2), ..., s(l))

, where

l∈N+

is the

length of the signal,

s(τ)∈Rd

is the value of signal

time τ.

A. Signal Temporal Logic

We use signal temporal logic (STL) to specify the behaviors

of time-series signals.

Deﬁnition 1:

The syntax of STL formulae with linear

predicates is deﬁned recursively as [3]:

ϕ::= µ| ¬ϕ|ϕ1∧ϕ2|ϕ1∨ϕ2|♢[t1,t2]ϕ|□[t1,t2]ϕ, (1)

where

is a predicate deﬁned as

µ:= aTs(τ)≥b

a∈Rd

b∈R

ϕ, ϕ1, ϕ2

are STL formulas. The Boolean operators

¬,∧,∨

are negation,conjunction and disjunction, respectively.

The temporal operators

♢,□

represent eventually and always.

♢[t1,t2]ϕ

is true if

is satisﬁed for at least one point

τ∈

[t1, t2]

, while

□[t1,t2]ϕ

is true if

is satisﬁed for all time

points τ∈[t1, t2].

Deﬁnition 2:

The quantitative semantics, i.e., the robust-

ness, of the STL formula

over signal

at time

is deﬁned

as:

r(s, µ, τ) = aTs(τ)−b, (2a)

r(s, ¬ϕ, τ) = −r(s, ϕ, τ),(2b)

r(s, ∧N

i=1ϕi, τ) = min({r(s, ϕi, τ)}i=1:N),(2c)

r(s, ∨N

i=1ϕi, τ) = max({r(s, ϕi, τ)}i=1:N),(2d)

r(s, □[t1,t2]ϕ, τ) = min

τ′∈[τ+t1,τ +t2]r(s, ϕ, τ′),(2e)

r(s, ♢[t1,t2]ϕ, τ) = max

τ′∈[τ+t1,τ +t2]r(s, ϕ, τ′),(2f)

The signal

is said to satisfy the formula

, denoted as

s|=ϕ

, if

r(s, ϕ, 0) >0

. Otherwise,

is said to violate

denoted as s̸|=ϕ.

Deﬁnition 3:

The quantitative semantics in Deﬁnition 2

can be expressed in the form of indicator vectors:

r(s, µ, τ) = aTs−b, (3a)

r(s, ¬ϕ, τ) = −r(s, ϕ, τ),(3b)

r(s, ∧N

i=1ϕi, τ) = −f(−rc,c),(3c)

r(s, ∨N

i=1ϕi, τ) = f(rd,d),(3d)

r(s, □wtϕ, τ) = −f(−rt,wt),(3e)

r(s, ♢wtϕ, τ) = f(rt,wt),(3f)

where

rc=stack({r(s, ϕi, τ)}i=1;N)

rd=stack({r(s, ϕi,

τ)}i=1;N)

rt=stack({r(s, ϕ, τ′)}τ′∈[0,l])

and

are

binary indicator vectors.

wt=wt0, ..., wti, ..., wtl

is based

on the time parameters in 2e, 2f. In other words,

wti = 1

i∈[τ+t1, τ +t2]

, otherwise,

wti = 0

f(r,w) = max{rs}

where

is obtained from

using the indicator vector

such that ri∈rsif wi= 1 and ri/∈rsif wi= 0.

Deﬁnition 4 (Soundness):

Let

denote an algorithm for

computing the robustness of an STL formula

over signal

. We say

is sound if

M(ϕ, s)

can provide a valid result

for evaluating STL satisfaction, i.e.,

s|=ϕ=⇒ M(ϕ, s)>0(4a)

s̸|=ϕ=⇒ M(ϕ, s)≤0(4b)

B. Problem Statement

We consider a binary classiﬁcation task on a labeled data

set

S={(si, ci)}N

i=1

, where

si∈Rl×d

is the

ith

signal

labeled as ci∈C.C={1,−1}is the set of classes.

Problem 1:

Given

S={(si, ci)}N

i=1

, ﬁnd an STL formula

that minimizes the misclassiﬁcation rate

MCR

deﬁned as:

MCR =|{si|(si|=ϕ∧ci=−1) ∨(si̸|=ϕ∧ci= 1)}|

C. Overview of Proposed Work

We propose a Temporal Logic Inference (TLI) method

based on neural network embedding of STL formulas. Using

our method, we can infer both the structure and parameters of

STL properties. The proposed Neural Network architecture for

TLI (NN-TLI) enables the use of high-performance training

methods and extraction of interpretable classiﬁers in the form

of STL formulas from networks’ weights. The NN-TLI maps

a time-series data point (a signal)

to its robustness value

of the learned formula with the sign of robustness deﬁning

the predicted class of signal

. We restrict ourselves to an

expressive fragment of STL that allows the proposed efﬁcient

encoding and that is easy to interpret. In the following, we

present the NN-TLI structure in Sec. III and its training

method in Sec. IV.

III. NEURAL NETWORK ARCHITECTURE

The overall architecture of NN-TLI consists of four layers.

The ﬁrst layer is associated with the predicates of sub-

formulas. It takes signals as input and outputs robustness

values for all predicates at all times. The second layer takes

robustness values from the ﬁrst layer and time variables as

input and applies temporal operators to generate sub-formulas.

The last two layers implement logical operators to combine

sub-formulas. In the following sections, we ﬁrst introduce

the fragment of STL captured by NN-TLI formulas. Next,

we describe details of each layer of the NN-TLI architecture

and show how they implement the STL formula.

A. STL(1)

We deﬁne level-one STL, denoted by STL(1), as

ϕ:= µ| ¬ϕ|ϕ1∧ϕ2|ϕ1∨ϕ2,

ψ:= ♢[t1,t2]ϕ|□[t1,t2]ϕ, (5)

It is a proper fragment of STL without nested temporal

operators; it still retains rich expressivity as shown by the

following result.

Theorem 1:

The STL fragment STL

(1)

is equal to its

Boolean closure [10].

Proof: [Sketch] It follows immediately from the dis-

tributivity properties of always and eventually with respect

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

LearningSignalTemporalLogicthroughNeuralNetworkforInterpretableClassificationDanyangLi1,MingyuCai2,Cristian-IoanVasile2,RobertoTron1Abstract—Machinelearningtechniquesusingneuralnet-workshaveachievedpromisingsuccessfortime-seriesdataclassification.However,themodelsthattheyproducearechallengingtoverif...

展开>> 收起<<

Learning Signal Temporal Logic through Neural Network for Interpretable Classification Danyang Li1 Mingyu Cai2 Cristian-Ioan Vasile2 Roberto Tron1.pdf

共8页,预览2页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

Learning Signal Temporal Logic through Neural Network for Interpretable Classification Danyang Li1 Mingyu Cai2 Cristian-Ioan Vasile2 Roberto Tron1

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: