Probabilistic Model Checking of Robots Deployed in Extreme Environments
Authors: Xingyu Zhao, Valentin Robu, David Flynn, Fateme Dinmohammadi, Michael Fisher, Matt Webster8066-8074
AAAI 2019 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We demonstrate our approach using data from a real-world deployment of unmanned underwater vehicles in extreme environments. We demonstrate and evaluate our framework by simulated experiments based on the UUV example of Fig. 1. |
| Researcher Affiliation | Academia | 1School of Engineering & Physical Sciences, Heriot-Watt University, Edinburgh EH14 4AS, U.K. 2Center for Collective Intelligence, Massachusetts Institute of Technology, Cambridge MA 02139, U.S. 3Department of Computer Science, University of Liverpool, Liverpool L69 3BX, U.K. Email:{xingyu.zhao, v.robu, d.flynn, f.dinmohammadi}@hw.ac.uk, {mfisher, matt}@liverpool.ac.uk |
| Pseudocode | No | No pseudocode or algorithm blocks were found in the paper. |
| Open Source Code | No | The paper does not provide any statements about open-source code availability or links to code repositories. |
| Open Datasets | No | We illustrate our new method with an example of an unmanned underwater vehicle (UUV) in the context of a valve turning scenario from the PANDORA2 project which created UUVs that keep going under extreme uncertainty. and to simulate and collect data of both previous missions and the current one for the pre-mission and runtime verifications respectively, we use the PRISM simulation module. No concrete access information for the used data is provided. |
| Dataset Splits | No | The paper does not provide specific details about training, validation, or test dataset splits. |
| Hardware Specification | No | The paper does not provide specific hardware details (e.g., GPU/CPU models, memory amounts) used for running its experiments. |
| Software Dependencies | No | We use the tool PRISM (Kwiatkowska, Norman, and Parker 2011) and using the Para MC engine of PRISM. No specific version numbers for PRISM or other software dependencies are provided. |
| Experiment Setup | Yes | First, to simulate and collect data of both previous missions and the current one for the pre-mission and runtime verifications respectively, we use the PRISM simulation module by assuming the true unknown transitions probabilities in Fig. 1 are: a1 = 0.05, a2 = 0.03, b1 = 0.2, b2 = 0.1, x = 10 5, y = 0.001, v = 0.3, w = 0.01. For the optimal policy of state 1, we assign a random number in [25/40] for γ in each simulated mission to mimic the practical case of changing policies. Then, it results in 49 previous missions and a 50-th as the current one which explicitly using γ = 0.75 as the optimal probabilistic policy of state 1. At the pre-mission stage, given the data of previous 49 missions...together with the prior knowledge in Table 1, the posteriors by our Bayesian estimators are also listed there. |