Probabilistic Model Checking of Robots Deployed in Extreme Environments

Xingyu Zhao, Valentin Robu, David Flynn, Fateme Dinmohammadi, Michael Fisher, Matt Webster

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Robots are increasingly used to carry out critical missions in extreme environments that are hazardous for humans. This requires a high degree of operational autonomy under uncertain conditions, and poses new challenges for assuring the robot’s safety and reliability. In this paper, we develop a framework for probabilistic model checking on a layered Markov model to verify the safety and reliability requirements of such robots, both at pre-mission stage and during runtime. Two novel estimators based on conservative Bayesian inference and imprecise probability model with sets of priors are introduced to learn the unknown transition parameters from operational data. We demonstrate our approach using data from a real-world deployment of unmanned underwater vehicles in extreme environments.
Original languageEnglish
Title of host publicationProceedings of the Thirty-Third AAAI Conference on Artificial Intelligence
PublisherAAAI Press
Pages8066-8074
Number of pages9
ISBN (Print)9781577358091
DOIs
Publication statusPublished - 17 Jul 2019
Event33rd AAAI Conference on Artificial Intelligence 2019 - Honolulu, United States
Duration: 27 Jan 20191 Feb 2019

Publication series

NameProceedings of the AAAI Conference on Artificial Intelligence
Number1
Volume33
ISSN (Print)2159-5399
ISSN (Electronic)2374-3468

Conference

Conference33rd AAAI Conference on Artificial Intelligence 2019
Abbreviated titleAAAI-19
CountryUnited States
CityHonolulu
Period27/01/191/02/19

Fingerprint

Model checking
Robots
Statistical Models

Keywords

  • Probabilistic model checking
  • Conservative Bayesian Inference
  • Imprecise Probability
  • Extreme Environments

Cite this

Zhao, X., Robu, V., Flynn, D., Dinmohammadi, F., Fisher, M., & Webster, M. (2019). Probabilistic Model Checking of Robots Deployed in Extreme Environments. In Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence (pp. 8066-8074). (Proceedings of the AAAI Conference on Artificial Intelligence; Vol. 33, No. 1). AAAI Press. https://doi.org/10.1609/aaai.v33i01.33018066
Zhao, Xingyu ; Robu, Valentin ; Flynn, David ; Dinmohammadi, Fateme ; Fisher, Michael ; Webster, Matt. / Probabilistic Model Checking of Robots Deployed in Extreme Environments. Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence. AAAI Press, 2019. pp. 8066-8074 (Proceedings of the AAAI Conference on Artificial Intelligence; 1).
@inproceedings{fb18cbdca38a4781a3f4103a21c9111d,
title = "Probabilistic Model Checking of Robots Deployed in Extreme Environments",
abstract = "Robots are increasingly used to carry out critical missions in extreme environments that are hazardous for humans. This requires a high degree of operational autonomy under uncertain conditions, and poses new challenges for assuring the robot’s safety and reliability. In this paper, we develop a framework for probabilistic model checking on a layered Markov model to verify the safety and reliability requirements of such robots, both at pre-mission stage and during runtime. Two novel estimators based on conservative Bayesian inference and imprecise probability model with sets of priors are introduced to learn the unknown transition parameters from operational data. We demonstrate our approach using data from a real-world deployment of unmanned underwater vehicles in extreme environments.",
keywords = "Probabilistic model checking, Conservative Bayesian Inference, Imprecise Probability, Extreme Environments",
author = "Xingyu Zhao and Valentin Robu and David Flynn and Fateme Dinmohammadi and Michael Fisher and Matt Webster",
year = "2019",
month = "7",
day = "17",
doi = "10.1609/aaai.v33i01.33018066",
language = "English",
isbn = "9781577358091",
series = "Proceedings of the AAAI Conference on Artificial Intelligence",
publisher = "AAAI Press",
number = "1",
pages = "8066--8074",
booktitle = "Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence",

}

Zhao, X, Robu, V, Flynn, D, Dinmohammadi, F, Fisher, M & Webster, M 2019, Probabilistic Model Checking of Robots Deployed in Extreme Environments. in Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence. Proceedings of the AAAI Conference on Artificial Intelligence, no. 1, vol. 33, AAAI Press, pp. 8066-8074, 33rd AAAI Conference on Artificial Intelligence 2019, Honolulu, United States, 27/01/19. https://doi.org/10.1609/aaai.v33i01.33018066

Probabilistic Model Checking of Robots Deployed in Extreme Environments. / Zhao, Xingyu; Robu, Valentin; Flynn, David; Dinmohammadi, Fateme; Fisher, Michael; Webster, Matt.

Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence. AAAI Press, 2019. p. 8066-8074 (Proceedings of the AAAI Conference on Artificial Intelligence; Vol. 33, No. 1).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Probabilistic Model Checking of Robots Deployed in Extreme Environments

AU - Zhao, Xingyu

AU - Robu, Valentin

AU - Flynn, David

AU - Dinmohammadi, Fateme

AU - Fisher, Michael

AU - Webster, Matt

PY - 2019/7/17

Y1 - 2019/7/17

N2 - Robots are increasingly used to carry out critical missions in extreme environments that are hazardous for humans. This requires a high degree of operational autonomy under uncertain conditions, and poses new challenges for assuring the robot’s safety and reliability. In this paper, we develop a framework for probabilistic model checking on a layered Markov model to verify the safety and reliability requirements of such robots, both at pre-mission stage and during runtime. Two novel estimators based on conservative Bayesian inference and imprecise probability model with sets of priors are introduced to learn the unknown transition parameters from operational data. We demonstrate our approach using data from a real-world deployment of unmanned underwater vehicles in extreme environments.

AB - Robots are increasingly used to carry out critical missions in extreme environments that are hazardous for humans. This requires a high degree of operational autonomy under uncertain conditions, and poses new challenges for assuring the robot’s safety and reliability. In this paper, we develop a framework for probabilistic model checking on a layered Markov model to verify the safety and reliability requirements of such robots, both at pre-mission stage and during runtime. Two novel estimators based on conservative Bayesian inference and imprecise probability model with sets of priors are introduced to learn the unknown transition parameters from operational data. We demonstrate our approach using data from a real-world deployment of unmanned underwater vehicles in extreme environments.

KW - Probabilistic model checking

KW - Conservative Bayesian Inference

KW - Imprecise Probability

KW - Extreme Environments

U2 - 10.1609/aaai.v33i01.33018066

DO - 10.1609/aaai.v33i01.33018066

M3 - Conference contribution

SN - 9781577358091

T3 - Proceedings of the AAAI Conference on Artificial Intelligence

SP - 8066

EP - 8074

BT - Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence

PB - AAAI Press

ER -

Zhao X, Robu V, Flynn D, Dinmohammadi F, Fisher M, Webster M. Probabilistic Model Checking of Robots Deployed in Extreme Environments. In Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence. AAAI Press. 2019. p. 8066-8074. (Proceedings of the AAAI Conference on Artificial Intelligence; 1). https://doi.org/10.1609/aaai.v33i01.33018066