系统仿真学报
繫統倣真學報
계통방진학보
JOURNAL OF SYSTEM SIMULATION
2003年
z1期
6-10
,共5页
线性时序逻辑%Petri网%B u chi自动机%同步积%模型检测
線性時序邏輯%Petri網%B u chi自動機%同步積%模型檢測
선성시서라집%Petri망%B u chi자동궤%동보적%모형검측
Petri网是一种重要的数学工具,它能有效地对并发系统进行描述和建模.线性时态逻辑LTL则是描述和验证并发系统特性的一种重要的形式化工具,它能方便准确地描述并发系统的重要性质,如安全性和活性.文章深入描述了线性时态逻辑、Bu chi自动机、Petri网和同步积之间的内在联系,并探讨了基于线性时态逻辑的Petri网模型检测策略.与其它方法比较,这种模型检测的策略结合了线性时态逻辑和Petri网模型的不同优点,增强了Petri网的模型分析和验证能力.最后,通过对一个并发系统形式化的模型检测分析,验证了相应的结论.
Petri網是一種重要的數學工具,它能有效地對併髮繫統進行描述和建模.線性時態邏輯LTL則是描述和驗證併髮繫統特性的一種重要的形式化工具,它能方便準確地描述併髮繫統的重要性質,如安全性和活性.文章深入描述瞭線性時態邏輯、Bu chi自動機、Petri網和同步積之間的內在聯繫,併探討瞭基于線性時態邏輯的Petri網模型檢測策略.與其它方法比較,這種模型檢測的策略結閤瞭線性時態邏輯和Petri網模型的不同優點,增彊瞭Petri網的模型分析和驗證能力.最後,通過對一箇併髮繫統形式化的模型檢測分析,驗證瞭相應的結論.
Petri망시일충중요적수학공구,타능유효지대병발계통진행묘술화건모.선성시태라집LTL칙시묘술화험증병발계통특성적일충중요적형식화공구,타능방편준학지묘술병발계통적중요성질,여안전성화활성.문장심입묘술료선성시태라집、Bu chi자동궤、Petri망화동보적지간적내재련계,병탐토료기우선성시태라집적Petri망모형검측책략.여기타방법비교,저충모형검측적책략결합료선성시태라집화Petri망모형적불동우점,증강료Petri망적모형분석화험증능력.최후,통과대일개병발계통형식화적모형검측분석,험증료상응적결론.
