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

doi:10.11772/j.issn.1001-9081.2014.05.1413

Journal of Computer Applications ›› 2014, Vol. 34 ›› Issue (5): 1413-1417.DOI: 10.11772/j.issn.1001-9081.2014.05.1413

Previous Articles Next Articles

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

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

林运国

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

通讯作者: 林运国
作者简介:林运国(1979-)，男，福建福清人，讲师，博士研究生，主要研究方向：模型检测、量子计算。

Abstract

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.

摘要：

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

CLC Number:

TP311

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

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

References

［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]	. Research advances in blockchain consensus mechanisms and improvement algorithms [J]. Journal of Computer Applications, 0, (): 0-0.
[2]	. Blockchain-based identity management system for internet of things [J]. Journal of Computer Applications, 0, (): 0-0.
[3]	Jinhui CAI, Zhongxu YIN, Guoxiao ZONG, Junru LI. Integrated method of inference and taint analysis for nested branch breakthrough [J]. Journal of Computer Applications, 2024, 44(12): 3823-3830.
[4]	Bo LI, Jianqiang HUANG, Dongqiang HUANG, Xiaoying WANG. Adaptive computing optimization of sparse matrix-vector multiplication based on heterogeneous platforms [J]. Journal of Computer Applications, 2024, 44(12): 3867-3875.
[5]	Ziqian CHEN, Kedi NIU, Zhongyuan YAO, Xueming SI. Review of blockchain lightweight technology applied to internet of things [J]. Journal of Computer Applications, 2024, 44(12): 3688-3698.
[6]	Tingting GAO, Zhongyuan YAO, Miao JIA, Xueming SI. Overview of on-chain and off-chain consistency protection technologies [J]. Journal of Computer Applications, 2024, 44(12): 3658-3668.
[7]	Miao JIA, Zhongyuan YAO, Weihua ZHU, Tingting GAO, Xueming SI, Xiang DENG. Progress and prospect of zero-knowledge proof enabling blockchain [J]. Journal of Computer Applications, 2024, 44(12): 3669-3677.
[8]	Kedi NIU, Min LI, Zhongyuan YAO, Xueming SI. Review of blockchain consensus algorithms for internet of things [J]. Journal of Computer Applications, 2024, 44(12): 3678-3687.
[9]	. Heterogeneous Environment Aware Streaming Graph Partitioning for Power-Law Graphs [J]. Journal of Computer Applications, 0, (): 0-0.
[10]	. Source code vulnerability detection method based on Transformer-GCN [J]. Journal of Computer Applications, 0, (): 0-0.
[11]	. Partial label regression algorithm integrating feature attention and residual connection [J]. Journal of Computer Applications, 0, (): 0-0.
[12]	. Cloud-edge collaborative data storage and retrieval architecture for industrial scenarios [J]. Journal of Computer Applications, 0, (): 0-0.
[13]	Jinxing TU, Zhixiong LI, Jianqiang HUANG. Dynamic partition algorithm for diagonal sparse matrix vector multiplication based on GPU [J]. Journal of Computer Applications, 2024, 44(11): 3521-3529.
[14]	Li ZENG, Jingru YANG, Gang HUANG, Xiang JING, Chaoran LUO. Survey on hypergraph application methods： issues， advances， and challenges [J]. Journal of Computer Applications, 2024, 44(11): 3315-3326.
[15]	. Two-stage data selection method for classifier with high performance and low energy consumption [J]. Journal of Computer Applications, 0, (): 0-0.

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

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

PDF

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Recommended Articles

Metrics