华东师范大学学报（自然科学版）Issue(4)：18-29,12.DOI:10.3969/j.issn.1000-5641.2024.04.002
一种基于机器学习的模型检查算法性能预测方法
Machine-learning-based model checker performance prediction
张枨宇 1蒲戈光 2诸嘉逸 2黄怿豪 3杨迪 2李建文 2缪炜恺 2阎迪 4顾斌 5詹乃军6
作者信息
- 1. 苏黎世联邦理工学院 计算机科学学院,苏黎世 8006
- 2. 华东师范大学 软件工程学院,上海 200062
- 3. 南洋理工大学 计算机科学与技术学院,新加坡 211106
- 4. 中航商用航空发动机有限责任公司,上海 200241
- 5. 中国航天科技集团有限公司,北京 100048
- 6. 中国科学院 软件研究所,北京 100190
- 折叠
摘要
Abstract
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.关键词
模型检查/与非图/组合模型检查器Key words
model checking/and-inverter graph/portfolio-based model checker分类
信息技术与安全科学引用本文复制引用
张枨宇,蒲戈光,诸嘉逸,黄怿豪,杨迪,李建文,缪炜恺,阎迪,顾斌,詹乃军..一种基于机器学习的模型检查算法性能预测方法[J].华东师范大学学报（自然科学版）,2024,(4):18-29,12.
