氏名: 木川泰夫 (l0571623)
論文題目: CCS動作式に対するLTSモデルの効率的構成法
論文概要
本論文では、並行システムの形式的体系であるMilnerのCCSの操作モデルであるラベル
付遷移系（LTS）の構成に必要なメモリ使用量を減らすことを目的とする。LTSを構成す
る際、状態遷移の非決定性によりすべての経路を探索するため、多くのメモリが必要と
なる。CCS動作式の基底となる部分式から帰納的にLTSを構成する場合、制限演算子を適
用すると一旦構成された遷移を除外するので、一時的に状態数が増大する。この問題に
対して、以下の２つの方法でメモリ使用量を改善できることを示す。
（１）動作式をあらかじめ等価変換する方法
（２）最外評価によってLTSを構成する方法
目次に戻る