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].
 
Search WWH ::




Custom Search