5 papers
Tractable Hyperproperties for MDPs
Lina Gerlach, Tobias Winkler, Erika Ábrahám +2
Probabilistic hyperproperties describe probabilistic relations between multiple sets of executions in a stochastic system. Prominent examples include information-theoretic characte…
A Hyperlogic for Strategies in Stochastic Games (Extended Version)
Lina Gerlach, Christof Löding, Erika Ábrahám
We propose a probabilistic hyperlogic called HyperSt that can express hyperproperties of strategies in turn-based stochastic games. To the best of our knowledge, HyperSt is…
Efficient Probabilistic Model Checking for Relational Reachability (Extended Version)
Lina Gerlach, Tobias Winkler, Erika Ábrahám +2
Markov decision processes model systems subject to nondeterministic and probabilistic uncertainty. A plethora of verification techniques addresses variations of reachability proper…
Counterfactual Strategies for Markov Decision Processes
Paul Kobialka, Lina Gerlach, Francesco Leofante +3
Counterfactuals are widely used in AI to explain how minimal changes to a model's input can lead to a different output. However, established methods for computing counterfactuals t…
Introducing Asynchronicity to Probabilistic Hyperproperties
Lina Gerlach, Oyendrila Dobe, Erika Ábrahám +2
Probabilistic hyperproperties express probabilistic relations between different executions of systems with uncertain behavior. HyperPCTL allows to formalize such properties, where…