Effective Approach to LTLf Best-Effort Synthesis in Multi-Tier Environments
Authors: Benjamin Aminof, Giuseppe De Giacomo, Gianmarco Parretti, Sasha Rubin
IJCAI 2024 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | To show the practicality of the proposed approach, we provide symbolic implementations by leveraging the framework of [Zhu et al., 2017] and, using such implementations, perform an empirical evaluation on some scalable benchmarks. and 8 Implementation and Evaluation |
| Researcher Affiliation | Academia | Benjamin Aminof1 , Giuseppe De Giacomo1,2 , Gianmarco Parretti1 and Sasha Rubin3 1Universit a degli Studi di Roma La Sapienza 2University of Oxford 3University of Sydney |
| Pseudocode | Yes | Algorithm 0 SYNTHPOS(φ, E) and Algorithm 1 MULTIENVBESYNTH(φ, E1, , En) and Algorithm 2 ONTHEFLYBESYNTH(φ, E1, , En) |
| Open Source Code | Yes | We implemented Algorithm 2 in a tool called Mt Syft5...5https://github.com/GianmarcoDIAG/MtSyft |
| Open Datasets | Yes | To evaluate the performance of our implementations, we devised an extension of the counter game benchmarks presented in [De Giacomo et al., 2020b; Zhu et al., 2020] to construct multi-tier environment specifications. |
| Dataset Splits | No | The paper describes constructing specific benchmark instances ('counter game benchmarks') and running the synthesis algorithms on them. It details the parameters for generating these instances (e.g., number of bits, number of tiers, base conjuncts), but it does not specify traditional dataset splits (like train/validation/test percentages or counts) as it deals with a synthesis problem rather than training a machine learning model on a pre-existing dataset. |
| Hardware Specification | Yes | Experiments were run on a laptop with an operating system 64-bit Ubuntu 20.04, 3.6 GHz CPU, and 12 GB of memory. |
| Software Dependencies | Yes | We code Boolean functions representing transitions and final states of symbolic DFAs by BDDs [Bryant, 1992] with the BDD library CUDD 3.0.0 [Somenzi, 2016]. |
| Experiment Setup | Yes | Timeout was set to 300 seconds. and The counter game involves a k-bit counter... environment issues between 1 and 100 increment requests... Our benchmark consists of counter games with at most 10-bits. For each game, we constructed multi-tier environments with n tiers as follows: (i) we fixed a base conjunct Eℓ; (ii) stacked the tiers Eℓ, , Eℓ+n 1 in increments of 1. As base conjucts, we considered E1, and E10 to E90 in increments of 10. |