您当前所在位置: 首页 > 首发论文
动态公开评议须知

1. 评议人本着自愿的原则,秉持科学严谨的态度,从论文的科学性、创新性、表述性等方面给予客观公正的学术评价,亦可对研究提出改进方案或下一步发展的建议。

2. 论文若有勘误表、修改稿等更新的版本,建议评议人针对最新版本的论文进行同行评议。

3. 每位评议人对每篇论文有且仅有一次评议机会,评议结果将完全公示于网站上,一旦发布,不可更改、不可撤回,因此,在给予评议时请慎重考虑,认真对待,准确表述。

4. 同行评议仅限于学术范围内的合理讨论,评议人需承诺此次评议不存在利益往来、同行竞争、学术偏见等行为,不可进行任何人身攻击或恶意评价,一旦发现有不当评议的行为,评议结果将被撤销,并收回评审人的权限,此外,本站将保留追究责任的权利。

5. 论文所展示的星级为综合评定结果,是根据多位评议人的同行评议结果进行综合计算而得出的。

勘误表

上传勘误表说明

  • 1. 请按本站示例的“勘误表格式”要求,在文本框中编写勘误表;
  • 2. 本站只保留一版勘误表,每重新上传一次,即会覆盖之前的版本;
  • 3. 本站只针对原稿进行勘误,修改稿发布后,不可对原稿及修改稿再作勘误。

示例:

勘误表

上传勘误表说明

  • 1. 请按本站示例的“勘误表格式”要求,在文本框中编写勘误表;
  • 2. 本站只保留一版勘误表,每重新上传一次,即会覆盖之前的版本;
  • 3. 本站只针对原稿进行勘误,修改稿发布后,不可对原稿及修改稿再作勘误。

示例:

上传后印本

( 请提交PDF文档 )

* 后印本是指作者提交给期刊的预印本,经过同行评议和期刊的编辑后发表在正式期刊上的论文版本。作者自愿上传,上传前请查询出版商所允许的延缓公示的政策,若因此产生纠纷,本站概不负责。

发邮件给 王小芳 *

收件人:

收件人邮箱:

发件人邮箱:

发送内容:

0/300

论文收录信息

论文编号 201901-71
论文题目 使用多种机器学习算法预测CTL模型检测
文献类型
收录
期刊

上传封面

期刊名称(中文)

期刊名称(英文)

