SCCS動作式に対するunfold変換によるLTSモデルの効率的な構成法 （並列・分散）

• Item type: SIG Technical Reports(1)
• 公開日: 1997-01-23
• タイトル: SCCS動作式に対するunfold変換によるLTSモデルの効率的な構成法 （並列・分散）
• タイトル / 言語: en
• タイトル: A Memory - efficient Contruction of Labeled Transition Models for SCCS Expressions by Unfold Trans formation
• 言語: jpn
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 名古屋大学工学部情報工学科
• 著者所属: 名古屋大学工学部情報工学科
• 著者所属: 名古屋大学工学部情報工学科
• 著者所属: 名古屋大学工学部情報工学科
• 著者所属(英): en
• 著者所属(英): Department of Information Engineering, Nagoya University
• 著者所属(英): en
• 著者所属(英): Department of Information Engineering, Nagoya University
• 著者所属(英): en
• 著者所属(英): Department of Information Engineering, Nagoya University
• 著者所属(英): en
• 著者所属(英): Department of Information Engineering, Nagoya University
• 著者名: 鈴木, 晃; 結縁祥治; 坂部, 俊樹; 稲垣, 康善
• 著者名(英): Akira, Suzuki; Shoji, Yuen; Toshiki, Sakabe; Yasuyoshi, Inagaki
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 本稿では、SCCS動作式に対するLTSモデル（ラベル付き遷移系モデル）を効率的に構成する方法を提案する。SCCS動作式によって並行システムを仕様記述するとき、並列合成演算子と遅延演算子の組み合わせによって、LTSモデルの非決定性が大きくなり状態遷移数が増加する。しかし、実際的な仕様記述は部分仕様の組み合わせとして(_1|…|P_)＼Lのような形をとり、このような仕様記述では部分仕様乃の並列合成による非決定性は制限演算＼Lによって限定されることが多い。このためまずP_1|…|P_nのLTSモデルを構成してから全体のLTSモデルを構成すると、中間結果として求めた多くの遷移先の状態が＼Lにより捨てられるため無駄になる。本稿では、この点に注目し、SCCS動作式をあらかじめ構文的に変換してLTSモデルを構成する際の中間結果を小さくする方法を与え、この変換がSCCSの強等価性に対して健全であることを示す。さらに実験により、本方法がSCCSにおける検証に対して有効であることを示す。
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: In this paper, we present a memory-efficient construction of LTS models (labeled transition system models) for SCCS expressions. In a construction of an LTS model, the combination of parallel compositions (|) and delay operators ($) will increase the number of states and state transitions. For this reason, a large amount of memory may be required to check if an SCCS specification satisfies some property. However, a typical SCCS specification is in the form of (P_1|…|P_n)＼L where ＼L internalizes the communications of L between P_i's. In this type of specification, it is often the case that the specification is deterministic externally although it is very nondeterministic internally because the restriction operation ＼L eliminates the internal nondeterminism that may cause the memory explosion by intermediate results. Based on this observation, we will give a transformation technique up to the strong equivalence of SCCS so that intermediate results may not be too large in constructing LTS models, where the SCCS expression is syntactically transformed beforehand. The transformation is given as the combination of process definition unfolding, expansion by the expansion theorem, and transformation by the strong equivalence. We show the impact of our transformation technique by presenting an example using Concurrency Workbench.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN10485570
• 書誌情報: 情報処理学会研究報告プログラミング（PRO）; 巻 1997, 号 9(1996-PRO-011), p. 93-100, 発行日 1997-01-23
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会