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...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2021-08-01
|
| Series: | Micromachines |
| Subjects: | |
| Online Access: | https://www.mdpi.com/2072-666X/12/9/1059 |