7 papers
Monitoring Discounted Sum Properties
Filip Cano, Thomas A. Henzinger, Konstantin Kueffner +1
Runtime monitoring of quantitative signals faces a fundamental trade-off between volatility and over-aggregation: instantaneous observations are noisy, while long-run averages obsc…
Extending QuAK with Nested Quantitative Automata
Thomas A. Henzinger, Nicolas Mazzocchi, N. Ege Saraç +1
Quantitative automata (QAs) extend finite-state automata on infinite words with weighted transitions to specify quantitative system properties. However, their finite weight sets ru…
Quantitative Language Automata
Thomas A. Henzinger, Pavol Kebis, Nicolas Mazzocchi +1
A quantitative word automaton (QWA) defines a function from infinite words to values. For example, every infinite run of a limit-average QWA A obtains a mean payoff, and every word…
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…
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…
Safety and Liveness of Quantitative Properties and Automata
Udi Boker, Thomas A. Henzinger, Nicolas Mazzocchi +1
Safety and liveness stand as fundamental concepts in formal languages, playing a key role in verification. The safety-liveness classification of boolean properties characterizes wh…