Synthesizing reactive systems from hyperproperties

DOI10.1007/978-3-319-96145-3_16MaRDI QIDQ6045009zbMATH OpenFDO

Authors Bernd Finkbeiner, Christopher Hahn, Philip Lukert, Marvin Stenger, Leander Tentrup

Publication date 26 May 2023

Published in Computer Aided Verification (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Abstract: We study the reactive synthesis problem for hyperproperties given as formulas of the temporal logic HyperLTL. Hyperproperties generalize trace properties, i.e., sets of traces, to sets of sets of traces. Typical examples are information-flow policies like noninterference, which stipulate that no sensitive data must leak into the public domain. Such properties cannot be expressed in standard linear or branching-time temporal logics like LTL, CTL, or CTL${}^{\ast }$. We show that, while the synthesis problem is undecidable for full HyperLTL, it remains decidable for the $exist{s}^{\ast }$, $exist{s}^{\ast }foral{l}^1$, and the $mathitlinear;foral{l}^{\ast }$ fragments. Beyond these fragments, the synthesis problem immediately becomes undecidable. For universal HyperLTL, we present a semi-decision procedure that constructs implementations and counterexamples up to a given bound. We report encouraging experimental results obtained with a prototype implementation on example specifications with hyperproperties like symmetric responses, secrecy, and information-flow.

Recommendations

• Synthesizing reactive programs
• Synthesizing skeletons for reactive systems
• scientific article; zbMATH DE number 4085004
• Reasoning about reactive systems
• Verification and synthesis of reactive programs
• Bounded synthesis of reactive programs
• scientific article; zbMATH DE number 2112979
• scientific article; zbMATH DE number 1973127

Cited in

(11)

• HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems
• Verifying hyperliveness
• Fairness, assumptions, and guarantees for extended bounded response \textsf{LTL+P} synthesis
• Efficient loop conditions for bounded model checking hyperproperties
• Parameter synthesis for probabilistic hyperproperties
• Runtime enforcement of hyperproperties
• Synthesis from hyperproperties
• Information Flow Guided Synthesis
• Finite-word hyperlanguages
• Realizing \(\omega\)-regular hyperproperties
• Deductive controller synthesis for probabilistic hyperproperties

This page was built for publication: Synthesizing reactive systems from hyperproperties

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