Please use this identifier to cite or link to this item:
Title: Counterexample generation for probabilistic model checking micro-scale cyber-physical systems
Authors: Liu, Yang
Ma, Yan
Yang, Yongsheng
Zheng, Tingting
Keywords: Counterexample
Genetic algorithm
Micro-scale cyber-physical systems
Probabilistic model checking
Issue Date: 31-Aug-2021
Publisher: MDPI
Citation: Liu, Yang, Ma, Yan, Yang, Yongsheng, Zheng, Tingting (2021-08-31). Counterexample generation for probabilistic model checking micro-scale cyber-physical systems. Micromachines 12 (9) : 1059. ScholarBank@NUS Repository.
Rights: Attribution 4.0 International
Abstract: 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 model checking are witnesses of requirements violation, which can provide the meaningful information for debugging, control, and synthesis of MCPSs. Solving the smallest counterexample for probabilistic model checking MDP has been proven to be an NPC (Non-deterministic Polynomial complete) problem. Although some heuristic methods are designed for this, it is usually difficult to fix the heuristic functions. In this paper, the Genetic algorithm optimized with heuristic, i.e., the heuristic Genetic algorithm, is firstly proposed to generate a counterexample for the probabilistic model checking MDP model of MCPSs. The diagnostic subgraph serves as a compact counterexample, and diagnostic paths of MDP constitute an AND/OR tree for constructing a diagnostic subgraph. Indirect path coding of the Genetic algorithm is used to extend the search range of the state space, and a heuristic crossover operator is used to generate more effective diagnostic paths. A prototype tool based on the probabilistic model checker PAT is developed, and some cases (dynamic power management and some communication protocols) are used to illustrate its feasibility and efficiency. © 2021 by the authors. Licensee MDPI, Basel, Switzerland.
Source Title: Micromachines
ISSN: 2072-666X
DOI: 10.3390/mi12091059
Rights: Attribution 4.0 International
Appears in Collections:Students Publications

Show full item record
Files in This Item:
File Description SizeFormatAccess SettingsVersion 
10_3390_mi12091059.pdf2 MBAdobe PDF



Google ScholarTM



This item is licensed under a Creative Commons License Creative Commons