pith. sign in

arxiv: 1907.07761 · v1 · pith:Y7PSGJEZnew · submitted 2019-07-10 · 💻 cs.LO · cs.FL· cs.PL

Runtime Verification For Timed Event Streams With Partial Information

Martin Leucker , C\'esar S\'anchez , Torben Scheffel , Malte Schmitz , Daniel Thoma This is my paper

Pith reviewed 2026-05-24 23:28 UTC · model grok-4.3

classification 💻 cs.LO cs.FLcs.PL
keywords runtime verificationstream runtime verificationTeSSLatimed event streamsincomplete tracesabstract streamsgapssoundness
0
0 comments X

The pith

Translating TeSSLa specifications into abstract versions lets them produce sound outputs from timed event streams that contain gaps.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops a method to run stream runtime verification on timed event streams even when parts of the trace are missing. It introduces abstract event streams that stand for every possible concrete sequence that could fit inside each gap. Specifications written in TeSSLa are then translated so they operate on these abstract streams and propagate uncertainty forward while guaranteeing that every reported output remains correct for any actual events that filled the gaps. The translation is realized as a set of macros on the existing TeSSLa implementation, and experiments confirm that the approach stays practical for realistic monitoring tasks.

Core claim

We define abstract event streams representing the set of all possible traces that could have occurred during gaps in the input trace. We show how to translate a TeSSLa specification to its abstract counterpart that can propagate gaps through the transformation of the input streams and thus generate sound outputs even if the input streams contain gaps and events with imprecise values.

What carries the argument

Abstract event streams that represent every possible concrete completion of a gap, together with the translation of TeSSLa specifications that operate directly on them.

If this is right

  • Runtime verification can continue on incomplete traces instead of failing when data is missing.
  • Outputs remain sound even when events carry imprecise values inside or across gaps.
  • The method applies to non-synchronized timed event streams as used by TeSSLa.
  • Implementation via macros on the original TeSSLa tool makes the technique immediately usable.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same abstraction pattern could be applied to other stream runtime verification languages beyond TeSSLa.
  • The technique might support monitoring in distributed or sensor-based systems where communication loss routinely creates gaps.
  • Further work could combine the abstract streams with statistical models that assign probabilities to different gap completions.

Load-bearing premise

Abstract event streams can be defined so that every possible concrete completion of a gap is captured and the translated specification preserves soundness for all such completions.

What would settle it

A concrete trace that completes a gap such that the output it produces lies outside the range reported by the abstract monitor would falsify the soundness guarantee.

Figures

Figures reproduced from arXiv: 1907.07761 by C\'esar S\'anchez, Daniel Thoma, Malte Schmitz, Martin Leucker, Torben Scheffel.

Figure 1
Figure 1. Figure 1: Example trace for a typical SRV specification (left) with two input streams values (with numeric values) and resets (with no internal value). The intention of the specification is to accumulate in the output stream sum all values since the last reset. The intermediate stream cond is derived from the input streams indicating if reset has currently the most recent event, and thus the sum should be reset to 0… view at source ↗
Figure 2
Figure 2. Figure 2: Example trace of the abstract queue specification. 5 Abstractions for Sliding Windows In this section we demonstrate how to apply the techniques presented in this paper to specifications with richer data domains. In particular, we show now a TeSSLa specification that uses a queue to compute the average load of a processor in the last five time units. The moving window is realized using a queue storing all … view at source ↗
Figure 3
Figure 3. Figure 3: Empirical results. The first three examples represent the class of common, simple TeSSLa specifications without complex interdependencies and no generation of additional events with delay: Reset-count counts between reset events; reset-sum sums up events between reset events; and filter-example filters events occurring in a certain timing-pattern. For these common specifications the overhead is small and t… view at source ↗
read the original abstract

