PV4 ⊧ BoSyHyperproves realizability of a given hyperproperty
- Reactive synthesis
- LTL synthesis
- Bounded synthesis
Type of toolSynthesis tool
Expected inputHyperLTL formula
Format:JSON based format
Expected outputWhether a specification is realizable. If realizable, then a solution can be given.
- 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.