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

概要

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