Runtime Verification (RV) studies how to analyze execution traces of a system under observation. Stream Runtime Verification (SRV) applies stream transformations to obtain information from observed traces. Incomplete traces with information missing in gaps pose a common challenge when applying RV and SRV techniques to real-world systems as RV approaches typically require the complete trace without missing parts. This paper presents a solution to perform SRV on incomplete traces based on abstraction. We use TeSSLa as specification language for non-synchronized timed event streams and define abstract event streams representing the set of all possible traces that could have occurred during gaps in the input trace. We show how to translate a TeSSLa specification to its abstract counterpart that can propagate gaps through the transformation of the input streams and thus generate sound outputs even if the input streams contain gaps and events with imprecise values. The solution has been implemented as a set of macros for the original TeSSLa and an empirical evaluation shows the feasibility of the approach.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The paper claims to extend TeSSLa-based stream runtime verification to incomplete timed event streams containing gaps and imprecise event values. It defines abstract event streams as the set of all possible concrete completions of such gaps and supplies a translation of TeSSLa operators into abstract counterparts whose outputs remain sound over-approximations for every possible concrete completion.

Significance. If the translation is shown to be sound, the work directly addresses a practical obstacle in applying SRV to real traces that suffer data loss or sensor imprecision. The reduction to a set of macros for the existing TeSSLa engine together with an empirical evaluation supplies concrete evidence of implementability.

minor comments (3)
  1. [§3] §3 (or the section presenting the abstract semantics): the definition of abstract event streams should explicitly state whether the abstraction is required to be the least fixed point or merely any sound over-approximation; the current wording leaves this ambiguous for the subsequent soundness argument.
  2. [Evaluation section] The empirical evaluation reports only runtime overhead; adding a column or paragraph that quantifies the precision loss (e.g., fraction of outputs that remain definite versus “gap”) would strengthen the practicality claim.
  3. Notation: the paper uses both “abstract stream” and “abstract event stream” interchangeably; a single defined term would improve readability.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary, the assessment of significance, and the recommendation of minor revision. No specific major comments were provided in the report.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper defines abstract event streams as the set of all possible concrete completions of gaps (including imprecise values) and provides translation rules from TeSSLa to an abstract counterpart that propagates gaps while preserving soundness. This is a direct constructive definition with formal semantics supplied in the manuscript; no equations reduce by construction to prior fitted values, no load-bearing self-citations are invoked for uniqueness or ansatz, and the central claim does not rename a known result or smuggle assumptions via citation. The approach is self-contained as a new abstraction construction.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 1 invented entities

Only the abstract is available; no explicit free parameters, background axioms, or additional invented entities beyond the core abstraction mechanism are identifiable.

invented entities (1)
  • abstract event streams no independent evidence
    purpose: represent the set of all possible traces during gaps
    Introduced to model uncertainty in incomplete traces

pith-pipeline@v0.9.0 · 5708 in / 1100 out tokens · 19473 ms · 2026-05-24T23:28:55.710352+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

