協調型言語における試験等価性と失敗等価性の関係とモデル検査への適用

摘要

本講演者は並列プログラムの作成において、各プロセス間の通信の仕様をCSPで与え、この詳細化を経て、最終的には協調型言語の枠組みによる実装を行っている。CSPでは主に失敗集合によってプロセスに意味を与えるが、試験等価性の立場からは、軌跡等価性とmay試験等価性の間に、失敗集合等価性とmust試験等価性の間に関係がある。ここではこれらの関係を協調型言語の枠組みの中で拡張して得られた開係を報告する.