Robust Online Monitoring of Signal Temporal Logic
Jyotirmoy V. Deshmukh, Alexandre Donze, Shromona Ghosh, Xiaoqing Jin, Garvit Juniwal, Sanjit Seshia

Citation
Jyotirmoy V. Deshmukh, Alexandre Donze, Shromona Ghosh, Xiaoqing Jin, Garvit Juniwal, Sanjit Seshia. "Robust Online Monitoring of Signal Temporal Logic". Unpublished article, 2015.

Abstract
Signal Temporal Logic (STL) is a formalism used to rigor- ously specify requirements of cyberphysical systems (CPS), i.e., systems mixing digital or discrete components in interaction with a continuous environment or analog components. STL is naturally equipped with a quantitative seman- tics which can be used for various purposes: from assessing the robustness of a specification to guiding searches over the input and parameter space with the goal of falsifying the given property over system behaviors. Algorithms have been proposed and implemented for offline computation of such quantitative semantics, but only few methods exist for an online setting, where one would want to monitor the sat- isfaction of a formula during simulation. In this paper, we formalize a semantics for robust online monitoring of par- tial traces, i.e., traces for which there might not be enough data to decide the Boolean satisfaction (and to compute its quantitative counterpart). We propose an efficient algorithm to compute it and demonstrate its usage on two large scale real-world case studies, in particular from the automotive domain and in CPS education. We show that savings in computationally expensive simulations far outweigh any overheads incurred by an online approach.

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

  Jyotirmoy V. Deshmukh, Alexandre Donze, Shromona Ghosh,
  Xiaoqing Jin, Garvit Juniwal, Sanjit Seshia. <a
  href="http://www.terraswarm.org/pubs/495.html"
  ><i>Robust Online Monitoring of Signal Temporal
  Logic</i></a>, Unpublished article,  2015.

• Plain text

  Jyotirmoy V. Deshmukh, Alexandre Donze, Shromona Ghosh,
  Xiaoqing Jin, Garvit Juniwal, Sanjit Seshia. "Robust
  Online Monitoring of Signal Temporal Logic".
  Unpublished article,  2015.

• BibTeX

  @unpublished{DeshmukhDonzeGhoshJinJuniwalSeshia15_RobustOnlineMonitoringOfSignalTemporalLogic,
      author = {Jyotirmoy V. Deshmukh and Alexandre Donze and
                Shromona Ghosh and Xiaoqing Jin and Garvit Juniwal
                and Sanjit Seshia},
      title = {Robust Online Monitoring of Signal Temporal Logic},
      year = {2015},
      abstract = {Signal Temporal Logic (STL) is a formalism used to
                rigor- ously specify requirements of cyberphysical
                systems (CPS), i.e., systems mixing digital or
                discrete components in interaction with a
                continuous environment or analog components. STL
                is naturally equipped with a quantitative seman-
                tics which can be used for various purposes: from
                assessing the robustness of a specification to
                guiding searches over the input and parameter
                space with the goal of falsifying the given
                property over system behaviors. Algorithms have
                been proposed and implemented for offline
                computation of such quantitative semantics, but
                only few methods exist for an online setting,
                where one would want to monitor the sat- isfaction
                of a formula during simulation. In this paper, we
                formalize a semantics for robust online monitoring
                of par- tial traces, i.e., traces for which there
                might not be enough data to decide the Boolean
                satisfaction (and to compute its quantitative
                counterpart). We propose an efficient algorithm to
                compute it and demonstrate its usage on two large
                scale real-world case studies, in particular from
                the automotive domain and in CPS education. We
                show that savings in computationally expensive
                simulations far outweigh any overheads incurred by
                an online approach.},
      URL = {http://terraswarm.org/pubs/495.html}
  }
  

Posted by Alexandre Donze on 9 Feb 2015.
Groups: tools