@inproceedings{cleaveland_monotonic_2022,
	title = {Monotonic {Safety} for {Scalable} and {Data}-{Efficient} {Probabilistic} {Safety} {Analysis}},
	doi = {10.1109/ICCPS54341.2022.00015},
	abstract = {Autonomous systems with machine learning-based perception can exhibit unpredictable behaviors that are difficult to quantify, let alone verify. Such behaviors are convenient to capture in proba-bilistic models, but probabilistic model checking of such models is difficult to scale - largely due to the non-determinism added to models as a prerequisite for provable conservatism. Statistical model checking (SMC) has been proposed to address the scalabil-ity issue. However it requires large amounts of data to account for the aforementioned non-determinism, which in turn limits its scalability. This work introduces a general technique for reduction of non-determinism based on assumptions of “monotonic safety”, which define a partial order between system states in terms of their probabilities of being safe. We exploit these assumptions to remove non-determinism from controller/plant models to drasti-cally speed up probabilistic model checking and statistical model checking while providing provably conservative estimates as long as the safety is indeed monotonic. Our experiments demonstrate model-checking speed-ups of an order of magnitude while main-taining acceptable accuracy and require much less data for accurate estimates when running SMC - even when monotonic safety does not perfectly hold and provable conservatism is not achieved.},
	booktitle = {2022 {ACM}/{IEEE} 13th {International} {Conference} on {Cyber}-{Physical} {Systems} ({ICCPS})},
	author = {Cleaveland, Matthew and Ruchkin, Ivan and Sokolsky, Oleg and Lee, Insup},
	month = may,
	year = {2022},
	keywords = {Data models, Model checking, monotonic safety, probabilistic \& statistical model checking, Probabilistic logic, Probability, Safety, Scalability, Sensitivity analysis},
	pages = {92--103},
	file = {IEEE Xplore Full Text PDF:/home/ivan/Dropbox/configs/zotero_storage/storage/T2R27287/Cleaveland et al. - 2022 - Monotonic Safety for Scalable and Data-Efficient P.pdf:application/pdf},
}