Probabilistic Model Checking of Robots Deployed in Extreme Environments

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

doi:10.1609/aaai.v33i01.33018066

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 proceeding › Conference contribution

27 Citations (Scopus)

72 Downloads (Pure)

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 language	English
Title of host publication	Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence
Publisher	AAAI Press
Pages	8066-8074
Number of pages	9
ISBN (Print)	9781577358091
DOIs	https://doi.org/10.1609/aaai.v33i01.33018066
Publication status	Published - 17 Jul 2019
Event	33rd AAAI Conference on Artificial Intelligence 2019 - Honolulu, United States Duration: 27 Jan 2019 → 1 Feb 2019

Publication series

Name	Proceedings of the AAAI Conference on Artificial Intelligence
Number	1
Volume	33
ISSN (Print)	2159-5399
ISSN (Electronic)	2374-3468

Conference

Conference	33rd AAAI Conference on Artificial Intelligence 2019
Abbreviated title	AAAI-19
Country/Territory	United States
City	Honolulu
Period	27/01/19 → 1/02/19

Keywords

Probabilistic model checking
Conservative Bayesian Inference
Imprecise Probability
Extreme Environments
robust estimation
runtime verification
safety-critical systems
safe AI
Assurance

Access to Document

10.1609/aaai.v33i01.33018066

Download pdf
Copyright © 2019, Association for the Advancement of Artificial Intelligence
Accepted author manuscript, 572 KB

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

@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{\textquoteright}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, robust estimation, runtime verification, safety-critical systems, safe AI, Assurance",

author = "Xingyu Zhao and Valentin Robu and David Flynn and Fateme Dinmohammadi and Michael Fisher and Matt Webster",

year = "2019",

month = jul,

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",

note = "33rd AAAI Conference on Artificial Intelligence 2019, AAAI-19 ; Conference date: 27-01-2019 Through 01-02-2019",

}

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, Hawaii, 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 et al.
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 proceeding › Conference 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

KW - robust estimation

KW - runtime verification

KW - safety-critical systems

KW - safe AI

KW - Assurance

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

T2 - 33rd AAAI Conference on Artificial Intelligence 2019

Y2 - 27 January 2019 through 1 February 2019

ER -

Probabilistic Model Checking of Robots Deployed in Extreme Environments

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this