情報処理学会 第74回全国大会講演要旨

　プログラム合成において、各モジュールごとに持たせた入出力条件のチェックを
行う際、合成されたプログラムのペトリネットモデルに対し、可到達性の判定を
行うことで、合成されたプログラムの可動性の判定ができないか検討を行う。
　ペトリネットの可到達性の判定には、状態方程式の解の存在を証明する手法を
用いるが、これだけでは解の存在の証明にしかならず、ペトリネットにおける
解である非負整数解の存在の証明にはならない。このため、T-インバリアント
を求めるための手法であるFourie-Motzkin法を改良し、直接、発火回数ベクトル
を数学的に求めることで解を導出し、ペトリネットの可到達性の判定を行う。