年, 卷(

上传封面

书名(中文)

书名(英文)

出版地

出版社

出版年

上传封面

书名(中文)

书名(英文)

出版地

出版社

出版年

上传封面

编者.论文集名称(中文) [c].

出版地 出版社 出版年-

编者.论文集名称(英文) [c].

出版地出版社 出版年-

上传封面

期刊名称(中文)

期刊名称(英文)

日期--

在线地址http://

上传封面

文题(中文)

文题(英文)

出版地

出版社,出版日期--

上传封面

文题(中文)

文题(英文)

出版地

出版社,出版日期--

英文作者写法:

中外文作者均姓前名后,姓大写,名的第一个字母大写,姓全称写出,名可只写第一个字母,其后不加实心圆点“.”,

作者之间用逗号“,”分隔,最后为实心圆点“.”,

示例1:原姓名写法:Albert Einstein,编入参考文献时写法:Einstein A.

示例2:原姓名写法:李时珍;编入参考文献时写法:LI S Z.

示例3:YELLAND R L,JONES S C,EASTON K S,et al.

上传修改稿说明:

1.修改稿的作者顺序及单位须与原文一致;

2.修改稿上传成功后,请勿上传相同内容的论文;

3.修改稿中必须要有相应的修改标记,如高亮修改内容,添加文字说明等,否则将作退稿处理。

4.请选择DOC或Latex中的一种文件格式上传。

上传doc论文   请上传模板编辑的DOC文件

上传latex论文

* 上传模板导出的pdf论文文件(须含页眉)

* 上传模板编辑的tex文件

回复成功!


  • 0

使用多种机器学习算法预测CTL模型检测

首发时间:2019-01-11

朱维军 1   

朱维军(1976-),男,副教授、硕导,主要研究方向:形式化方法、人工智能

樊永文 1    班绍桓 1   
  • 1、郑州大学信息工程学院,郑州,450001

摘要:计算树逻辑(CTL)模型检测现已应用在多个领域。然而,状态爆炸问题限制了计算树逻辑模型检测的进一步应用。研究人员已经提出了许多方法来解决这些问题。但是,由于该问题本身固有的复杂性的限制,在传统的模型检测技术框架内,根本问题难以被有效解决。我们的前期工作使用BT算法来预测CTL模型检测,取得了准确率轻微下降而效率大幅提高的结果。采用其他机器学习算法是否可以获得更加准确更加快速的CTL模型检测预测结果?为此,本文又使用了另外四种机器学习方法。首先,对于一些Kripke结构和CTL公式,使用CTL模型检测算法获得包含模型检测结果的数据集A。其次,CTL模型检测问题可以归结为机器学习的二元分类问题。换句话说,A中的一些记录作为随机森林(Random Forest,RF)算法、逻辑回归(Logistic Regression,LR)算法、决策树(Decision Tree,DT)算法和支持向量机(Support Vector Machine,SVM)算法的训练集,并且获得相应的机器学习模型M,利用M来预测CTL模型检测的结果。实验表明,基于RF方法的平均准确率为95.6%,基于LR方法的平均准确率为91.1%,基于DT方法的平均准确率为95.1%,基于SVM方法的平均准确率为94.9%。而且,基于RF方法的平均效率比传统的模型检测方法的平均效率高122倍,基于LR方法的平均效率比传统的模型检测方法的平均效率高113倍,基于DT方法的平均效率比传统的模型检测方法的平均效率高81倍,基于SVM方法的平均效率比传统的模型检测方法的平均效率高91倍。这些结果表明,使用RF机器学习预测CTL模型检测结果,可以达到良好的准确预测效果。

关键词: 机器学习 模型检测 计算树逻辑 Kripke结构

For information in English, please click here

Predicting the Results of CTL Model Checking using Multiple Machine Learning Algorithms

ZHU Weijun 1   

朱维军(1976-),男,副教授、硕导,主要研究方向:形式化方法、人工智能

FAN Yongwen 1    BAN Shaohuan 1   
  • 1、School of Information Engineering,Zhengzhou University,Zhengzhou 450001,China

Abstract:Computational Tree Logic (CTL) model checking has been applied to many fields. However, the state explosion problem restricts the further applications of CTL model checking. A lot of approaches have been presented to address these problems. However, the essential issue has not been resolved due to the limitation of the inherent complexity of the problem. We used the BT algorithm to predict CTL model detection and achieved a result that BT-based approach has a significant increase in efficiency with a slight decrease in accuracy,in our preliminary work. Can other machine learning algorithms obtain more accurate and faster result when used in CTL model detection prediction results? To this end, we use another four machine learning methods in this paper. First, for a number of Kripke structures and CTL formulas, a data set A containing model checking results are obtained, using the existing CTL model checking algorithm. Second, the CTL model checking problem can be induced to a binary classification problem of machine learning. In other words, some records in A form a training set for the Random Forest (RF) algorithm, Logistic Regression (LR) one, Decision Tree (DT) one and Support Vector Machine (SVM) one, and the corresponding model is obtained. On the basis of it, a ML model M is obtained to predict the results of CTL model checking. The experiments show that the RF-based one has the average accuracy of 95.6%, the LR-based one has the average accuracy of 91.1%, the DT-based one has the average accuracy of 95.1%, and the SVM-based one has the average accuracy of 94.9%. Furthermore, the average efficiency of the RF-based approach is 112 times higher than that of the existing one, the average efficiency of the LR-based approach is 113 times higher than that of the existing one, the average efficiency of the DT-based approach is 81 times higher than that of the existing one, and the average efficiency of the SVM-based approach is 91 times higher than that of the existing one. These results indicate that RF-based approach have a good prediction effect in determining the results of CTL model checking.

Keywords: Machine Learning Model Checking Computational Tree Logic Kripke Structure

Click to fold

点击收起

论文图表:

引用

导出参考文献

.txt .ris .doc
朱维军,樊永文,班绍桓. 使用多种机器学习算法预测CTL模型检测[EB/OL]. 北京:中国科技论文在线 [2019-01-11]. http://www.paper.edu.cn/releasepaper/content/201901-71.

No.****

同行评议

未申请同行评议

评论

全部评论

0/1000

勘误表

使用多种机器学习算法预测CTL模型检测