计算机应用
計算機應用
계산궤응용
COMPUTER APPLICATION
2014年
5期
1413-1417
,共5页
迁移系统%线性时间属性%模型检测%安全性%半环
遷移繫統%線性時間屬性%模型檢測%安全性%半環
천이계통%선성시간속성%모형검측%안전성%반배
transition system%linear time property%model checking%safety property%semiring
针对加权迁移系统,提出了线性时间属性及其安全性检测.首先定义了半环K上的加权迁移系统,提出了加权线性时间属性概念,并根据权重函数确定加权线性时间属性的上确界、下确界和闭包;接着给出了几种常见的加权线性时间属性并且讨论了它们的关系;然后重点研究了加权安全性,通过加权自动机和闭包给出了加权正则安全性;最后基于加权有穷自动机,建立了加权正则安全性的检测方法.检测过程结合半环和形式幂级数,构造了加权迁移系统和加权有穷自动机的乘积系统,将加权安全性检测问题转化为验证乘积系统的不变性,给出了加权正则安全性检测的算法和复杂度.实例结果表明,所提的方法能够对加权迁移系统的安全性进行检测.
針對加權遷移繫統,提齣瞭線性時間屬性及其安全性檢測.首先定義瞭半環K上的加權遷移繫統,提齣瞭加權線性時間屬性概唸,併根據權重函數確定加權線性時間屬性的上確界、下確界和閉包;接著給齣瞭幾種常見的加權線性時間屬性併且討論瞭它們的關繫;然後重點研究瞭加權安全性,通過加權自動機和閉包給齣瞭加權正則安全性;最後基于加權有窮自動機,建立瞭加權正則安全性的檢測方法.檢測過程結閤半環和形式冪級數,構造瞭加權遷移繫統和加權有窮自動機的乘積繫統,將加權安全性檢測問題轉化為驗證乘積繫統的不變性,給齣瞭加權正則安全性檢測的算法和複雜度.實例結果錶明,所提的方法能夠對加權遷移繫統的安全性進行檢測.
침대가권천이계통,제출료선성시간속성급기안전성검측.수선정의료반배K상적가권천이계통,제출료가권선성시간속성개념,병근거권중함수학정가권선성시간속성적상학계、하학계화폐포;접착급출료궤충상견적가권선성시간속성병차토론료타문적관계;연후중점연구료가권안전성,통과가권자동궤화폐포급출료가권정칙안전성;최후기우가권유궁자동궤,건립료가권정칙안전성적검측방법.검측과정결합반배화형식멱급수,구조료가권천이계통화가권유궁자동궤적승적계통,장가권안전성검측문제전화위험증승적계통적불변성,급출료가권정칙안전성검측적산법화복잡도.실례결과표명,소제적방법능구대가권천이계통적안전성진행검측.
