Counterexample Generation for Probabilistic Model Checking Micro-Scale Cyber-Physical Systems

Micro-scale Cyber-Physical Systems (MCPSs) can be automatically and formally estimated by probabilistic model checking, on the level of system model MDPs (Markov Decision Processes) against desired requirements in PCTL (Probabilistic Computation Tree Logic). The counterexamples in probabilistic mode...

Descripción completa

Detalles Bibliográficos
Autores principales: Liu, Yang, Ma, Yan, Yang, Yongsheng, Zheng, Tingting
Formato: Online Artículo Texto
Lenguaje:English
Publicado: MDPI 2021
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC8470795/
https://www.ncbi.nlm.nih.gov/pubmed/34577703
http://dx.doi.org/10.3390/mi12091059

Internet

https://www.ncbi.nlm.nih.gov/pmc/articles/PMC8470795/
https://www.ncbi.nlm.nih.gov/pubmed/34577703
http://dx.doi.org/10.3390/mi12091059

Ejemplares similares