10 papers
Shielding for Higher-Order Safety
Filip Cano, Thomas A. Henzinger, Konstantin Kueffner
Safety shields are runtime enforcement mechanisms that restrict the actions of a controller to guarantee safety. Classical shields are usually synthesised for state predicates: the…
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…
Confidence Sequences for Online Statistical Model Checking of Markov Decision Processes
Konstantin Kueffner, Tobias Meggendorfer, Maximilian Weininger +1
Markov decision processes (MDPs) are a classic model of decision making under uncertainty, exhibiting both non-deterministic choice as well as probabilistic uncertainty. Traditiona…
Energy Shields for Fairness
Filip Cano, Thomas A. Henzinger, Konstantin Kueffner
Runtime fairness is not a one-time constraint but a dynamic property evaluated over a sequence of decisions. To ensure fairness at runtime, it is necessary to account for past deci…
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…
Algorithmic Fairness: A Runtime Perspective
Filip Cano, Thomas A. Henzinger, Konstantin Kueffner
Fairness in AI is traditionally studied as a static property evaluated once, over a fixed dataset. However, real-world AI systems operate sequentially, with outcomes and environmen…