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

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...

Full description

Bibliographic Details
Main Authors: Yang Liu, Yan Ma, Yongsheng Yang, Tingting Zheng
Format: Article
Language:English
Published: MDPI AG 2021-08-01
Series:Micromachines
Subjects:
probabilistic model checking
micro-scale cyber-physical systems
counterexample
genetic algorithm
Online Access:https://www.mdpi.com/2072-666X/12/9/1059

Internet

https://www.mdpi.com/2072-666X/12/9/1059

Similar Items