PV4 BoSyproves realisability of a given property

Application domain/field

Type of tool

Synthesis tool

Expected input

LTL formula

Format:

JSON based format

Expected output

Whether a specification is realisable. If realisable, then a solution can be extracted.

Internals

Constraint-solving The tool uses bounded synthesis, this means that it results in a minimal implementation.

Comments

BoSyHyper is from the same team but for synthesis of HyperLTL.
LTL Synthesis

Links

Last commit date

17 May 2021

Related papers

Last publication date

14 July 2020

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.