On Expressing and Monitoring Oscillatory Dynamics

TL;DR

This paper introduces STL*, an extension of Signal Temporal Logic with a signal-value freezing operator, enabling detailed expression and monitoring of biological oscillations, supported by a Matlab prototype and case study evaluation.

Contribution

It proposes STL*, a novel logic extension for better oscillation analysis, and provides a monitoring algorithm with practical implementation.

Findings

STL* can distinguish detailed biological oscillatory properties.

The monitoring algorithm is effective on real biological data.

Prototype implementation demonstrates practical applicability.

Abstract

To express temporal properties of dense-time real-valued signals, the Signal Temporal Logic (STL) has been defined by Maler et al. The work presented a monitoring algorithm deciding the satisfiability of STL formulae on finite discrete samples of continuous signals. The logic has been used to express and analyse biological systems, but it is not expressive enough to sufficiently distinguish oscillatory properties important in biology. In this paper we define the extended logic STL* in which STL is augmented with a signal-value freezing operator allowing us to express (and distinguish) detailed properties of biological oscillations. The logic is supported by a monitoring algorithm prototyped in Matlab. The monitoring procedure of STL* is evaluated on a biologically-relevant case study.