• 検索結果がありません。

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

N/A
N/A
Protected

Academic year: 2021

シェア "プッシュダウンシステムの拡張およびそのモデル検査法"

Copied!
1
0
0

読み込み中.... (全文を見る)

全文

(1)Vol. 44. No. SIG 13(PRO 18). Oct. 2003. 情報処理学会論文誌:プログラミング. 発表概要. プッシュダウンシステムの拡張およびそのモデル検査法 新. 田. 直. 也†. 関. 浩. 之†. 現在,無限の状態空間を持つ遷移システムに対するモデル検査法の研究がさかんに行われており, 特にプッシュダウンシステムやペトリネットに対するモデル検査において良い結果が得られている. 本発表では,プッシュダウンシステムを拡張した遷移システムを項書き換え系の部分クラスとして定 義し,その LTL( 線形時相論理)によるモデル検査が決定可能となることを示す.プッシュダウンシ ステムの項書き換え系による定式化は,一般に文字列で表現されるスタック構造の木構造への拡張を 意味し,この拡張によってより豊かなデータ構造を持った遷移システムの自動検証が可能になること が期待される.. An Extension of Pushdown System and Its Model Checking Method Naoya Nitta† and Hiroyuki Seki† 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.. ( 平成 15 年 1 月 23 日発表). † 奈良先端科学技術大学院大学情報科学研究科 Graduate School of Information Science, Nara Institute of Science and Technology. 111.

(2)

参照

関連したドキュメント

We provide an accurate upper bound of the maximum number of limit cycles that this class of systems can have bifurcating from the periodic orbits of the linear center ˙ x = y, y ˙ =

, 6, then L(7) 6= 0; the origin is a fine focus of maximum order seven, at most seven small amplitude limit cycles can be bifurcated from the origin.. Sufficient

Keywords and phrases: super-Brownian motion, interacting branching particle system, collision local time, competing species, measure-valued diffusion.. AMS Subject

Using the results of Sec- tions 2, 3, we establish conditions of exponential stability of the zero solution to (1.1) and obtain estimates characterizing exponential decay of

We study in Section 3 the generalized Cauchy problem of the Dunkl linear symmetric systems, and we prove the principle of finite speed of propagation of these systems.. In the

The advection-diffusion equation approximation to the dispersion in the pipe has generated a considera- bly more ill-posed inverse problem than the corre- sponding

A variety of methods have been introduced for the synchronization of chaotic systems which include complete synchronization, generalized synchronization, phase synchronization,

Our objective in Section 4 is to extend, several results on curvature of a contractive tuple by Popescu [19, 20], for completely contractive, covari- ant representations of