Runtime enforcement of hyperproperties

DOI10.1007/978-3-030-88885-5_19zbMATH Open1497.68291arXiv2203.04146OpenAlexW3206405735MaRDI QIDQ2147207FDOQ2147207

Jana Hofmann, Norine Coenen, Bernd Finkbeiner, Yannick Schillo, Christopher Hahn

Publication date: 22 June 2022

Abstract: An enforcement mechanism monitors a reactive system for undesired behavior at runtime and corrects the system's output in case it violates the given specification. In this paper, we study the enforcement problem for hyperproperties, i.e., properties that relate multiple computation traces to each other. We elaborate the notion of sound and transparent enforcement mechanisms for hyperproperties in two trace input models: 1) the parallel trace input model, where the number of traces is known a-priori and all traces are produced and processed in parallel and 2) the sequential trace input model, where traces are processed sequentially and no a-priori bound on the number of traces is known. For both models, we study enforcement algorithms for specifications given as formulas in universally quantified HyperLTL, a temporal logic for hyperproperties. For the parallel model, we describe an enforcement mechanism based on parity games. For the sequential model, we show that enforcement is in general undecidable and present algorithms for reasonable simplifications of the problem (partial guarantees or the restriction to safety properties). Furthermore, we report on experimental results of our prototype implementation for the parallel model.

Full work available at URL: https://arxiv.org/abs/2203.04146

Mathematics Subject Classification ID

Applications of game theory (91A80) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Cites Work

• A new solution of Dijkstra's concurrent programming problem
• Title not available (Why is that?)
• On the menbership problem for functional and multivalued dependencies in relational databases
• Runtime enforcement of security policies on black box reactive programs
• Runtime enforcement monitors: Composition, synthesis, and enforcement abilities
• Program Repair for Hyperproperties
• Algorithms for model checking HyperLTL and HyperCTL\(^*\)
• Model checking quantitative hyperproperties
• Shield Synthesis:
• Verifying hyperliveness
• Monitoring hyperproperties
• Parity Games: Zielonka's Algorithm in Quasi-Polynomial Time
• Unifying Hyper and Epistemic Temporal Logics
• From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata
• Optimal enforcement of (timed) properties with uncontrollable events
• Synthesizing reactive systems from hyperproperties
• Constraint-based monitoring of hyperproperties

Cited In (8)

• Program Repair for Hyperproperties
• HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems
• Runtime enforcement with reordering, healing, and suppression
• Compositional runtime enforcement revisited
• Explaining Hyperproperty Violations
• Deciding hyperproperties combined with functional specifications
• Temporal team semantics revisited
• Title not available (Why is that?)

Uses Software

• PGSolver
• Strix

This page was built for publication: Runtime enforcement of hyperproperties

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2147207)