SCCS動作式に対する unfold 変換によるLTSモデルの効率的な構成法

概要

論文の詳細を見る
本稿では、SCCS動作式に対するLTSモデル(ラベル月遷移系モデル)を効率的に構成する方法を提案する。SCCS動作式によって並行システムを仕様記述するとき、並列合成演算子と遅延演算子の組み合わせによって、LTSモデルの非決定性が大きくなり状態遷移数が増加する。しかし、実際的な仕様記述は部分仕様の組み合わせとして(P_1|…|P_n)＼Lのような形をとり、このような仕様記述では部分仕様P_iの並列合成による非決定性は制限演算＼Lによって限定されることが多い。このためまずP_1|…|P_nのLTSモデルを構成してから全体のLTSモデルを構成すると、中間結果として求めた多くの遷移先の状態が＼Lにより捨てられるため無駄になる。本稿では、この点に注目し、SCCS動作式をあらかじめ構文的に変換してLTSモデルを構成する際の中間結果を小さくする方法を与え、この変換がSCCSの強等価性に対して健全であることを示す。さらに実際により、本方法がSCCSにおける検証に対して有効であることを示す。
社団法人電子情報通信学会の論文
1997-01-23