Efficient Robust Monitoring for STL
Alexandre Donze, Thomas Ferrere, Oded Maler

Citation
Alexandre Donze, Thomas Ferrere, Oded Maler. "Efficient Robust Monitoring for STL". Proceedings of CAV 2013, April, 2013.

Abstract
Monitoring transient behaviors of real-time systems plays an important role in model-based systems design. Signal Temporal Logic (STL) emerges as a convenient and powerful formalism for continuous and hybrid systems. This paper presents an efficient algorithm for computing the robustness degree in which a piecewise-continuous signal satisfies or violates an STL formula. The algorithm, by leveraging state-of-the-art streaming algorithms from Signal Processing, is linear in the size of the signal and its implementation in the Breach tool is shown to outperform alternative implementations.

Electronic downloads

Internal. This publication has been marked by the author for TerraSwarm-only distribution, so electronic downloads are not available without logging in.

Citation formats

• HTML

  Alexandre Donze, Thomas Ferrere, Oded Maler. <a
  href="http://www.terraswarm.org/pubs/54.html"
  >Efficient Robust Monitoring for STL</a>,
  Proceedings of CAV 2013, April, 2013.

• Plain text

  Alexandre Donze, Thomas Ferrere, Oded Maler. "Efficient
  Robust Monitoring for STL". Proceedings of CAV 2013,
  April, 2013.

• BibTeX

  @inproceedings{DonzeFerrereMaler13_EfficientRobustMonitoringForSTL,
      author = {Alexandre Donze and Thomas Ferrere and Oded Maler},
      title = {Efficient Robust Monitoring for STL},
      booktitle = {Proceedings of CAV 2013},
      month = {April},
      year = {2013},
      abstract = {Monitoring transient behaviors of real-time
                systems plays an important role in model-based
                systems design. Signal Temporal Logic (STL)
                emerges as a convenient and powerful formalism for
                continuous and hybrid systems. This paper presents
                an efficient algorithm for computing the
                robustness degree in which a piecewise-continuous
                signal satisfies or violates an STL formula. The
                algorithm, by leveraging state-of-the-art
                streaming algorithms from Signal Processing, is
                linear in the size of the signal and its
                implementation in the Breach tool is shown to
                outperform alternative implementations. },
      URL = {http://terraswarm.org/pubs/54.html}
  }
  

Posted by Mila MacBain on 26 Apr 2013.