Robustness Envelopes for Temporal Plans

Authors: Michael Cashmore, Alessandro Cimatti, Daniele Magazzeni, Andrea Micheli, Parisa Zehtabi7538-7545

AAAI 2019 | Conference PDF | Archive PDF | Plain Text | LLM Run Details

Reproducibility Variable Result LLM Response
Research Type Experimental In this section, we present an experimental evaluation aimed at showing the immediate applicability of the technique: we prove that the validation of STN plans is effectively applicable to various domains taking very reasonable computational resources, and that the robustness envelope synthesis problem, while not scaling to huge plan and domains yet, can be solved by directly employing existing solvers and tools and shows promising results.
Researcher Affiliation Academia 1King s College London, United Kingdom {michael.cashmore, daniele.magazzeni, parisa.zehtabi}@kcl.ac.uk, 2Fondazione Bruno Kessler, Italy {cimatti, amicheli}@fbk.eu
Pseudocode No The paper describes the encoding in SMT and the steps of the approach but does not include a dedicated pseudocode block or algorithm listing.
Open Source Code Yes The implementation of the tool and all benchmarks are available online3. 3 http://es.fbk.eu/people/amicheli/resources/aaai2019
Open Datasets Yes As a case-study, we used three domains: Autonomous Underwater Vehicle (AUV) (Buksz et al. 2018), the Solar Rover (Piotrowski et al. 2016), and the linear generator from the PDDL+ benchmarks (Cashmore et al. 2016).
Dataset Splits No The paper does not provide specific training/validation/test dataset splits (percentages, counts, or explicit standard split citations) for reproduction of data partitioning. It describes the generation of STN plans for testing but not a train/validation/test split for a learning model.
Hardware Specification No The paper does not provide specific hardware details (like CPU/GPU models, processor types, or memory amounts) used for running its experiments.
Software Dependencies No The paper states: 'The tool is implemented in Python, and uses the Py SMT library (Gario and Micheli 2015)... We use the Virtual Substitution... provided by the MATHSAT5 (Cimatti et al. 2013) SMT solver... and the Z3 (de Moura and Bjørner 2008) solver...' While it mentions the tools and libraries, it does not provide specific version numbers for Python, Py SMT, MATHSAT5, or Z3.
Experiment Setup Yes We generated time-triggered plans for each problem instance using the planner SMTPLAN (Cashmore et al. 2016) for the linear generator and POPF (Coles et al. 2010) for the others. STN plans were then generated by relaxing the duration of each action in the time-triggered plan. For each plan, 10 STNs were generated, allowing the duration d of each action to lie between (d d 0.01 v) and (d + d 0.01 v) for v = 0 9. For the synthesis problem, we parametrized each domain by expressing constants as problem parameters: the time needed for a full recharge and the speed of the navigation actions in the AUV domain, the required charge for communication in the Solar Rover, and refuel rate in the linear generator domain.