Optimal Policy Generation for Partially Satisfiable Co-Safe LTL Specifications
Authors: Bruno Lacerda, David Parker, Nick Hawes
IJCAI 2015 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We illustrate and evaluate our approach in a robot task planning scenario, where the task is to visit a set of rooms that may be inaccessible during execution. We implemented our approach in the widely used PRISM model checker [Kwiatkowska et al., 2011]... The MDP model used for the scenario on Fig. 2 has 10,206 states and 49,572 transitions. ... Based on the values in Fig. 2 the probability of the policy satisfying the specification is 0.729, with an expected time of 11.8 minutes. The values for the expected time of success and failure are 13.8 and 6.42, respectively. |
| Researcher Affiliation | Academia | Bruno Lacerda, David Parker and Nick Hawes School of Computer Science, University of Birmingham Birmingham, United Kingdom {b.lacerda, d.a.parker, n.a.hawes}@cs.bham.ac.uk |
| Pseudocode | No | The paper describes procedures and calculations but does not include any explicitly labeled 'Pseudocode' or 'Algorithm' blocks. |
| Open Source Code | No | The paper does not provide any concrete access information (e.g., repository link, explicit statement of code release) for the methodology's source code. |
| Open Datasets | No | The paper uses a custom-designed scenario and topological map for evaluation, but does not provide concrete access information (link, DOI, formal citation for a public dataset) for this experimental data. |
| Dataset Splits | No | The paper describes a policy generation method for an MDP model, not a machine learning model trained on a dataset, hence the concept of train/validation/test splits is not directly applicable or mentioned for data partitioning. |
| Hardware Specification | Yes | on an Intel Core i7 @ 1.70GHz x 4 processor, 8GB of RAM |
| Software Dependencies | Yes | We implemented our approach in the widely used PRISM model checker [Kwiatkowska et al., 2011] |
| Experiment Setup | Yes | Consider the topological map of an office environment in Fig. 2. We assume that v0 should always be avoided... and that our task is to visit nodes v1, v6 and v18... The MDP model also includes the state of each door, and before navigating through a door the robot must check if it is open (we assume probability 0.9 of being open for each door). All navigation actions are successful with probability 1, except from v3 to v4, which might finish in v0, with probability 0.2. A cost structure, representing the expected time taken to move between each pair of nodes, is defined by a coarse distance between the nodes. |