PV4 ⊧ BoSyHyperproves realizability of a given hyperproperty

Application domain/field

• Reactive synthesis
• LTL synthesis
• Bounded synthesis

Type of tool

Synthesis tool

Expected input

HyperLTL formula

Format:

JSON based format

Expected output

Whether a specification is realizable. If realizable, then a solution can be given.

Internals

• Implementation based on BoSy LTL synthesis tool.
• Uses Z3

Comments

• Synthesis tool for universal HyperLTL based on a bounded synthesis algorithm (i.e.: Given a specification in HyperLTL, it synthesizes a reactive system).
• HyperLTL is an extension of LTL with trace variables and explicit trace quantification. Hyperlogics (like HyperLTL) can be used to express things that relate multiple traces, e.g. absence of information leaks.