加权迁移系统线性时间属性及其安全性检测

doi:10.11772/j.issn.1001-9081.2014.05.1413

计算机应用 ›› 2014, Vol. 34 ›› Issue (5): 1413-1417.DOI: 10.11772/j.issn.1001-9081.2014.05.1413

加权迁移系统线性时间属性及其安全性检测

林运国

福建农林大学计算机与信息学院，福州 350002

收稿日期:2013-10-15 修回日期:2013-12-26 发布日期:2014-05-30 出版日期:2014-05-01
通讯作者: 林运国
作者简介:林运国(1979-)，男，福建福清人，讲师，博士研究生，主要研究方向：模型检测、量子计算。

Linear time properties of weighted transition system and checking of safety property

LIN Yunguo

School of Computer and Information, Fujian Agriculture and Forestry University, Fuzhou Fujian 350002, China

Received:2013-10-15 Revised:2013-12-26 Online:2014-05-30 Published:2014-05-01
Contact: LIN Yunguo

摘要/Abstract

摘要：

针对加权迁移系统，提出了线性时间属性及其安全性检测。首先定义了半环K上的加权迁移系统，提出了加权线性时间属性概念，并根据权重函数确定加权线性时间属性的上确界、下确界和闭包; 接着给出了几种常见的加权线性时间属性并且讨论了它们的关系; 然后重点研究了加权安全性，通过加权自动机和闭包给出了加权正则安全性; 最后基于加权有穷自动机，建立了加权正则安全性的检测方法。检测过程结合半环和形式幂级数，构造了加权迁移系统和加权有穷自动机的乘积系统，将加权安全性检测问题转化为验证乘积系统的不变性，给出了加权正则安全性检测的算法和复杂度。实例结果表明，所提的方法能够对加权迁移系统的安全性进行检测。

Abstract:

With regard to the weighted transition system, the linear time properties were proposed. Firstly, the weighted transition system above semiring K was defined, the concepts of the weighted linear time properties were given, the upper, the lower and the closure of weighted linear time properties were determined by the weighted function; secondly some familiar weighted linear time properties and their relationships were discussed; thirdly the weighted safety property was mainly studied, the weighted regular safety property was defined through weighted automaton and closure of weighted regular safety property; finally, the checking method of the weighted regular safety was built based on weighted finite automaton. The checking was follows. Together with semiring and formal series, the product system was built over weighted transition and weighted finite automaton, the model checking about weighted safety property of weighted transition was transferred to verify the invariance of the product system, the algorithm and complexity were given. Finally, an example shows the model checking of weighted regular safety property is reasonable and efficient. The example result shows the proposed method can verify the safety of the weighted system.

中图分类号:

TP311

林运国. 加权迁移系统线性时间属性及其安全性检测[J]. 计算机应用, 2014, 34(5): 1413-1417.

LIN Yunguo. Linear time properties of weighted transition system and checking of safety property[J]. Journal of Computer Applications, 2014, 34(5): 1413-1417.

参考文献

［1］BAIER C, KATOEN J P. Principles of model checking ［M］. Cambridge: MIT Press, 2008:745-747.
［2］SHOHAM S, GRUMBERG O. Multi-valued model checking games ［J］. Journal of Computer and System Sciences, 2012,78(2):414-429.
［3］LI Y, LI L. Model checking of linear-time properties based on possibility measure ［J］. IEEE Transactions on Fuzzy Systems, 2013,21(5):842-854.
［4］GROSU R, SMOLKA S A. Quantitative model checking ［C］// ISoLA '04: Proceedings of the 1st International Symposium on Leveraging Applications of Formal Methods. Berlin: Springer-Verlag, 2004: 165-174.
［5］FAELLA M, LEGAY A, STOELINGA M. Model checking quantitative linear time logic ［J］. Electronic Notes in Theoretical Computer Science, 2008,220(3):61-77.
［6］BRIHAYE T, BRUYRE V, RASKIN J F. Model-checking for weighted timed automata ［EB/OL］. ［2013-05-11］. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.83.8436&rep=rep1&type=pdf.
［7］BOUYER P. Weighted timed automata: model-checking and games ［EB/OL］. ［2013-05-16］. http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bouyer-mfps06.pdf.
［8］BUCHHOLZ P, KEMPER P. Model checking for a class of weighted automata ［J］. Discrete Event Dynamic Systems, 2010,20(1):103-137.
［9］DROSTE M, KUICH W, VOGLER H. Handbook of weighted automata ［M］. Berlin: Springer, 2009:122-127.
［10］GERLA B. Many valued logic and semirings ［EB/OL］. ［2013-05-18］. http://www.dmi.unisa.it/people/bgerla/www/papers/bgerla-ercim.pdf.
［11］JIANG Z, JIANG S. Formal language and automata theory ［M］. 2nd ed. Beijing: Tsinghua University Press, 2007:89-91.(蒋宗礼,姜守旭.形式语言与自动机理论［M］.2版.北京:清华大学出版社,2007:89-91.)
［12］DROSTE M, GASTIN P. Weighted automata and weighted logics ［J］. Theoretical Computer Science, 2007,380(1/2):69-86.
［13］DROSTE M, MEINECKE I, EELJA B, et al. A cascade decomposition of weighted finite transition systems ［C］// DLT '11: Proceedings of the 15th International Conference on Developments in Language Theory. Berlin: Springer-Verlag, 2011:472-473.

