An Extension of Pushdown System and Its Model Checking Method

IPSJ

Bibliographic Information

Other Title
  • プッシュダウンシステムの拡張およびそのモデル検査法

Search this article

Description

現在，無限の状態空間を持つ遷移システムに対するモデル検査法の研究がさかんに行われており，特にプッシュダウンシステムやペトリネットに対するモデル検査において良い結果が得られている．本発表では，プッシュダウンシステムを拡張した遷移システムを項書き換え系の部分クラスとして定義し，そのLTL （線形時相論理）によるモデル検査が決定可能となることを示す．プッシュダウンシステムの項書き換え系による定式化は，一般に文字列で表現されるスタック構造の木構造への拡張を意味し，この拡張によってより豊かなデータ構造を持った遷移システムの自動検証が可能になることが期待される．

Recently, in the field of model checking, many researches for infinite systems have been done. Particularly for pushdown systems and petri nets, there are good decidablity results on model checking. In this presentation, we define a class of transition systems which is an extension of pushdown systems as a subclass of TRS (term rewriting systems) and show that LTL (linear temporal logic) model checking problem for the class is decidable. Formulating pushdown systems as a subclass of TRS, we can extend the structure of stacks to tree structure. By this extension, it is expected that transition systems with richer data structure become verifiable.

Journal

Keywords

Details 詳細情報について

Report a problem

Back to top