計算機言語論第3回

XENO @xenophobia__

イントロ #計算機言語論

wistery_k @wistery_k

モデル検査とは: (モデル*仕様) -> bool #計算機言語論

wistery_k @wistery_k

自動販売機の例 #計算機言語論

wistery_k @wistery_k

モデルの例: (オートマトンの図), 仕様の例: 有限回の操作の後にstart状態に戻る #計算機言語論

wistery_k @wistery_k

モデルも仕様も無限語で表すことができる,よって 「モデルを表す無限語⊆仕様を表す無限語」になってるか判定すればいい #計算機言語論

XENO @xenophobia__

システムが仕様を満たすとは、L(System)⊆L(Spec)が成り立つということ #計算機言語論

XENO @xenophobia__

お？これhso先生のレポート課題じゃね？ #計算機言語論

XENO @xenophobia__

Peterson Algorithm #計算機言語論

XENO @xenophobia__

覚えてないし、使った記憶もない #計算機言語論

あかざき @ultraredrays

プロセス共有の安全性をモデル検査で証明する #計算機言語論

あかざき @ultraredrays

モデル検査の種類 #計算機言語論

あかざき @ultraredrays

automataとω-rational、様相論理、monadic-2nd-orderの表現力が同等で、そのモデル検査が有限状態モデル検査 #計算機言語論

NLT @nltkawa

wikipedia「チョムスキー階層での正規言語の位置によれば、正規言語は文脈自由言語に含まれる。その逆は真ではない。」　#計算機言語論

XENO @xenophobia__

高階再帰スキームの例 #計算機言語論