14 citations · 19 across the 11 of their papers we have counts for
9 papers · 1 filter
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…
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…
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…
The Complexity of Second-order HyperLTL
Hadar Frenkel, Gaëtan Regaud, Martin Zimmermann
We determine the complexity of second-order HyperLTL satisfiability, finite-state satisfiability, and model-checking: All three are equivalent to truth in third-order arithmetic. W…
Second-Order Hyperproperties
Raven Beutner, Bernd Finkbeiner, Hadar Frenkel +1
We introduce HyperLTL, a temporal logic for the specification of hyperproperties that allows for second-order quantification over sets of traces. Unlike first-order temporal lo…
Automata-Based Software Model Checking of Hyperproperties
Bernd Finkbeiner, Hadar Frenkel, Jana Hofmann +1
We develop model checking algorithms for Temporal Stream Logic (TSL) and Hyper Temporal Stream Logic (HyperTSL) modulo theories. TSL extends Linear Temporal Logic (LTL) with memory…
Explaining Hyperproperty Violations
Norine Coenen, Raimund Dachselt, Bernd Finkbeiner +5
Hyperproperties relate multiple computation traces to each other. Model checkers for hyperproperties thus return, in case a system model violates the specification, a set of traces…
Inferring Symbolic Automata
Dana Fisman, Hadar Frenkel, Sandra Zilles
We study the learnability of symbolic finite state automata (SFA), a model shown useful in many applications in software verification. The state-of-the-art literature on this topic…