Method of Constructing Two-Way Alternating Automata for PSL and Translation to Nondeterministic Automata
DOI:
Author:
Affiliation:

Clc Number:

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    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.

    Reference
    Related
    Cited by
Get Citation

虞蕾,陈火旺. PSL构造双向交换自动机及非确定自动机的方法.软件学报,2010,21(1):34-46

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:January 31,2008
  • Revised:August 11,2008
  • Adopted:
  • Online:
  • Published:
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063