6 papers
Verifying Asynchronous Hyperproperties in Reactive Systems
Raven Beutner, Bernd Finkbeiner
Hyperproperties are system properties that relate multiple execution traces and commonly occur when specifying information-flow and security policies. Logics like HyperLTL utilize…
Checking Satisfiability of Hyperproperties using First-Order Logic
Raven Beutner, Bernd Finkbeiner
Hyperproperties are system properties that relate multiple execution traces and occur, e.g., when specifying security and information-flow properties. Checking if a hyperproperty i…
On Conformant Planning and Model-Checking of Hyperproperties
Raven Beutner, Bernd Finkbeiner
We study the connection of two problems within the planning and verification community: Conformant planning and model-checking of hyperproperties. Conformant planning is the task o…
Strategy Logic, Imperfect Information, and Hyperproperties
Raven Beutner, Bernd Finkbeiner
Strategy logic (SL) is a powerful temporal logic that enables first-class reasoning over strategic behavior in multi-agent systems (MAS). In many MASs, the agents (and their strate…
On Hyperproperty Verification, Quantifier Alternations, and Games under Partial Information
Raven Beutner, Bernd Finkbeiner
Hyperproperties generalize traditional trace properties by relating multiple execution traces rather than reasoning about individual runs in isolation. They provide a unified way t…
Visualizing Game-Based Certificates for Hyperproperty Verification
Raven Beutner, Bernd Finkbeiner, Angelina Göbl
Hyperproperties relate multiple executions of a system and are commonly used to specify security and information-flow policies. While many verification approaches for hyperproperti…