[1]	高威刘丽华和斌涛邓方安. 区块链共识机制与改进算法研究进展[J]. 《计算机应用》唯一官方网站, 0, (): 0-0.
[2]	翟社平朱鹏举杨锐刘佳一腾. 基于区块链的物联网身份管理系统[J]. 《计算机应用》唯一官方网站, 0, (): 0-0.
[3]	蔡锦辉, 尹中旭, 宗国笑, 李俊儒. 面向嵌套分支突破的推断与污点分析融合的方法[J]. 《计算机应用》唯一官方网站, 2024, 44(12): 3823-3830.
[4]	李博, 黄建强, 黄东强, 王晓英. 基于异构平台的稀疏矩阵向量乘自适应计算优化[J]. 《计算机应用》唯一官方网站, 2024, 44(12): 3867-3875.
[5]	陈姿芊, 牛科迪, 姚中原, 斯雪明. 适用于物联网的区块链轻量化技术综述[J]. 《计算机应用》唯一官方网站, 2024, 44(12): 3688-3698.
[6]	高婷婷, 姚中原, 贾淼, 斯雪明. 链上链下一致性保护技术综述[J]. 《计算机应用》唯一官方网站, 2024, 44(12): 3658-3668.
[7]	贾淼, 姚中原, 祝卫华, 高婷婷, 斯雪明, 邓翔. 零知识证明赋能区块链的进展与展望[J]. 《计算机应用》唯一官方网站, 2024, 44(12): 3669-3677.
[8]	牛科迪, 李敏, 姚中原, 斯雪明. 面向物联网的区块链共识算法综述[J]. 《计算机应用》唯一官方网站, 2024, 44(12): 3678-3687.
[9]	杨巍白璐宁俊义董建军单春海信俊昌. 异构环境感知的幂律图流划分方法[J]. 《计算机应用》唯一官方网站, 0, (): 0-0.
[10]	梁辰王奕森魏强杜江. 基于Transformer-GCN的源代码漏洞检测方法[J]. 《计算机应用》唯一官方网站, 0, (): 0-0.
[11]	吴海峰陶丽青程玉胜. 集成特征注意力和残差连接的偏标签回归算法[J]. 《计算机应用》唯一官方网站, 0, (): 0-0.
[12]	秦学程刘春颜李宝赵蕴龙. 面向工业场景的云边协同数据存储与检索架构[J]. 《计算机应用》唯一官方网站, 0, (): 0-0.
[13]	涂进兴, 李志雄, 黄建强. 基于GPU对角稀疏矩阵向量乘法的动态划分算法[J]. 《计算机应用》唯一官方网站, 2024, 44(11): 3521-3529.
[14]	曾蠡, 杨婧如, 黄罡, 景翔, 罗超然. 超图应用方法综述：问题、进展与挑战[J]. 《计算机应用》唯一官方网站, 2024, 44(11): 3315-3326.
[15]	崔双双王宏志朱加昊吴昊. 面向低能耗高性能的分类器两阶段数据选择方法[J]. 《计算机应用》唯一官方网站, 0, (): 0-0.

加权迁移系统线性时间属性及其安全性检测

Linear time properties of weighted transition system and checking of safety property

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics