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

69 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 - Jun 8 2010
Externally publishedYes
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

Other

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

All Science Journal Classification (ASJC) codes

  • Computational Theory and Mathematics
  • Control and Systems Engineering

Keywords

  • Hybrid systems
  • Metric temporal logic
  • Robustness
  • Testing

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

    Nghiem, T., Sankaranarayanan, S., Fainekos, G., Ivančić, F., Gupta, A., & Pappas, G. J. (2010). Monte-Carlo techniques for falsification of temporal properties of non-linear hybrid systems. In HSCC'10 - Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control (pp. 211-220). (HSCC'10 - Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control). https://doi.org/10.1145/1755952.1755983