Isabelle
CSP

アルファベット指定による並行合成の failures

More than 3 years have passed since last update.

「アルファベット指定による並行合成の failures」という文書を書きました。

CSP のアルファベット指定による並行合成演算子 apar をインターフェイス指定による並行合成演算子 par で表し,それを使って apar の failures を計算してみます。まず式の意味が分かるように手で計算します。その後で Isabelle で確認しました。

http://www.principia-m.com/ts/0076/index-jp.html