Please use this identifier to cite or link to this item:
DC FieldValue
dc.titleCounterexample generation for probabilistic model checking micro-scale cyber-physical systems
dc.contributor.authorLiu, Yang
dc.contributor.authorMa, Yan
dc.contributor.authorYang, Yongsheng
dc.contributor.authorZheng, Tingting
dc.identifier.citationLiu, 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.
dc.description.abstractMicro-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.
dc.rightsAttribution 4.0 International
dc.sourceScopus OA2021
dc.subjectGenetic algorithm
dc.subjectMicro-scale cyber-physical systems
dc.subjectProbabilistic model checking
dc.contributor.departmentDEPARTMENT OF COMPUTER SCIENCE
Appears in Collections:Students Publications

Show simple 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