CAJ | 학술논문

PSL(property specification language)是一种用于描述并行系统的属性规约语言,包括线性时序逻辑FL(foundation language)和分支时序逻辑OBE(optional branching extension)两部分.由于OBE就是CTL(computation tree logic),并且具有时钟声明的公式很容易改写成非时钟公式,因此重点研究了非时钟FL逻辑.为便于进行模型检验,每个FL公式必须转化成为一种可验证形式,通常是自动机(非确定自动机).构造非确定自动机的过程主要是通过中间构建交换自动机来实现.详细给出了由非时钟FL构造双向交换自动机的构造规则.构造规则的核心逻辑不仅仅局限于是在LTL(linear temporal logic)基础上的正规表达式,而且全面而充分地考虑了各种FL操作算子的可能性.并且给出了将双向交换自动机转化为非确定自动机的一种方法.最后,编写了将PSL转化为上述自动机的实现工具.FL双向交换自动机的构造规则计算复杂度仅是FL公式长度的线性表达式,验证了构造规则的正确性.在此基础上,证明了双向交换自动机与其转化的等价的非确定自动机接受的语言相同.上述工作对解决复杂并行系统建模和模型验证问题具有重要的理论意义和应用价值.
PSL(property specification language)시일충용우묘술병행계통적속성규약어언,포괄선성시서라집FL(foundation language)화분지시서라집OBE(optional branching extension)량부분.유우OBE취시CTL(computation tree logic),병차구유시종성명적공식흔용역개사성비시종공식,인차중점연구료비시종FL라집.위편우진행모형검험,매개FL공식필수전화성위일충가험증형식,통상시자동궤(비학정자동궤).구조비학정자동궤적과정주요시통과중간구건교환자동궤래실현.상세급출료유비시종FL구조쌍향교환자동궤적구조규칙.구조규칙적핵심라집불부부국한우시재LTL(linear temporal logic)기출상적정규표체식,이차전면이충분지고필료각충FL조작산자적가능성.병차급출료장쌍향교환자동궤전화위비학정자동궤적일충방법.최후,편사료장PSL전화위상술자동궤적실현공구.FL쌍향교환자동궤적구조규칙계산복잡도부시FL공식장도적선성표체식,험증료구조규칙적정학성.재차기출상,증명료쌍향교환자동궤여기전화적등개적비학정자동궤접수적어언상동.상술공작대해결복잡병행계통건모화모형험증문제구유중요적이론의의화응용개치.
PSL (property specification language) is a property specification language to describe parallel systems and can be divided into two parts, FL (foundation language) and OBE (optional branching extension). Since OBE is essentially the temporal logic CTL (computation tree logic), and PSL formulas with clock statements can be easily rewritten to unclocked formulas, this paper plays an emphasis on the unclocked FL logic. In order to be model-checked, each FL formula needs to be translated into a verifiable form, usually as an automaton (nondeterministic automaton). The translation into nondeterministic automata can be realized mainly by the construction of alternating automata. The translation rules for the two-way alternating automata from unclocked FL logic are explained in detail in this paper. The core logic of the construction rules is not only limited to an extension of LTL (linear temporal logic) with regular expressions, but considers overall FL operators adequately. A translation method from two-way alternating automata to nondeterministic automata is also provided. Finally, a translation tool from PSL formulas to the above two automata has been written. The complexity of the construction rules for the two-way alternating automata grows linearly with the length of the FL formulas, and at the same time, the correctness of the rules is verified. It is also proved that the two-way alternating automata and its corresponding nondeterministic automata accept the same language. The work above has important theoretical and application values for the modeling and model checking for the complex parallel systems.