Robust Satisfaction of Temporal Logic over Real-Valued Signals

Abstract. We consider temporal logic formulae specifying constraints in continuous time and space on the behaviors of continuous and hybrid dynamical system admitting uncertain parameters. We present several variants of robustness measures that indicate how far a given trajectory stands, in space and time, from satisfying or violating a property. We present a method to compute these robustness measures as well as their sensitivity to the parameters of the system or parameters appearing in the formula. Combined with an appropriate strategy for exploring the parameter space, this technique can be used to guide simulation-based verification of complex nonlinear and hybrid systems against temporal properties. Our methodology can be used for other non-traditional applications of temporal logic such as characterizing subsets of the parameter space for which a system is guaranteed to satisfy a formula with a desired robustness degree.

• Type: Journal
• Year: 2010
• Where: FORMATS
• Authors: Alexandre Donzé, Oded Maler
• Keywords: Formal Methods, FORMATS 2010, Parameter, Space, Temporal Logic