一种基于机器学习的模型检查算法性能预测方法OA北大核心CSTPCD

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.