The thesis deals with monitoring and robustness analysis of Signal Temporal Logic extended with a signal-value freezing operator. The logic has been defined in the paper "On Expressing and Monitoring Oscillatory Dynamics" (Dluhoš et al., HSB 2012) The thesis has two theoretical and one practical goals.

The first theoretical goal is to get deep understanding of STL* semantics and extend the logic to unlimited nesting of freezing operators.

The second theoretical goal (the main contribution) is to define the notion of robustness of a signal with respect to an STL* formula. To this end, the student will extend the notion of robustness as introduced in the paper "Robustness of Temporal Logic Specifications for Signals" (G.E.Fainekos et al.).

Practical goal of the thesis is to design and implement an algorithm for computing robustness of signals with respect to STL* formulae. The implementation will be realized as an extension of the tool ParaSim (http://github.com/sybila/parasim).