主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2018年第10期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
刘尧,段振华,田聪.NuTL2PFG:νTL公式的可满足性检查.软件学报,2017,28(4):898-906
NuTL2PFG:νTL公式的可满足性检查
NuTL2PFG: Checking Satisfiability of νTL Formulas
投稿时间:2015-12-25  修订日期:2016-02-24
DOI:10.13328/j.cnki.jos.005057
中文关键词:  线性μ演算  当前-未来范式  当前-未来范式图  可满足性
英文关键词:linear time μ-calculus  present future form  present future form graph  satisfiability
基金项目:国家自然科学基金(61322202,61133001,61420106004,91418201)
作者单位E-mail
刘尧 西安电子科技大学 计算理论与技术研究所, 陕西 西安 710071
综合业务网理论及关键技术国家重点实验室(西安电子科技大学), 陕西 西安 710071 
 
段振华 西安电子科技大学 计算理论与技术研究所, 陕西 西安 710071
综合业务网理论及关键技术国家重点实验室(西安电子科技大学), 陕西 西安 710071 
zhhduan@mail.xidian.edu.cn 
田聪 西安电子科技大学 计算理论与技术研究所, 陕西 西安 710071
综合业务网理论及关键技术国家重点实验室(西安电子科技大学), 陕西 西安 710071 
ctian@mail.xidian.edu.cn 
摘要点击次数: 1416
全文下载次数: 771
中文摘要:
      线性μ演算(linear time μ-calculus,简称νTL)语法简单,表达能力强,可用于验证并发程序的多种性质.然而,不动点操作符的嵌套使其判定问题难以有效解决.针对这一问题,开发了工具NuTL2PFG,用以判定νTL公式的可满足性.利用νTL公式的当前-未来范式(present future form,简称PF式),该工具能够为一个给定公式构造其当前-未来范式图(present future form graph,简称PFG),用以描述满足该公式的模型.通过在所得PFG中寻找一条ν-路径,即,不涉及最小不动点公式的无穷展开的路径,该工具便可判断出给定公式的可满足性.实验结果表明,NuTL2PFG的执行效率优于已有工具.
英文摘要:
      Linear time μ-calculus (νTL) is a formalism which has a strong expressive power with a succinct syntax. It is useful for specifying and verifying various properties of concurrent programs. However, the nesting of fix point operators makes its decision problem difficult to solve. To tackle the issue, a tool called NuTL2PFG for checking the satisfiability of νTL formulas is developed in this paper. Based on present future form (PF form) of νTL formulas, the tool is able to construct the present future form graph (PFG) for a given formula to specify the models that satisfy the formula. Further, the tool checks the satisfiability of a given formula by searching for a ν-path in its PFG free of infinite unfoldings of least fixpoints. Experimental results show that NuTL2PFG is more efficient than the existing tools.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利