Bayesian statistical model-checking of continuous stochastic logic
dc.contributor.author | Prabhakar, Pavithra | |
dc.date.accessioned | 2022-04-12T18:45:32Z | |
dc.date.available | 2022-04-12T18:45:32Z | |
dc.date.graduationmonth | May | |
dc.date.issued | 2022 | |
dc.description.abstract | Autonomous systems are transforming the society by enabling sophisticated technologies such as robotic surgery and driverless cars. On one hand, increased automation through removal of the human-in-the-loop promises enhanced efficiency, while, on the other hand, the highly uncertain and safety critical environments, such as, varying weather and road conditions, and the presence of pedestrians on the road, pose challenge to the design of reliable autonomous systems. Hence, there is an immediate need for a robust framework for certifying the correctness of autonomous systems. In this report, we explore verifying the correctness of uncertain autonomous systems modeled as discrete-time Markov chains (DTMCs) against correctness criteria provided as continuous stochastic logic (CSL) formulae. Statistical model-checking (SMC) is a paradigm for verification based on formulating the verification problem as a hypothesis testing prob- lem. We propose a novel statistical model-checking algorithm based on Bayesian hypothesis testing. While Bayesian approaches for simpler logics without nested probabilistic operators and Frequentist approaches for nested logic have been previously explored, the Bayesian ap- proach for CSL that has nested probabilistic operators has not been addressed. The challenge in the nested case arises from the fact that unlike in probabilistic model-checking (PMC), where we obtain a definitive answer for the model-checking problem for the sub-formulae, we only obtain a correct answer with a certain confidence, which needs to be factored into the recursive SMC algorithm. We have implemented our algorithm in a Python Toolbox, and present our evaluation on some benchmark examples. We observe that while both the Bayesian and frequentist SMC perform well in terms of inference, Bayesian SMC is more efficient in terms of the number of samples. On several examples, it even beats the state-of- the-art probabilistic model-checker PRISM. | |
dc.description.advisor | Christopher I. Vahl | |
dc.description.degree | Master of Science | |
dc.description.department | Department of Statistics | |
dc.description.level | Masters | |
dc.description.sponsorship | National Science Foundation; Office of Naval Research | |
dc.identifier.uri | https://hdl.handle.net/2097/42093 | |
dc.language.iso | en_US | |
dc.publisher | Kansas State University | |
dc.rights | © the author. This Item is protected by copyright and/or related rights. You are free to use this Item in any way that is permitted by the copyright and related rights legislation that applies to your use. For other uses you need to obtain permission from the rights-holder(s). | |
dc.rights.uri | http://rightsstatements.org/vocab/InC/1.0/ | |
dc.subject | Bayesian | |
dc.subject | Hypothesis testing | |
dc.subject | Formal verification | |
dc.subject | Statistical model-checking | |
dc.subject | Stochastic logic | |
dc.subject | Discrete-time Markov chains | |
dc.title | Bayesian statistical model-checking of continuous stochastic logic | |
dc.type | Report |