On Expressing and Monitoring Oscillatory Dynamics
For researchers analyzing biological oscillations, this work provides a more expressive temporal logic to capture nuanced oscillatory dynamics that STL cannot distinguish.
The paper extends Signal Temporal Logic (STL) with a freezing operator to create STL*, enabling expression and monitoring of detailed oscillatory properties in biological systems. The monitoring algorithm is prototyped in Matlab and evaluated on a biological case study.
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.