セミナー内容

プロセス代数 CSP (Communicating Sequential Processes) は並行に動作するプロセスの振る舞いを記述し，性質を論証するための理論です．

理論への入門として，構文と操作的意味論を解説します．操作的意味論はプロセスの遷移を定めることでプロセスとは何かを明確にする方法です。

操作的意味論を使ってプロセスについての性質を証明する方法を解説します．机上で行う方法と定理証明支援系を使って行う方法の2通りを解説し，練習問題をやっていただきます．

プログラム

1. 構文と直観的意味
2. 操作的意味論
3. 遷移の導出
4. 演習：遷移の導出
5. 演習：状態遷移グラフの導出
6. Isabelle 上での形式化
7. 演習：遷移の導出
8. 演習：他に遷移がないことの証明

必要なもの

• 計算用紙と筆記用具
• 定理証明支援系 Isabelle https://isabelle.in.tum.de/

配布物と Zoom meeting URL

セミナー募集締め切り後に CONNPASS のメッセージにてお知らせします。

ご注意

• 配布スライド資料の公開は禁止です．
• 不測の事態が生じセミナーを開催または完遂できなかった場合は、日を改めて再開催することで対処させていただきます．
• 都合により申し込み後に参加できなくなった場合は，同等のセミナーを再演する際にご参加いただけるよう配慮しますのでご連絡ください．

参考書

• 並行システムの検証と実装, 磯部 祥尚
• Communicating Sequential Processes, C. A. R. Hoare
• The Theory and Practice of Concurrency, A.W. Roscoe
• Concurrent and Real-time Systems: The CSP Approach, Steve Schneider
• Understanding Concurrent Systems, A.W. Roscoe