π計算に対する時間拡張と合同的性質

摘要

本論文では文献に基づくπ計算の時間拡張において，等価関係と擬順序関係が合同的性質をもつ十分条件を示す．時間経過が含まれるため，等価関係である時間拡張された双模倣関係は一般的には合同性を満たさない．しかし，チャネル名を束縛する入力プレフィックス以外のコンテクストに対しては合同であることを示す．ハードリアルタイム性をモデル化するために，遅延時間順関係と呼ぶ順序関係を定義する．遅延時間順関係は同じ入出力動作を一方のプロセスが他方より早いタイミングで実行できることを表す．遅延時間順関係は入力プレフィックス以外のコンテクストに対し合同であるが，並行合成されるプロセスは時間経過によって変換しないプロセスに制限される．ネットワーク構成が動的に変化するストリーミングシステムを用いて時間付きπ計算による記述と遅延時間順関係の例を示す．