3 citations · 8 across the 22 of their papers we have counts for
23 papers
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…
Less Effort, Shorter Proofs: Reinforcement Learning for Security Protocol Analysis in Tamarin
Matthias Cosler, Cas Cremers, Bernd Finkbeiner +2
Tools like Tamarin and ProVerif have achieved notable success in analyzing and verifying complex real-world protocols such as EMV, 5G, and WPA2, even detecting zero-day exploits. D…
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…
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…
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…
Learning Representations Through Contrastive Neural Model Checking
Vladimir Krsmanovic, Matthias Cosler, Mohamed Ghanem +1
Model checking is a key technique for verifying safety-critical systems against formal specifications, where recent applications of deep learning have shown promise. However, while…
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…
Hyper Strategy Logic
Raven Beutner, Bernd Finkbeiner
Strategy logic (SL) is a powerful temporal logic that enables strategic reasoning in multi-agent systems. SL supports explicit (first-order) quantification over strategies and prov…
Learning Better Representations From Less Data For Propositional Satisfiability
Mohamed Ghanem, Frederik Schmitt, Julian Siber +1
Training neural networks on NP-complete problems typically demands very large amounts of training data and often needs to be coupled with computationally expensive symbolic verifie…
On Alternating-Time Temporal Logic, Hyperproperties, and Strategy Sharing
Raven Beutner, Bernd Finkbeiner
Alternating-time temporal logic (ATL) is a well-established framework for formal reasoning about multi-agent systems. However, while ATL can reason about the strategic abil…
Leveraging Static Analysis: An IDE for RTLola
Bernd Finkbeiner, Florian Kohn, Malte Schledjewski
Runtime monitoring is an essential part of guaranteeing the safety of cyber-physical systems. Recently, runtime monitoring frameworks based on formal specification languages gained…
Proceedings Second International Workshop on Interactions, Games and Protocols
Johannes Reich, Bernd Finkbeiner
This volume contains the proceedings of the second International Workshop on Interactions, Games and Protocols (IWIGP 2012). The workshop was held in Tallinn on March 25, 2012, as…