Information Technology Reference
In-Depth Information
On Signal Temporal Logic
Alexandre Donze
EECS Dept., University of California, Berkeley
donze@eecs.berkeley.edu
Tutorial Description
Temporal Logic (TL) is a popular formalism, introduced into systems design
[Pnu77] as a language for specifying acceptable behaviors of reactive systems.
Traditionally, it has been used for formal verification, either by deductive meth-
ods [MP95], or algorithmic methods (Model Checking [CGP99,QS82]). In this
framework, the behaviors in question are typically discrete, that is, sequences of
states and/or events. In recent years, several trends suggest alternative ways to
use TL. One is due to the state-explosion wall, which limits the size of systems
that can be verified especially when dealing with programs involving numerical
computations or hybrid (discrete-continuous systems). As a result we can see a
proliferation of statistical methods -la Monte-Carlo, where universal quantifica-
tion is replaced by random simulation, with and sometimes without statistical
coverage guarantees. In this framework, related to
runtime verification
,
asser-
tion checking
or
monitoring
, the temporal formula is still used for a rigorous
specification of the requirements, but unlike model-checking, it is evaluated on a
single
behavior at a time. Another trend is concerned with
quantitative
evalua-
tion of TL formula. In many real-life applications, especially when dealing with
continuous dynamics and numerical quantities, yes/no answers provide only par-
tial information and could be augmented with
quantitative
information about
the satisfaction to provide a better basis for decision making. Such notions have
been introduced into TL by Fainekos and Pappas [FP09] and later In [DM10]
where notions of robustness both in space and time are described. This tutorial
is concerned with
signal temporal logic
(STL), a formalism for specifying prop-
erties of dense-time real-valued signals, originally introduced in [MN04]. It will
review both the fundamentals of STL and the most recent progress, and will
introduce the tool Breach [Don10] for illustration and practical applications. It
will be organized into three parts:
Part 1
will provide a general introduction to dense-time and real-valued tem-
poral logics
Part 2
will present the STL monitoring algorithm of [MN04], notions of robust
semantics [DM10] and robust monitoring algorithms [DFM13]
Part 3
will review various extensions, namely Parametric STL [ADMN11],
Time-Frequency Logic [DMB
+
12]) as well as different applications in
particular in the automative industry [JDDS13] and in systems biology
[DFG
+
11,MDMF12].