一种基于机器学习的模型检查算法性能预测方法  

Machine-learning-based model checker performance prediction

作　　者：张枨宇 诸嘉逸 黄怿豪 杨迪[2] 李建文[2] 缪炜恺[2] 阎迪 顾斌 詹乃军[6] 蒲戈光[2] ZHANG Chengyu;ZHU Jiayi;HUANG Yihao;YANG Di;LI Jianwen;MIAO Weikai;YAN Di;GU Bin;ZHAN Naijun;PU Geguang(Department of Computer Science,ETH Zurich,Zurich 8006,Switzerland;Software Engineering Institute,East China Normal University,Shanghai 200062,China;College of Computer Science and Technology,Nanyang Technological University,Singapore 211106,Singapore;Aero Engine Corporation of China,Shanghai 200241,China;China Aerospace Science and Technology Corporation,Beijing100048,China;The Institute of Software,Chinese Academy of Sciences,Beijing 100190,China)

机构地区：[1]苏黎世联邦理工学院计算机科学学院,苏黎世8006 [2]华东师范大学软件工程学院,上海200062 [3]南洋理工大学计算机科学与技术学院,新加坡211106 [4]中航商用航空发动机有限责任公司,上海200241 [5]中国航天科技集团有限公司,北京100048 [6]中国科学院软件研究所,北京100190

出　　处：《华东师范大学学报（自然科学版）》2024年第4期18-29,共12页Journal of East China Normal University(Natural Science)

摘　　要：与非图模型是一种表示电路设计的通用基础形式,同时也是模型检查器的一种通用输入格式.介绍了一种基于与非图结构编码的特征提取方法,并基于该方法实现了一种快速的组合模型检查器Liquid.所提出的结构编码的核心思想:首先罗列出与非图中所有可能的子结构,再将每个子结构出现的次数编码成向量,该向量即作为与非图的特征向量参与之后的机器学习过程.由于各种模型检查算法的性能在不同的与非图上参差不齐,Liquid的设计目标是组合多种模型检查算法,针对不同的与非图使用机器学习模型挑选出合适的算法.收集了目前所有的模型检查器基准测试集作为实验数据集并进行了实验.实验结果表明,Liquid在实验数据集上的表现优于所有组合中的独立模型检查算法,并有着不错的预测准确率.同时,还从多个维度分析了Liquid有效的原因.An and-inverter graph(AIG)is a representation of electrical circuits typically passed as input into a model checker.In this paper,we propose an AIG structural encoding that we use to extract the features of AIGs and construct a portfolio-based model checker called Liquid.The underlying concept of the proposed structural encoding is the enumeration of all possible AIG substructures,with the frequency of each substructure encoded as a feature vector for use in subsequent machine-learning processes.Because the performance of model-checking algorithms varies across different AIGs,Liquid combines multiple such algorithms and selects the algorithm appropriate for a given AIG via machine learning.In our experiments,Liquid outperformed all state-of-the-art model checkers in the portfolio,achieving a high prediction accuracy.We further studied the effectiveness of Liquid from several perspectives.

关 键 词：模型检查 与非图 组合模型检查器 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]