The datasets for finite-synthesis consists of three classes:
- The first one is from the Random family, composed of LTLf formulas formed by random conjunction, generated as described in ZTLPV17.
- The second one is from TV19 and BLTV20, which describes Two-player games, split into the Single-Counter, Double-Counters and Nim dataset families.
- The third one is from XLZSPV20, originated from RV07 and GH06, which consists of Pattern formuls, split into the GF and U dataset families.
Moreover, for each family, there are two versions referring to which player (agent or environment) moves first.
The Random datasets are constructed from basic cases taken from LTL synthesis datasets Lily and Load balancer. Formally, a random conjunction formula has the form:
where
is the number of conjuncts, or the length of the formula, and
is a randomly selected basic case. Variables
are chosen randomly from a set of
candidate variables. Given
and
(the size of the candidate variable set), we generate a formula
in the following way:
- Randomly select
basic cases;
- For each case
, substitute every variable
with a random new variable
chosen from
atomic propositions. If
. The same applies to the agent-variables.
This class of datasets has 1400 instances, from which there are 1000 are from DF21, and 400 are from ZTLPV17.
This dataset family is a simple example where the behavior of the system is completely determined by the actions of the environment. Therefore, the challenge in this family lies mostly in proving that the specification is realizable. The system stores an -bit counter (where
is the scaling parameter) which it must increment upon a signal by the environment. The system wins if the counter eventually overflows to
. To guarantee that the game is winning for the system, the specification assumes that the environment will send the increment signal at least once every two timesteps.
This dataset family is similar to the Single-Counter one, except that in this case there are two -bit counters, one incremented by the environment and another by the system. The goal of the system is for its counter to eventually catch up with the environment’s counter. To guarantee that this is achievable, the specification assumes that the environment cannot increment its counter twice in a row.
This dataset family describes a generalized version of the game of Nim Bouton1901 with heaps of
tokens each. The environment and the system take turns removing any number of tokens from one of the heaps, and the player who removes the last token loses.