１月２４日
MTSAチュートリアル： 人工知能技術を応用したソフトウェア仕様自動生成ツール
http://topse.or.jp/mtsa-tutorial/
の話を聞いてきたんだけど、話はそこまでいかなくて、
どちらかというと、状態遷移モデルの分析の話を聞いてきた感じ
まあ、とりあえず、メモメモ。
なお、もともとは全部英語のセミナーだったが、英語は全然分からないので、
まあ、適当なことメモってる（信憑性０）と思ってみてください。
■The Modal Transition systems analise
MTSAツール
・ソフトウェア工学
・ゲーム理論：このツールのベース
・自己適応システム
・AI：もゲーム理論と一緒に使う
・ロボテックス
・制御理論
MTSAでも
・状態遷移図がかける
→リアクティブシステム
システムは永遠に走っている
（コンピューターは入力がって出力する）
環境がかぎ
例：車のコントロール 周りの車に影響
そういうシステムをどう分析するかを今日やる。
・検証
・コンカレント実行
要求
・ホーアのtriplesを使う{p}C{Q}
・振る舞いは、状態・行動のシーケンス
・時相論理を使う
モデル検査：状態を満たすか、すべてチェック
モデル ｜＝ 仕様
→リアクティブシステムをモデル検査したい
↓
SYNTHESIS
・チャーチの定理
オートマトン
コントローラーSYNTHESIS
モデル||環境 |= 仕様
環境は、コントロールできない。コンカレントに
例 今 クッキングで、
||x |= NOT□オーバーヒート
となるｘにしたい
どうしたら
・チャーチの問題１９６５
：
・時相論理
・LTL → ２の指数乗の時間かかる
コンカレンシー
・マルチスレッド
シングルマシン→メモリー
複数→ネットワーク
なぜ、コンカレンシー
・並列化
→バグでやすい
→そこでモデル
モデリング
LTS VS トレース（えいえんにながくなる）
LTS VS ペトリネット
LTS VS 時相論理
・ほかのモデル
プロセス代数：CPS、CCS
I/Oオートマタ
モデリングプロセス
LTS Server ○ーリクエスト→○ーT→○
↑ ↓
ーーーーレスポンスーーー
ｔのところがServer（ｔのところがみえない）
プロセスのモデル
・記述
・グラフ表示
・トレース
FINITE STATE PROCESSES（FSP)
・LTSをコンパクトにしたもの
デットロックプロセス
FSP－選択
DRINKS=(red→Coffee→DRINKS | blue→tea→DRINK)
MONDETERMINISTIC CHOICE
おなじ状態Xから、PまたはQにわかれることがある
X→P｜X→Q
例：コイントス
表と裏の２つのループを作る→どっちを選ぶか、コイントスの前に決まってしまう
コイントスした状態をつくる→コイントスの時点では決まらない、作った状態のところで分かれる
→振舞い違う
インデックスを使って、合計とかも求められる
ガードアクション
コンカレンシー
LTL P||Q
Pが２
Qが３なら
このくみあわせを１つの状態とすると、（２X３)６とおりの状態で表現できる
ところが・・・これだけ要らないケースもある
MAKERv2 = (make-＞ready-＞used-＞MAKERv2).
USERv2 = (ready-＞use-＞used-＞USERv2).
||MAKER_USERv2 = (MAKERv2||USERv2).
は、make,ready,use,usedの４ケースだけ
Model logics（様相論理？）
・need,possibilityをしめす
・[] Need：
・＜＞ possibility
線形時相論理
＜＞＝U
□ ＝NOT＜＞NOT
Buchi
（Uはうむらると）
LTL FOR LTS
・オートマタとクリプキ構造の違い
フリューエントLTL
・拡張する ふゅーえんと
フリューエントLIGHT
・FLTLモデル検査
ゲーム分析
・ゲームに勝つかどうかを考える
コントロールできる状態と
コントロールできない状態にわける
論理の複雑性
LTL ２の指数じょう
リアクティビティ 指数
：
いつかはFになるを考える
結論Fから逆に考えていく
→結論から逆に再帰的に考える
→ツリーをいじるのではない。ツリーは終わらない
グラフを操作する：勝つところだけを逆から探し、そこに入ればかつでしょ！
→コントロールできる状態を選んでいく
制御を使った話（時間がなかったので急いで話してたので、めもとれなかった）
ツールでのシンセシス コントローラー
アクセス
トータル
ランキング
