On Expressing and Monitoring Oscillatory Dynamics

Petr Dluhoš
(Masaryk University)
Luboš Brim
(Masaryk University)
David Šafránek
(Masaryk University)

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.

In Ezio Bartocci and Luca Bortolussi: Proceedings First International Workshop on Hybrid Systems and Biology (HSB 2012), Newcastle Upon Tyne, 3rd September 2012, Electronic Proceedings in Theoretical Computer Science 92, pp. 73–87.
Published: 15th August 2012.

ArXived at: http://dx.doi.org/10.4204/EPTCS.92.6 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org