计算机应用研究
計算機應用研究
계산궤응용연구
APPLICATION RESEARCH OF COMPUTERS
2010年
5期
1788-1790
,共3页
行为时序逻辑%公平性%并发系统%系统描述%蕴涵关系
行為時序邏輯%公平性%併髮繫統%繫統描述%蘊涵關繫
행위시서라집%공평성%병발계통%계통묘술%온함관계
基于行为时序逻辑(TLA)的并发系统描述,就是对系统的初始状态、系统行为和行为的公平性进行规约和描述,但TLA中的公平性具有局限性,无法准确地描述某些系统的行为,从而限制了TLA的描述能力.通过研究TLA中公平性的推导过程,分析公平性的概念与定义方法,并以实际例子说明它的局限性.在此基础上,提出以加入两级新的公平性方式对其进行完善.最后,证明了新公平性等级之间的蕴涵关系.完善后的公平性具有更强的描述能力,能够对系统进行更完整的描述与规约.
基于行為時序邏輯(TLA)的併髮繫統描述,就是對繫統的初始狀態、繫統行為和行為的公平性進行規約和描述,但TLA中的公平性具有跼限性,無法準確地描述某些繫統的行為,從而限製瞭TLA的描述能力.通過研究TLA中公平性的推導過程,分析公平性的概唸與定義方法,併以實際例子說明它的跼限性.在此基礎上,提齣以加入兩級新的公平性方式對其進行完善.最後,證明瞭新公平性等級之間的蘊涵關繫.完善後的公平性具有更彊的描述能力,能夠對繫統進行更完整的描述與規約.
기우행위시서라집(TLA)적병발계통묘술,취시대계통적초시상태、계통행위화행위적공평성진행규약화묘술,단TLA중적공평성구유국한성,무법준학지묘술모사계통적행위,종이한제료TLA적묘술능력.통과연구TLA중공평성적추도과정,분석공평성적개념여정의방법,병이실제례자설명타적국한성.재차기출상,제출이가입량급신적공평성방식대기진행완선.최후,증명료신공평성등급지간적온함관계.완선후적공평성구유경강적묘술능력,능구대계통진행경완정적묘술여규약.
