Synthesis from Satisficing and Temporal Goals
Authors: Suguman Bansal, Lydia Kavraki, Moshe Y. Vardi, Andrew Wells9679-9686
AAAI 2022 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | The objective of our case studies is to demonstrate the utility of reactive synthesis from LTL and satisficing goals in realistic domains inspired from robotics and planning. Since ours is the first algorithm to offer theoretical guarantees with fractional discount factors, there are not any baselines to compare to. So, we focus on our scalability trends and identify future scalability opportunities. Our evaluation demonstrates that our solution successfully scales to very large benchmarks. Despite their difficulty, we solve almost all of our benchmarks (Figure 5). Runtime examination indicates that our algorithm is linear in size of the game and the comparator, in practice. The scalability trends in size of the game for varying discount factors are shown in Figure 3. Determining the dependence on the comparator automata is more involved since its size depends on several parameters, namely positive reward, the discount factor, and the approximation factor. Figure 4 suggests the algorithm is linear in positive reward. |
| Researcher Affiliation | Collaboration | Suguman Bansal,1 Lydia Kavraki, 2 Moshe Y. Vardi, 2 Andrew Wells 2,3 1 University of Pennsylvania 2 Rice University 3 Tesla |
| Pseudocode | No | The paper describes its algorithms and constructions mathematically and in prose (e.g., Section 4, 5) but does not include structured pseudocode or an algorithm block. |
| Open Source Code | Yes | Source code and benchmarks are open source1. 1https://github.com/suguman/Non Integer Games |
| Open Datasets | Yes | Source code and benchmarks are open source1. 1https://github.com/suguman/Non Integer Games |
| Dataset Splits | No | The paper evaluates its algorithm on specific problem instances and environments ('Grid World', 'Conveyor Belt') with varying parameters (e.g., n=4, 6, 8, 10 for Grid World). It does not use or specify traditional train/validation/test dataset splits. |
| Hardware Specification | Yes | Our prototype is implemented in C + + on Ubuntu 18.04LTS. Experiments are run on an i7-4770 with 32GBs of RAM with a timeout of 750 sec. |
| Software Dependencies | No | Our prototype is implemented in C + + on Ubuntu 18.04LTS. Experiments are run on an i7-4770 with 32GBs of RAM with a timeout of 750 sec. This lists the programming language and operating system but no specific software dependencies with version numbers (e.g., specific C++ libraries or compilers). |
| Experiment Setup | Yes | On grid world, we take n = 4, 6, 8, 10. On conveyor belt, we take r c = 4 3, 5 3 with 2 or 3 blocks. Every benchmark is run with d = 1.5, 1.25, 1.125 (k = 1, 2, 3), approx. factor ε = 0.5 (p = 1) and threshold v = 0. |