Monte-Carlo techniques for falsification of temporal properties of non-linear hybrid systems

Truong Nghiem, Sriram Sankaranarayanan, Georgios Fainekos, Franjo Ivančić, Aarti Gupta, George J. Pappas

Research output: Chapter in Book/Report/Conference proceedingConference contribution

105 Scopus citations

Abstract

We present a Monte-Carlo optimization technique for finding inputs to a system that falsify a given Metric Temporal Logic (MTL) property. Our approach performs a random walk over the space of inputs guided by a robustness metric defined by the MTL property. Robustness can be used to guide our search for a falsifying trajectory by exploring trajectories with smaller robustness values. We show that the notion of robustness can be generalized to consider hybrid system trajectories. The resulting testing framework can be applied to non-linear hybrid systems with external inputs. We show through numerous experiments on complex systems that using our framework can help automatically falsify properties with more consistency as compared to other means such as uniform sampling.

Original languageEnglish (US)
Title of host publicationHSCC'10 - Proceedings of the 13th ACM International Conference on Hybrid Systems
Subtitle of host publicationComputation and Control
Pages211-220
Number of pages10
DOIs
StatePublished - 2010
Event13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC'10 - Stockholm, Sweden
Duration: Apr 12 2010Apr 15 2010

Publication series

NameHSCC'10 - Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control

Conference

Conference13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC'10
Country/TerritorySweden
CityStockholm
Period4/12/104/15/10

Keywords

  • Hybrid systems
  • Metric temporal logic
  • Robustness
  • Testing

ASJC Scopus subject areas

  • Computational Theory and Mathematics
  • Control and Systems Engineering

Fingerprint

Dive into the research topics of 'Monte-Carlo techniques for falsification of temporal properties of non-linear hybrid systems'. Together they form a unique fingerprint.

Cite this