Threshold monitors of real-valued signals fire on one of two operational semantics: the crossing modality, with events at upward transits of a threshold, or the touch modality, with events at local extrema. The runtime-verification and signal-processing literatures treat these as competing encoder families, usually presenting one as primitive and the other as a degenerate case. We argue that this framing is wrong: touch and crossing are dual primitives with incomparable minimal resource requirements - crossing is causal and carries one bit of memory, whereas touch is memoryless but needs a three-sample window and one step of lookahead - so neither monitor can simulate the other without genuinely new structure, and bridging them costs exactly one added bit of structure in each direction: persistent state one way, window or lookahead the other. We develop three consequences. First, the two modalities sit on a ladder indexed by the number of distinct verdicts a monitor may emit: a verdict-free baseline, a degenerate binary rung, a ternary rung that hosts the touch/crossing duality, and a four-valued rung that organises both along orthogonal touch/crossing and weak/strong axes. The two-, three-, and four-valued rungs themselves are the known runtime-verification verdict progression (the two-/three-/four-valued LTL semantics); our contribution at this layer is not the ladder but the strict tuning hierarchy L1 < L2 < L3 of tuning powers that realise the rungs. Second, the touch-crossing join is a literal parameter coincidence at the four-valued rung: a single augmented monitor realises both modalities as exact parameter choices, and the three classical engineering encoders - edge detector, Schmitt trigger, and extremum detector - appear as named special cases of its ternary subfamily. Third, the duality is operational: a pointwise count inequality (upward crossings never outnumber touches, up to a trace-boundary tick) separates the two on every signal; a linear-time algorithm synthesises tuning parameters realising any feasible target finite event pattern, with an asymmetric feasibility criterion; and a safety / cosafety / liveness / coliveness classification places both modalities inside the existing temporal-property landscape without new logical machinery.

Touch and Crossing: Dual Primitive Modalities of Threshold Monitors / Bragetti, D.. - (2026 Jan 01), pp. 1-105.

Touch and Crossing: Dual Primitive Modalities of Threshold Monitors

Bragetti, Davide
2026

Abstract

Threshold monitors of real-valued signals fire on one of two operational semantics: the crossing modality, with events at upward transits of a threshold, or the touch modality, with events at local extrema. The runtime-verification and signal-processing literatures treat these as competing encoder families, usually presenting one as primitive and the other as a degenerate case. We argue that this framing is wrong: touch and crossing are dual primitives with incomparable minimal resource requirements - crossing is causal and carries one bit of memory, whereas touch is memoryless but needs a three-sample window and one step of lookahead - so neither monitor can simulate the other without genuinely new structure, and bridging them costs exactly one added bit of structure in each direction: persistent state one way, window or lookahead the other. We develop three consequences. First, the two modalities sit on a ladder indexed by the number of distinct verdicts a monitor may emit: a verdict-free baseline, a degenerate binary rung, a ternary rung that hosts the touch/crossing duality, and a four-valued rung that organises both along orthogonal touch/crossing and weak/strong axes. The two-, three-, and four-valued rungs themselves are the known runtime-verification verdict progression (the two-/three-/four-valued LTL semantics); our contribution at this layer is not the ladder but the strict tuning hierarchy L1 < L2 < L3 of tuning powers that realise the rungs. Second, the touch-crossing join is a literal parameter coincidence at the four-valued rung: a single augmented monitor realises both modalities as exact parameter choices, and the three classical engineering encoders - edge detector, Schmitt trigger, and extremum detector - appear as named special cases of its ternary subfamily. Third, the duality is operational: a pointwise count inequality (upward crossings never outnumber touches, up to a trace-boundary tick) separates the two on every signal; a linear-time algorithm synthesises tuning parameters realising any feasible target finite event pattern, with an asymmetric feasibility criterion; and a safety / cosafety / liveness / coliveness classification places both modalities inside the existing temporal-property landscape without new logical machinery.
2026-01-01
File allegati a questo prodotto
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11573/1770547
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact