3 citations · 8 across the 22 of their papers we have counts for
15 papers · 1 filter
Disintegration Temporal Logic for Probabilistic Hyperproperties
Mishel Carelli, Bernd Finkbeiner
We introduce Disintegration Temporal Logic (DTL), a new probabilistic temporal logic that can express a wide range of probabilistic hyperproperties, including probabilistic non-int…
Complexity of Model Checking Second-Order Hyperproperties on Finite Structures
Bernd Finkbeiner, Hadar Frenkel, Tim Rohde
We study the model checking problem of Hyper2LTL over finite structures. Hyper2LTL is a second-order hyperlogic, that extends the well-studied logic HyperLTL by adding quantificati…
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…
Explainability Requirements as Hyperproperties
Bernd Finkbeiner, Julian Siber
Explainability is emerging as a key requirement for autonomous systems. While many works have focused on what constitutes a valid explanation, few have considered formalizing expla…
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…
An Information-Flow Perspective on Explainability Requirements: Specification and Verification
Bernd Finkbeiner, Hadar Frenkel, Julian Siber
Explainable systems expose information about why certain observed effects are happening to the agents interacting with them. We argue that this constitutes a positive flow of infor…
Closure and Complexity of Temporal Causality
Mishel Carelli, Bernd Finkbeiner, Julian Siber
Temporal causality defines what property causes some observed temporal behavior (the effect) in a given computation, based on a counterfactual analysis of similar computations. In…
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…
Counterfactual Explanations for MITL Violations
Bernd Finkbeiner, Felix Jahn, Julian Siber
MITL is a temporal logic that facilitates the verification of real-time systems by expressing the critical timing constraints placed on these systems. MITL specifications can be ch…
Syntax-Guided Automated Program Repair for Hyperproperties
Raven Beutner, Tzu-Han Hsu, Borzoo Bonakdarpour +1
We study the problem of automatically repairing infinite-state software programs w.r.t. temporal hyperproperties. As a first step, we present a repair approach for the temporal log…
Non-Deterministic Planning for Hyperproperty Verification
Raven Beutner, Bernd Finkbeiner
Non-deterministic planning aims to find a policy that achieves a given objective in an environment where actions have uncertain effects, and the agent - potentially - only observes…
Synthesis of Temporal Causality
Bernd Finkbeiner, Hadar Frenkel, Niklas Metzger +1
We present an automata-based algorithm to synthesize omega-regular causes for omega-regular effects on executions of a reactive system, such as counterexamples uncovered by a model…
Monitoring Second-Order Hyperproperties
Raven Beutner, Bernd Finkbeiner, Hadar Frenkel +1
Hyperproperties express the relationship between multiple executions of a system. This is needed in many AI-related fields, such as knowledge representation and planning, to captur…