5 papers · 1 filter
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…
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…
Automating the Analysis of Quantitative Automata with QuAK
Marek Chalupa, Thomas A. Henzinger, Nicolas Mazzocchi +1
Quantitative automata model beyond-boolean aspects of systems: every execution is mapped to a real number by incorporating weighted transitions and value functions that generalize…