Planning as Model Checking in Hybrid Domains

Authors: Sergiy Bogomolov, Daniele Magazzeni, Andreas Podelski, Martin Wehrle

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

Reproducibility Variable Result LLM Response
Research Type Experimental 5 Case Study As a case study, we apply our translation with the Space Ex model checker (Frehse et al. 2011)... The results for unsolvable instances are reported in Table 1. ... The results are depicted in Table 2.
Researcher Affiliation Academia Sergiy Bogomolov University of Freiburg Germany bogom@cs.uni-freiburg.de Daniele Magazzeni King s College London United Kingdom daniele.magazzeni@kcl.ac.uk Andreas Podelski University of Freiburg Germany podelski@cs.uni-freiburg.de Martin Wehrle University of Basel Switzerland martin.wehrle@unibas.ch
Pseudocode No The paper describes the translation and models using text and diagrams, but it does not provide any structured pseudocode or algorithm blocks.
Open Source Code No The paper does not provide any statement or link indicating that the source code for the described methodology is publicly available.
Open Datasets Yes We consider several instances (with growing size) of the generator (Howey, Long, and Fox 2004) and the car domains (Fox and Long 2006), which are standard and challenging benchmarks in the hybrid planning community.
Dataset Splits No The paper uses established benchmark domains but does not provide specific details regarding dataset splits (e.g., training, validation, testing percentages or counts) for its experiments.
Hardware Specification Yes The experiments are performed on an x64 Linux machine with 6 GB of RAM and an Intel i7 CPU (2.20GHz).
Software Dependencies No The paper mentions the use of 'Space Ex model checker (Frehse et al. 2011)', 'Colin (Coles et al. 2012)', and 'UPMurphi (Della Penna, Magazzeni, and Mercorio 2012)', but does not provide specific version numbers for these or other software dependencies.
Experiment Setup No The paper details the formal translation scheme and the structure of the hybrid automata, but it does not specify concrete experimental setup details such as hyperparameters or system-level training settings typically found in empirical studies (e.g., learning rates, batch sizes, optimization algorithms).