Liu Yang, Ma Yan, Yang Yongsheng, Zheng Tingting
Institute of Logistics Science and Engineering, Shanghai Maritime University, Shanghai 201306, China.
School of Computing, National University of Singapore, Singapore 117417, Singapore.
Micromachines (Basel). 2021 Aug 31;12(9):1059. doi: 10.3390/mi12091059.
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.
微尺度信息物理系统（MCPSs）可以在系统模型马尔可夫决策过程（MDPs）层面，针对概率计算树逻辑（PCTL）中的期望需求，通过概率模型检验进行自动且形式化的评估。概率模型检验中的反例是需求违反的见证，可为MCPSs的调试、控制和综合提供有意义的信息。已证明求解概率模型检验MDP的最小反例是一个NP完全（非确定性多项式完全）问题。尽管为此设计了一些启发式方法，但通常很难确定启发式函数。本文首先提出用启发式方法优化的遗传算法，即启发式遗传算法，来为MCPSs的概率模型检验MDP模型生成反例。诊断子图用作紧凑的反例，MDP的诊断路径构成用于构建诊断子图的与或树。遗传算法的间接路径编码用于扩展状态空间的搜索范围，并且使用启发式交叉算子来生成更有效的诊断路径。开发了基于概率模型检验器PAT的原型工具，并使用一些案例（动态功率管理和一些通信协议）来说明其可行性和效率。
