Synthesis from hyperproperties

Area of Science:

• Formal methods
• Computer science
• Logic

Background:

• Hyperproperties generalize trace properties to sets of traces, crucial for policies like noninterference.
• Standard temporal logics (LTL, CTL) cannot express hyperproperties.
• HyperLTL offers a framework for these complex properties, encompassing realizability extensions.

Purpose of the Study:

• Investigate the reactive synthesis problem for hyperproperties specified in HyperLTL.
• Determine the decidability of synthesis for various HyperLTL fragments.
• Develop procedures for synthesizing systems and generating counterexamples for universal HyperLTL.

Main Methods:

• Formal analysis of the synthesis problem for HyperLTL.
• Identification and characterization of decidable fragments of HyperLTL.
• Development of a semi-decision procedure for universal HyperLTL.

Main Results:

• The synthesis problem is undecidable for full HyperLTL.
• Decidability is retained for the $$, $$, and $$ fragments of HyperLTL.
• A semi-decision procedure for universal HyperLTL constructs implementations and counterexamples.

Conclusions:

• Synthesis for hyperproperties is feasible within specific HyperLTL fragments.
• The study provides a foundation for synthesizing systems with complex security and information-flow guarantees.
• Experimental results demonstrate the practical applicability of the developed methods.