Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Quantitative Monitoring of Signal First-Order Logic

Marek Chalupa, Thomas A. Henzinger, N. Ege Saraç, Emily Yu

TL;DR

This work identifies a past-time fragment of SFO and gives a pastification procedure that transforms bounded-response SFO formulas into equisatisfiable formulas in this fragment, and develops an efficient runtime monitoring algorithm for this past-time fragment.

Abstract

Runtime monitoring checks, during execution, whether a partial signal produced by a hybrid system satisfies its specification. Signal First-Order Logic (SFO) offers expressive real-time specifications over such signals, but currently comes only with Boolean semantics and has no tool support. We provide the first robustness-based quantitative semantics for SFO, enabling the expression and evaluation of rich real-time properties beyond the scope of existing formalisms such as Signal Temporal Logic. To enable online monitoring, we identify a past-time fragment of SFO and give a pastification procedure that transforms bounded-response SFO formulas into equisatisfiable formulas in this fragment. We then develop an efficient runtime monitoring algorithm for this past-time fragment and evaluate its performance on a set of benchmarks, demonstrating the practicality and effectiveness of our approach. To the best of our knowledge, this is the first publicly available prototype for online quantitative monitoring of full SFO.

Quantitative Monitoring of Signal First-Order Logic

TL;DR

This work identifies a past-time fragment of SFO and gives a pastification procedure that transforms bounded-response SFO formulas into equisatisfiable formulas in this fragment, and develops an efficient runtime monitoring algorithm for this past-time fragment.

Abstract

Runtime monitoring checks, during execution, whether a partial signal produced by a hybrid system satisfies its specification. Signal First-Order Logic (SFO) offers expressive real-time specifications over such signals, but currently comes only with Boolean semantics and has no tool support. We provide the first robustness-based quantitative semantics for SFO, enabling the expression and evaluation of rich real-time properties beyond the scope of existing formalisms such as Signal Temporal Logic. To enable online monitoring, we identify a past-time fragment of SFO and give a pastification procedure that transforms bounded-response SFO formulas into equisatisfiable formulas in this fragment. We then develop an efficient runtime monitoring algorithm for this past-time fragment and evaluate its performance on a set of benchmarks, demonstrating the practicality and effectiveness of our approach. To the best of our knowledge, this is the first publicly available prototype for online quantitative monitoring of full SFO.
Paper Structure (14 sections, 8 theorems, 31 equations, 2 figures, 1 table, 5 algorithms)

This paper contains 14 sections, 8 theorems, 31 equations, 2 figures, 1 table, 5 algorithms.

Table of Contents

  1. Introduction
  2. Related work.
  3. Signal First-Order Logic (SFO)
  4. Quantitative Semantics of SFO
  5. Past-Time SFO (pSFO)
  6. Online Quantitative Monitoring of pSFO
  7. Experiments
  8. Benchmarks and Properties
  9. Results and Discussion
  10. Conclusion
  11. Omitted Proofs
  12. Proof of \ref{['cl:soundness']} (Soundness of Quantitative Semantics)
  13. Proof of \ref{['cl:past-equiv']} (Equisatisfiability Under Pastification)
  14. Proof of \ref{['cl:correctness-monitor']} (Correctness of Monitor (\ref{['alg:monitoring']}))

Key Result

theorem 1

Let $\phi$ be an SFO formula, $w$ a signal trace, and $\nu$ a valuation. If $\mu(w, \nu, \phi) > 0$, then $w, \nu \models \phi$. If $\mu(w, \nu, \phi) < 0$, then $w, \nu \not\models \phi$.

Figures (2)

  • Figure 1: Illustration of the quantitative semantics for the bounded stabilization property given in \ref{['ex:bstab']}. For convenience, we use piecewise-linear interpolation. Upward arrows indicate rising edges at $t_1 = 1$ and $t_2 = 12$. Following $t_1$, the signal $f$ stabilizes rapidly within the $\pm 0.5$ tolerance band around $r_1 = 1$. Conversely, following $t_2$, the signal exhibits wide oscillations that violate the band. The quantitative evaluation considers all $8$-unit windows starting within $10$ units of $t_2$, identifying the window with the minimum range to determine the maximal robustness value.
  • Figure 1: Monitor

Theorems & Definitions (25)

  • definition 1: Syntax
  • definition 2: Boolean Semantics
  • remark 1: Well-definedness
  • definition 3: Quantitative Semantics
  • remark 2: Units and Compatibility
  • theorem 1: Soundness of Quantitative Semantics
  • definition 4: Access time terms and pSFO
  • definition 5: Horizons
  • definition 6: Pastification
  • theorem 2: Equisatisfiability under Pastification
  • ...and 15 more