27 citations · 30 across the 16 of their papers we have counts for
7 papers · 1 filter
Quantitative Monitoring of Signal First-Order Logic
Marek Chalupa, Thomas A. Henzinger, N. Ege Saraç +1
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…
Flavors of Quantifiers in Hyperlogics
Marek Chalupa, Thomas A. Henzinger, Ana Oliveira da Costa
Hypertrace logic is a sorted first-order logic with separate sorts for time and execution traces. Its formulas specify hyperproperties, which are properties relating multiple trace…
Monitoring Hyperproperties over Observed and Constructed Traces
Marek Chalupa, Thomas A. Henzinger, Ana Oliveira da Costa
We study the problem of monitoring at runtime whether a system fulfills a specification defined by a hyperproperty, such as linearizability or variants of non-interference. For thi…
Alignment Monitoring
Thomas A. Henzinger, Konstantin Kueffner, Vasu Singh +1
Formal verification provides assurances that a probabilistic system satisfies its specification--conditioned on the system model being aligned with reality. We propose alignment mo…
Quantitative and Approximate Monitoring
Thomas A. Henzinger, N. Ege Saraç
In runtime verification, a monitor watches a trace of a system and, if possible, decides after observing each finite prefix whether or not the unknown infinite trace satisfies a gi…
Supermartingale Certificates for Quantitative Omega-regular Verification and Control
Thomas A. Henzinger, Kaushik Mallik, Pouya Sadeghi +1
We present the first supermartingale certificate for quantitative -regular properties of discrete-time infinite-state stochastic systems. Our certificate is defined on the prod…