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

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-01 发布日期:2014-05-30
通讯作者: 林运国
作者简介:林运国(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-01 Published:2014-05-30
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]. 《计算机应用》唯一官方网站, 2021, 41(11): 3394-3401.
[2]	祁祥洲邢红杰. 基于中心核对齐的多核单类支持向量机[J]. 计算机应用, 0, (): 0-0.
[3]	陈浩杰，范江亭，刘勇. 分布式强化学习解决动态旅行商问题[J]. 计算机应用, 0, (): 0-0.
[4]	郭一阳于炯杜旭升杨少智曹铭. 基于自编码器与集成学习的离群点检测算法[J]. 计算机应用, 0, (): 0-0.
[5]	李卓, 宋子晖, 沈鑫, 陈昕. 边缘计算支持下的移动群智感知本地差分隐私保护机制[J]. 计算机应用, 2021, 41(9): 2678-2686.
[6]	王周恺, 张炯, 马维纲, 王怀军. 面向高速列车监测数据的并行解压缩算法[J]. 计算机应用, 2021, 41(9): 2586-2593.
[7]	张妮韩萌王乐李小娟程浩东. 基于正负效用划分的高效用模式挖掘方法综述[J]. 计算机应用, 0, (): 0-0.
[8]	武鹏, 吴尽昭. 基于线性误差断言的推理方法[J]. 计算机应用, 2021, 41(8): 2199-2204.
[9]	孙蕊, 韩萌, 张春砚, 申明尧, 杜诗语. 含负项top-k高效用项集挖掘算法[J]. 计算机应用, 2021, 41(8): 2386-2395.
[10]	王梓森, 梁英, 刘政君, 谢小杰, 张伟, 史红周. 科研项目同行评议专家学术专长匹配方法[J]. 计算机应用, 2021, 41(8): 2418-2426.
[11]	赵全, 汤小春, 朱紫钰, 毛安琪, 李战怀. 大规模短时间任务的低延迟集群调度框架[J]. 计算机应用, 2021, 41(8): 2396-2405.
[12]	康军, 黄山, 段宗涛, 李宜修. 时空轨迹序列模式挖掘方法综述[J]. 计算机应用, 2021, 41(8): 2379-2385.
[13]	陈静, 毛莺池, 陈豪, 王龙宝, 王子成. 基于改进单点多盒检测器的大坝缺陷目标检测方法[J]. 计算机应用, 2021, 41(8): 2366-2372.
[14]	马华, 陈跃鹏, 唐文胜, 娄小平, 黄卓轩. 面向工作者能力评估的众包任务分配方法的研究进展综述[J]. 计算机应用, 2021, 41(8): 2232-2241.
[15]	李莉吴怡杨祉坤陈云鹏. 基于分区型区块链医疗电子病历共享方案[J]. , 0, (): 0-0.

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

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

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics