否定前件を含む構造操作意味定義に対するプロセス計算コンパイラ

摘要

構造操作意味定義（Structural Operational Semantics，SOS）は並行プロセス計算の操作的意味の定義に用いられる．前件にラベル付き遷移の否定を含む遷移規則を持つSOSは表現力が増す反面，遷移規則からのラベル付き遷移関係の導出が複雑になり，プロセス言語の定義を難しくしている．本稿では，Maudeのメタレベル機構を用いて否定前件を含む遷移規則を持つSOSから遷移を機械的に導出する手法を実装し，Maude言語へ変換するコンパイラの実装を示す．本稿のコンパイラの適用例として，時間プロセス計算TPLの記述·実行をあげ，否定前件を含むSOSによって定義されるプロセス言語の実行系を自動生成できることを示す．