24 extracted references · 24 canonical work pages · 1 internal anchor

  1. [1]

    In: ESOP

    Alur, R., Fisman, D., Raghothaman, M.: Regular programming for quantitative properties of data streams. In: ESOP. pp. 15–40. Springer (2016)

    work page 2016

  2. [2]

    Asarin, E., Caspi, P., Maler, O.: Timed regular expressions. J. ACM49(2), 172–206 (2002)

    work page 2002

  3. [3]

    In: FSTTCS

    Basin, D.A., Klaedtke, F., Zalinescu, E.: Failure-aware runtime verification of distributed systems. In: FSTTCS. LIPIcs, vol. 45, pp. 590–603. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)

    work page 2015

  4. [4]

    Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM T. Softw. Eng. Meth.20(4), 14 (2011)

    work page 2011

  5. [5]

    The foundations of Esterel, pp

    Berry, G.: Proof, language, and interaction: essays in honour of Robin Milner, chap. The foundations of Esterel, pp. 425–454. MIT Press (2000)

    work page 2000

  6. [6]

    Bozelli, L., Sánchez, C.: Foundations of Boolean stream runtime verification. In: RV. LNCS, vol. 8734, pp. 64–79. Springer (2014)

    work page 2014

  7. [7]

    In: SBMF

    Convent, L., Hungerecker, S., Leucker, M., Scheffel, T., Schmitz, M., Thoma, D.: Tessla: Temporal stream-based specification language. In: SBMF. LNCS, Springer (2018)

    work page 2018

  8. [8]

    In: POPL

    Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL. pp. 238–252. ACM (1977)

    work page 1977

  9. [9]

    In: POPL

    Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL. pp. 238–252. ACM Press (1977)

    work page 1977

  10. [10]

    Journal of Logic and Computation 2(4), 511–547 (1992)

    Cousot, P., Cousot, R.: Abstract interpretation frameworks. Journal of Logic and Computation 2(4), 511–547 (1992)

    work page 1992

  11. [11]

    In: TIME

    D’Angelo, B., Sankaranarayanan, S., Sánchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: LOLA: runtime monitoring of synchronous systems. In: TIME. pp. 166–174. IEEE (2005)

    work page 2005

  12. [12]

    In: Proc

    Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Campenhout, D.V.: Reasoning with temporal logic on truncated paths. In: Proc. of CAV’03. pp. 27–39. LNCS 2725, Springer (2003)

    work page 2003

  13. [13]

    In: Proc

    Eliot, C., Hudak, P.: Functional reactive animation. In: Proc. of ICFP’07. pp. 163–173. ACM (1997)

    work page 1997

  14. [14]

    Faymonville, P., Finkbeiner, B., Schirmer, S., Torfah, H.: A stream-based speci- fication language for network monitoring. In: RV. pp. 152–168. LNCS, Springer (2016)

    work page 2016

  15. [15]

    Real-time Stream-based Monitoring

    Faymonville, P., Finkbeiner, B., Schwenger, M., Torfah, H.: Real-time Stream-based Monitoring. arXiv:1711.03829 (Nov 2017),http://arxiv.org/abs/1711.03829

    work page internal anchor Pith review Pith/arXiv arXiv 2017

  16. [16]

    In: Proc

    Gautier, T., Le Guernic, P., Besnard, L.:SIGNAL: A declarative language for synchronous programming of real-time systems. In: Proc. of FPCA’87. pp. 257–277. LNCS 274, Springer (1987)

    work page 1987

  17. [17]

    Gorostiaga, F., Sánchez, C.: Striver: Stream runtime verification for real-time event-streams. In: RV. pp. 282–298. LNCS, Springer (2018)

    work page 2018

  18. [18]

    In: Proc

    Halbwachs, N., Caspi, P., Pilaud, D., Plaice, J.: Lustre: a declarative language for programming synchronous systems. In: Proc. of POPL’87. pp. 178–188. ACM Press (1987) 18 M. Leucker, C. Sánchez, T. Scheffel, M. Schmitz, and D. Thoma

    work page 1987

  19. [19]

    In: TACAS

    Havelund, K., Roşu, G.: Synthesizing monitors for safety properties. In: TACAS. pp. 342–356. LNCS, Springer (2002)

    work page 2002

  20. [20]

    In: FTRTFT

    Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: FTRTFT. pp. 152–166 (2004)

    work page 2004

  21. [21]

    Springer, New York (1995)

    Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)

    work page 1995

  22. [22]

    ENTCS 89(2), 226–245 (2003)

    Sen, K., Roşu, G.: Generating optimal monitors for extended regular expressions. ENTCS 89(2), 226–245 (2003)

    work page 2003

  23. [23]

    Stoller, S.D., Bartocci, E., Seyster, J., Grosu, R., Havelund, K., Smolka, S.A., Zadok, E.: Runtime verification with state estimation. In: RV. Lecture Notes in Computer Science, vol. 7186, pp. 193–207. Springer (2011)

    work page 2011

  24. [24]

    Wang, S., Ayoub, A., Sokolsky, O., Lee, I.: Runtime verification of traces under recording uncertainty. In: RV. pp. 442–456. LNCS, Springer (2011) Runtime Verification For Timed Event Streams With Partial Information 19 A TeSSLa Evaluation Example Consider the equation y = merge ( lift ( + 1 )( last(y, x) ) , 0 ) where 0 = zero = const(0, unit) = const(0, ∞...

    work page 2011